expand

The built-in function expand accepts one sentence expression value and uses the predicate or relation’s corresponding sentence definition to expand the sentence.

Syntax

expand([sentence argument expression])

Behavior

The argument must be an expression evaluating to a sentence expression value. If the argument is not a top-level predicate or relation, then an error is raised. If the argument has any unbound objects or predicates, an error is raised. If the predicate or relation has no sentence definition, then an error is raised.

If the argument is a top-level predicate, then the return value is a copy of the sentence definition with substituted unbound objects. The n-th unbound object of the sentence definition is substituted with the n-th argument of the predicate. The resulting sentence is returned.

If the argument is a top-level relation, then the return value is a copy of the sentence definition with the two unbound objects substituted. The first unbound object of the sentence definition is substituted with the first object related. The second unbound object of the sentence definition is substituted with the second object related. The resulting sentence is returned.

The returned sentence value is verified if and only if the argument sentence value is verified.

Examples

Suppose in is a relation with no sentence definition and = is defined so that for objects X and Y, X = Y if and only if the following sentence is true:

*Z(Z in X <-> Z in Y)

In other words, the above is the sentence definition of = when viewing X and Y as the first and second unbound objects.

Now suppose that NAT and W are two objects, and the variable equal stores the verified sentence:

NAT = W

Then the following expression:

expand(equal)

Evaluates to the following verified sentence:

*Z(Z in NAT <-> Z in W)

Now suppose successor is a predicate defined so that for any two objects X and Y, successor(X, Y) if and only if:

*Z(Z in X <-> Z in Y | Z = Y)

In other words, the above is the sentence definition of successor when regarding X and Y as the first and second unbound objects.

If A and B are objects, then the following expression:

expand(<: successor(A, B)>)

Evaluates to the unverified sentence:

*Z(Z in A <-> Z in B | Z = B)