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.