Lurch core classes

Class

Declaration

In mathematics, we declare new variables and constants regularly, when we write text such as, "Let $n$ be any integer," or "So let $k$ be the unique value making $f(k)=t-1$ hold." We call these Declarations.

We do not distinguish different types of declaration (variable, constant, operator, symbol, etc.) but treat all declarations as behaving the same.

Each Declaration instance has a list of symbols being declared (which are instances of the Symbol class), and optionally a body that stipulates some fact about the symbols that is being stated by the declaration. For instance, in the declaration "Let $x\in A$ be arbitrary," the list of symbols contains just one entry, $x$, and the body is the statement being made about $x$, which is $x\in A$.

Unlike Expressions and Environments, Declarations do not respect the "given" attribute. A Declaration marked with such an attribute will not use that attribute in any algorithm, such as when validating the correctness of a deduction, or rendering a text-based form of the Declaration (such as putdown).

To see how Declarations impact how Symbols are processed, see the Scoping module.

Constructor

new Declaration(symbols, bodyopt)

Construct a declaration. The first argument must be either the Symbol to be declared or an array of one or more Symbols to be declared. The optional final argument is the body of the declaration.

In mathematics, we often declare symbols with certain conditions, such as "Let $x$ be any real number greater than $N$." In that sentence, we are declaring a variable $x$ and imposing on it a two-part condition (a conjunction), that $x$ is a real number and it is greater than $N$. Thus the body of the declaration would be that mathematical expression, $x\in\mathbb{R}\wedge x>N$. Or it could be formulated as an Environment with two claims, which are $x\in\mathbb{R}$ and $x>N$.

However, it is also possible to declare symbols with no conditions attached, as in the mathematical statement "Let $x$ be arbitrary." So the body of a declaration is optional.

The resulting Declaration instance will have as its children list the list of symbols it declares followed by the body, if a body is present.

Parameters

  • symbols Symbol | Array.<Symbol>

    Either a single Symbol instance or an array of Symbol instances. Note that this must be a Symbol in the sense of the class defined in this repository, rather than the standard JavaScript Symbol type. If a single symbol is passed, it will be treated as an array of just one symbol.

  • body LogicConcept <optional>

    An optional body of the declaration, as described above. The body may be any LogicConcept. If a declaration comes with several assumptions about the declared variables, they can be placed inside an Environment to conjoin them.

See

Source

Classes

Declaration

Methods

body() → {LogicConcept|undefined}

Returns the body of this declaration. For an explanation of the meaning of a declaration body, see the documentation for the constructor.

In those cases where the Declaration has a body, it will also be the Declaration's last child. Declarations that were not constructed with a body will have a simple placeholder object as their last child, a symbol indicating where the body would go if there were one. For such Declarations, this function returns undefined.

See

Returns

  • LogicConcept undefined

    The body provided to this object at construction time, if there was one, or undefined if not. If there was one, it is guaranteed to be an instance of the LogicConcept class.

Source

copy() → {Declaration}

We override here the default copy() method for LogicConcepts because that method assumes that the arguments the constructor requires are the LogicConcept's children. But in this case, we may need to collect several children into an array, passed as the first parameter.

See

  • copy()
  • equals()

Returns

  • Declaration

    a structural copy of this object

Source

removeBody()

Remove the body of this Declaration, if there is one, replacing it with a placeholder indicating that the Declaration now has no body. Thereafter, calling body() will return undefined.

See

Source

setBody()

Set a new body for this Declaration, replacing any old body that it had before (or, if it had none, replacing the placeholder that sits where a body would go). Thereafter, calling body() will return the new body provided to this function.

See

Source

symbols() → {Array.<Symbol>}

Return the array of Symbols provided to this object at construction time. This will be of length at least one, since the constructor requires there to be at least one symbol. The only exception to this rule is that Declarations, once constructed, can be modified by removing their children, so one could theoretically remove all symbols from a Declaration, putting it into an invalid form, so clients of this class should not do so.

See

Returns

  • Array.<Symbol>

    An array of Symbol instances, those symbols being declared by this object

Source