Transformation is complete

Transformation is complete is a theorem prover by the former User:TBPO, a big fan of User:Hakerh400. It has beautiful Greek aesthetics.

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 - juxtaposition in functions and AεB in sets. This was introduced because of aesthetics.

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

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 θ 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 Fx

fet Fxy

etc.

• 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 ι.

Expressions

An expression can be formed with the rules below:

• ι, θ, ψ and ω are expressions.
• All literals (one-character names) are expressions.
• If x is nothing or an expression that evaluates to a set, y is a literal and z is an expression, then xαyz is an expression.
• If x is an expression that evaluates to a set, y is a literal and z is an expression, then xβyz is an expression.
• If x is an expression and y is an expression that evaluates to a set, then xεy is an expression.
• If x is a function and Y is a number of expressions equal to the number of x's arguments, then xY 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 xτy is an expression.
• If x is an expression, then δxη is an expression.
• If R is a relation or expression, then ρR is a relation or expression.

Expressions do some things:

• xεy returns what y maps x to.
• When evaluating fxy... check if there are any axioms regarding the function, apply them and return result. If not, if at least one argument is ψ, return ψ. Else, return unique atom.
• Literals are always treated as free variables, except when there are some quatifiers over them.
• Quantifier xαyz: z is ι for every y (in x).
• Quantifier xβyz: z is ι for at least one y (in x).
• π is an equality relation: it returns ι if two values can be proven equal, θ if they can't and ψ if they are both functions.
• τ is an implication relation: AτB returns θ if A is ι and B is θ, ι if AB are any of ιι, θθ, θι and ψ in all other cases.
• ρR negates effect of R if R is a relation, turns ιθψ into θιψ if R is a boolean or returns ψ 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 ψ.

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 ι, 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.

Examples

SKI calculus

You can perform any calculation that SKI calculus can, proving TiC Meta turing-complete. S, K and I are typical in use, but you must replace parentheses with δ...η. You must also surround entire program with it and add εT to the end. If the program halts, the output is steps of computation; if not, no output is made.

set T
fet Sxyz, Kxy, Ix
CombS: Sxyzπxzδyzη
CombK: Kxyπx
CombI: Ixπx
SetS: SεT
SetK: KεT
SetI: IεT

Natural numbers

let 0
set N
fet Fx
NatZero: 0εN
NatSucc: Nαx SxεN
NatPrev: Nρεx Sxπ0
NatEq: Nαx Nαy SxπSyτxπy

Note that axiom of induction is redunant because every set always maps everything into θ by default. Because of NatZero N maps zero into ι, and because of NatSucc if x is proven to map into ι, Sx maps into ι. 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 Nαx Sxρπx.

See also

• More readable dialect