Substitution

Substitution

Paradigm(s)	Declarative
Designed by	User:Hakerh400
Appeared in	2021
Computational class	Unknown
Reference implementation	Unimplemented
File extension(s)	.txt

Substitution is a declarative programming language invented by User:Hakerh400 in 2021.

Syntax

Source code consists of zero or more statements.

Statement

A statement consists of two expressions separated by an equals sign.

Expression

An expression can be one of the following:

• Structure
• Identifier
• Substitution

Structure

A structure is either a constant, or a pair.

Constants are represented by alphanumeric strings that start with an uppercase letter. Examples: A, B, C, Xyz, MyConstant. Two constants are equal iff they have the same name.

A pair consists of two expressions encapsulated into parentheses. Examples: (A B), (A (B C)), ((Abcde Xyz) ((P Q) R)). Two pairs are equal iff both of their corresponding expressions are equal. No pair is equal to a constant.

Identifier

Identifiers are represented by alphanumeric strings that start with a lowercase letter. Examples: abc, xyz, myIdent. Two identifiers that have the same name are equal. Two identifiers that do not have the same name may or may not be equal.

Substitution

Represented by three expressions encapsulated into brackets. Example: [myIdent A (X Y)].

Let $\alpha$, $\beta$, $\gamma$, $\delta$ be any expressions. Substitution [$\alpha$ $\beta$ $\gamma$] is equal to expression $\delta$ iff any of the following is true:

• $\alpha$ is equal to $\beta$ and $\delta$ is equal to $\gamma$
• $\alpha$ is not equal to $\beta$ and $\alpha$ is a constant and $\delta$ is equal to $\alpha$
• $\alpha$ is not equal to $\beta$ and $\alpha$ is equal to ($\alpha _{1}$ $\alpha _{2}$) (for some expressions $\alpha _{1}$ and $\alpha _{2}$) and $\delta$ is equal to ([$\alpha _{1}$ $\beta$ $\gamma$] [$\alpha _{2}$ $\beta$ $\gamma$])

Here is an example: is [(A B) A C] equal to (C B)? First, according to the third substitution rule, we conclude that [(A B) A C] is equal to ([A A C] [B A C]). Using the first substitution rule, we conclude that [A A C] is equal to C. Using the second rule, we conclude that [B A C] is equal to B. Since two pairs are equal iff they contain equal expressions, we conclude that [(A B) A C] is indeed equal to (C B).

Another example: consider substitution [(A A) (A A) B]. Using the first rule, we conclude that it is equal to B.

Semantics

If each identifier in the program can be replaced by a finite structure such that all statements are true, then the interpreter outputs sat. Otherwise, the interpreter outputs unsat.

Examples

Empty program

If there are no statements, the output is sat.

Same identifier

Program:

x = x

We can replace x with any structure (for example constant A) and we get A = A, which is true, because both A have the same name. The output is sat.

Same constant

Program:

A = A

This also trivially outputs sat.

Different constants

Program:

A = B

This is unsat, because A is not equal to B (they do not have the same name).

Transitivity of equality

Program:

x = A
x = B

From the first statement we conclude that x must be A, but the second statement asserts that x is B, so this is unsat.

Infinite structure

Program:

x = (A x)

This is unsat, because x cannot be a finite structure.

Infinite structure using a substitution

Program:

f = (A Arg)
x = [f Arg x]

This is also unsat. Identifier f is used like a function with formal argument Arg and [f Arg x] represents calling f with argument x. It reduces to x = (A x), which is the previous example.

Exclude a constant

Program:

[x A B] = [x A C]

This simply asserts that constant A does not appear anywhere in x. For example, x can be B, C, Xyz, (X, ((Y, Z), (P, Q))), but it cannot be A, (A, B), ((X, A), (Y, Z)), or anything that contains A. This is useful in implementing multi-argument functions. We can assert that the constant that represents the second formal argument does not apper in the structure that is passed as the first argument.

Negation

It is also possible to assert that two expressions are not equal. If we want to assert that two identifiers x and y are not equal, we can write the following program:

[(x x) (y y) A] = ([x (y y) A] [x (y y) A])

Note that A can be any constant, even a constant that appears in x or y. This exploits the definition of substitution. The second and the third substitution rule can be applied iff the first two parameters of the substitution are not equal. However, since we don't know whether x and y are constants or pairs, we encapsulate them into pairs and ensure that the result is not a constant (because a pair cannot be equal to a constant).

Russell's Paradox

Program:

x = [A x B]

Suppose that x = A, then we conclude that [A x B] = [A A B] = B and therefore x = B. Since A != B, it is a contradiction. Therefore, x != A. However, then [A x B] = A and thus x = A, a contradiction. The system is unsat.

Disjunction

It is also possible to implement a disjunction. If we want to assert that identifier x is either A or B, we can do the following:

x = [A y B]

where y is a new identifier that is not used anywhere else in the program. If y = A, then x = B, otherwise x = A.

Generalised disjunction

If we have any two expressions $\alpha$ and $\beta$ and we want to assert that x is either $\alpha$ or $\beta$, then we can do the following:

(x x) = [($\alpha$ $\alpha$) y ($\beta$ $\beta$)]
[$\alpha$ y A] = [$\alpha$ y B]

where y is a new identifier that is not used anywhere else in the program, and A and B are any two constants. We can also optionally assert that $\alpha \neq \beta$ using negation.

Single statement

Any program can be written using a single statement. If we have two statements

$\alpha$ = $\beta$
$\gamma$ = $\delta$

we can reduce them to

($\alpha$ $\gamma$) = ($\beta$ $\delta$)

Computational class

Unknown.

Interpreters

Unimplemented.