12
1
Output a full formal poof of such statements such as 1+2=3
, 2+2=2*(1+1)
etc.
Introuction
If you know Peano Arithmetic you can probably skip this section.
Here's how we define the Natural Numbers:
(Axiom 1) 0 is a number
(Axiom 2) If `x` is a number, the `S(x)`, the successor of `x`, is a number.
Hence, for example S(S(S(0)))
is a number.
You can use any equivalent representation in your code. For example, all of these are valid:
0 "" 0 () !
1 "#" S(0) (()) !'
2 "##" S(S(0)) ((())) !''
3 "###" S(S(S(0))) (((()))) !'''
...
etc
We can extend the rules to define addition as follows.
(Rule 1) X+0 = X
(Rule 2) X+S(Y)=S(X)+Y
With this we can prove 2+2=4 as follows
S(S(0)) + S(S(0)) = 2 + 2
[Rule 2 with X=S(S(0)), Y=S(0)]
S(S(S(0))) + S(0) = 3 + 1
[Rule 2 with X=S(S(S(0))), Y=0]
S(S(S(S(0)))) + 0 = 4 + 0
[Rule 1 with X=S(S(S(S(0))))
S(S(S(S(0)))) = 4
We can extend these rules to define multiplication as follows
(Rule 3) X*0 = 0
(Rule 4) X*S(Y) = (X*Y) + X
Although to allow this we need to define the structural role of parentheses.
(Axiom 3) If X is a number, (X) is the same number.
Addition and multiplication operators are strictly binary and parentheses must always be explicit. A+B+C
is not well-defined, but (A+B)+C
and A+(B+C)
are.
Example
Now we have enough to prove a theorem about multiplication: 2+2=2*2
2 + 2
(2) + 2
(0 + 2) + 2
((0*2) + 2) + 2
(1*2) + 2
2*2
Requirements
A proof that A=B
is a list expressions such that:
- the first is
A
, - the last is
B
, and - each expression in the list apart from the first can obtained from the previous by transforming it under one of the rules.
Your program will take two valid expressions as input, each expression contains numbers, addition, multiplication, and parentheses as defined above.
Your program will output a proof, a list as defined above, that the two expressions are equal, if such a proof exists.
If the two expressions are not equal, your program will output nothing.
Proving or disproving is always possible in a finite number of steps, because each expression can be reduced to a single number and these numbers can be trivially tested for equality.
If the input expressions are not valid (e.g. unbalanced parentheses, contains non-numbers, or non-binary operators) then your program should exit with error, throw an exception, print an error, or otherwise produce some observable behaviour which is distinct from the case in which the inputs are valid but non-equal.
In summary, the normal output for admissible inputs is a list of equal numbers, including the inputs, which is produced by the following rules.
(Axiom 1) 0 is a number
(Axiom 2) If `x` is a number, the `S(x)`, the successor of `x`, is a number.
(Axiom 3) If X is a number, (X) is the same number
(Rule 1) X+0 = X
(Rule 2) X+S(Y)=S(X)+Y
(Rule 3) X*0 = 0
(Rule 4) X*S(Y) = (X*Y) + X
(Rule 5) X = (X) (Axiom 3 expressed as a transformation rule.)
Any suitable representation of the numbers in the input and output is allowed, e.g. 0=""=()
, 3="###"=(((())))
, etc. Whitespace is irrelevant.
Rules can, of course, be applied in either direction. Your program does not have to output which rule is used, just the expression produced by its action on the previous expression.
Shortest code wins.
Some examples of proofs converting expressions to numbers and back – LegionMammal978 – 2016-11-22T13:08:31.907