TNTNT

In TNTNT you have to write your program in the form of a proof. First all steps are followed and any invalid step that does not follow from the previous ones is skipped, and then it is checked if the last line is valid following from the previous steps. It is possible to receive input, and infinite loops. This proof system has exactly two rules and three axioms.

Expressions

An expression has the form of one of these three forms:

• name
• name(expression)
• name(expression,expression)

A name can contain any letters (uppercase and lowercase, case sensitive, minus signs, underscores, numbers, and # mark, Each name must be used always with the same number of parameters every time it occurs in the program, or in a rule or axiom; it is improper to use it a different number of times. No more than two parameters are permitted.

If a name is already used somewhere in the program with parentheses and commas, you can optionally, in any other places in the program, omit the parentheses and comma.

Rules

The rules you can use in constructing the proof are:

• Rule of Detachment: If you have a theorem "Imp(x,y)", and you also have a theorem "x", you can make "y".
• Rule of Metaness: If you have a theorem of the form "Imp(a,b)", where "a" contains one or more strings "#x(y)" (where "x" and "y" must be the same in all of them), you may select a string to replace all of them in "a" with, and then also replace all of "#x(z)" and "#x(w)" and so on in "b" with the same string, but replacing all of the "y" in that string with "z" and "w" and so on, instead. Restriction: Neither the replacement string, nor the strings "y" and and "z" and "w" and so on, is allowed to contain any "#".

Axioms

• Axiom of Separation: Imp(And(#x(Void),#y(Void)),#x(Void))
• Axiom of Program: The second axiom is defined by the first line in the program which isn't a special command. This line might contain macro expansions, and it might come from an include file.
• Axiom of Input: This axiom is the expression which comes from the user input.

Macros

• Godel number macro: [program] you cannot define macros inside of that program. The inside program must follow all proper number of parameters of outer program.
• Named macro: $m:name:expression;
• Macro parameters: $1 and $2 which must be used as an expression, in the syntax.
• Include file: $i:filename;
• Number conversion macro: $n:successor:zero; for example the command "$n:Succ:Zero;" will cause "3" to be converted to "Succ(Succ(Succ(Zero)))".
• Loop count: $c
• All theorem macro: $a makes it try this line using all theorems so far in place of this macro.
• Repeat nest macro: + for example "+And Zero One Two Three" assuming that "Zero" and "One" and "Two" and "Three" are having zero-parameters, will expand to "And(Zero,And(One,And(Two,Three)))".
• Temporary: $t(steps) which causes this theorem to expire after the specified number of steps.

Program Working

The program is working according to the following way:

1. Set loop counter to zero.
2. Assume all axioms are theorems. Do not destroy any previous theorems.
3. Run each line. If it is a valid step from a previous theorem by following the rules, it is added to the list of theorems, otherwise it is ignored.
4. If the last line is a theorem, stop. The output will be the value of the loop counter
5. If the last line is not a theorem, continue. Increment the loop counter and go back to step 2.

Note

There is something wrong with this!! Please write down (and discuss) what things are wrong with this, on the Talk page!!