Substitution

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.
Category:Languages
Category:Unknown computational class
Category:2021
Category:Unimplemented
Category:Declarative paradigm
Category:No_IO