Transformation is complete/readable

This is dialect of Transformation is complete that is less beautiful but more readable.

Data types

• Set is a map that maps each non-set to a boolean.
• Function is a map that transforms value(s) into a value.
• Atom is atom. Simple.
• Boolean can be true, false or NaV (Not a Value).

The reason the sets are not functions is that a Turing machine must be able to compare two sets.

Note that there are two separate methods of application - A(B,C,...) for functions and A in B for sets. This was introduced because of readability.

"x is in y" is shortcut of "y maps x to true".

Syntax

Declarations

The program consists of any number of declarations. A declaration can be:

• Atom declaration - declares that a given atom(s) exist(s).

let A

• Set declaration - declares that a given set(s) exist(s). All values map to false by default, but it can be changed by axioms. Earlier axioms have more priority that later axioms.

set S

• Function declaration - declares that a given function(s) exist(s).

fet F

fet F(A,B,...)

• Axiom definition - Defines an axiom (see below).

An axiom definition is:

[axiom]: [expression]

Where [axiom] is the axiom's name and [expression] is an expression. An axiom is a definition of form [expression] is true.

Expressions

An expression can be formed with the rules below:

• true, false, NaV and _ are expressions.
• All names are expressions.
• If x is an expression that evaluates to a set, y is a literal and z is an expression, then For every y in x, z is an expression.
• If y is a literal and z is an expression, then For every y, z is an expression.
• If x is an expression that evaluates to a set, y is a literal and z is an expression, then For some y in x, z is an expression.
• If y is a literal and z is an expression, then For some y, z is an expression.
• If x is an expression and y is an expression that evaluates to a set, then x in y is an expression.
• If F is a function and A,B,... is a number of expressions equal to the number of F's arguments, then F(A,B,...) is an expression.
• If x and y are expressions, then x = y is an expression.
• If x and y are expressions that evaluate to booleans, then if x, then y is an expression.
• If x is an expression, then (x) is an expression.
• If R is a relation or expression, then not R is a relation or expression.

Expressions do some things:

• x in y returns what y maps x to.
• When evaluating F(A,B,...) check if there are any axioms regarding the function, apply them and return result. If not, if at least one argument is NaV, return NaV. Else, return unique atom.
• Names are always treated as free variables, except when there are some quatifiers over them.
• Quantifier For every y (in x), z: z is true for every y (in x).
• Quantifier For some y (in x), z: z is true for at least one y (in x).
• A = B is an equality relation: it returns true if A can be proven equal to B, false if they can't and NaV if they are both functions or one of them is NaV.
• if A, then B is an implication relation: it returns false if A is true and B is false, false for every other case involving only true and false, and NaV in all other cases.
• not R negates effect of R if R is a relation, turns true into false and false into true, returns complement of R if R is the set and returns NaV in every other case.
• For every function F, F(...,_,...) returns another function which gets all arguments substituded with _ in F and returns F with these args applied. _ can't occur outside the function call; in such case the expression where it was used automatically returns NaV. Note that if number of arguments applied to the function is less that required, then every non-listed argument is _ by default. Also F is the same as F().

If function call of F has too many arguments, then F is called only with required number of arguments, and then the result is called with the rest of arguments.

Execution

Execution of TiC:

• An input is taken as a logical statement.
• The program applies systematically axioms that can be applied to it.
• If it can be reduced to true, the program returns the sequence of axioms applied to it.
• If it can't, the program never halts.

Note that the exact output is interpreter-dependent (may be non-deterministic).

Examples

SKI calculus

You can perform any calculation that SKI calculus can, proving TiC Meta turing-complete. S, K and I are used in standard functional notation. You must surround entire program with parentheses and add in T to the end. If the program halts, the output is steps of computation; if not, no output is made.

set T
fet S(x,y,z), K(x,y), I(x)
CombS: S(x,y,z) = x(z,y(z))
CombK: K(x,y) = x
CombI: I(x) = x
SetS: S in T
SetK: K in T
SetI: I in T

Natural numbers

let 0
set N
fet F(x)
NatZero: 0 in N
NatSucc: for every x in N, S(x) in N
NatPrev: for every x, if S(x) = 0, then x not in N
NatEq: for every x in N, for every y in N, if S(x) = S(y), then x = y

Note that axiom of induction is redunant because every set always maps everything into false by default. Because of NatZero N maps zero into true, and because of NatSucc if x is proven to map into true, S(x) maps into true. N doesn't contain anything that can't be proved to be in it, so N is the set of standard natural numbers. Also every function transforms values into unique values by default, so it's obvious that for every x in N, S(x) not = x.