Ausgabe eine vollständige formale puh solcher Aussagen wie 1+2=3, 2+2=2*(1+1)usw.

Einführung

Wenn Sie Peano Arithmetic kennen, können Sie diesen Abschnitt wahrscheinlich überspringen.

So definieren wir die natürlichen Zahlen:

(Axiom 1) 0 is a number
(Axiom 2) If `x` is a number, the `S(x)`, the successor of `x`, is a number.

Daher ist zum Beispiel S(S(S(0)))eine Zahl.

Sie können in Ihrem Code jede äquivalente Darstellung verwenden. Zum Beispiel sind alle diese gültig:

0    ""    0           ()       !
1    "#"   S(0)        (())     !'
2    "##"  S(S(0))     ((()))   !''
3    "###" S(S(S(0)))  (((()))) !'''
...
etc

Wir können die Regeln wie folgt erweitern, um die Addition zu definieren.

(Rule 1) X+0 = X
(Rule 2) X+S(Y)=S(X)+Y

Damit können wir 2 + 2 = 4 wie folgt beweisen

         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

Wir können diese Regeln wie folgt erweitern, um die Multiplikation zu definieren

(Rule 3) X*0 = 0
(Rule 4) X*S(Y) = (X*Y) + X

Um dies zu ermöglichen, müssen wir jedoch die strukturelle Rolle von Klammern definieren.

(Axiom 3) If X is a number, (X) is the same number.

Additions- und Multiplikationsoperatoren sind streng binär und Klammern müssen immer explizit sein. A+B+Cist nicht genau definiert, aber(A+B)+C und A+(B+C)sind.

Beispiel

Jetzt haben wir genug, um einen Satz über die Multiplikation zu beweisen: 2 + 2 = 2 * 2

2 + 2
(2) + 2
(0 + 2) + 2
((0*2) + 2) + 2
(1*2) + 2
2*2

Bedarf

Ein Beweis, derA=B Ausdrücke einer Liste ist, wie:

• das erste ist A ,
• der letzte ist B und
• Jeder Ausdruck in der Liste, mit Ausnahme des ersten, kann aus dem vorherigen erhalten werden, indem er nach einer der Regeln transformiert wird.

Ihr Programm verwendet zwei gültige Ausdrücke als Eingabe . Jeder Ausdruck enthält Zahlen, Additionen, Multiplikationen und Klammern, wie oben definiert.

Ihr Programm gibt einen Beweis aus, eine Liste wie oben definiert, dass die beiden Ausdrücke gleich sind, wenn ein solcher Beweis existiert.

Wenn die beiden Ausdrücke nicht gleich sind, gibt Ihr Programm nichts aus.

Beweisen oder widerlegen ist immer in einer endlichen Anzahl von Schritten möglich, da jeder Ausdruck auf eine einzige Zahl reduziert werden kann und diese Zahlen trivial auf Gleichheit geprüft werden können.

Wenn die eingegebenen Ausdrücke ungültig sind (z. B. unausgeglichene Klammern, nicht numerische oder nicht binäre Operatoren), sollte Ihr Programm mit einem Fehler beendet werden, eine Ausnahme auslösen, einen Fehler ausgeben oder auf andere Weise ein anderes beobachtbares Verhalten erzeugen, das sich vom unterscheidet Fall, in dem die Eingaben gültig, aber ungleich sind .

Zusammenfassend ist die normale Ausgabe für zulässige Eingaben eine Liste gleicher Zahlen, einschließlich der Eingaben, die nach den folgenden Regeln erstellt wird.

(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.)

Jede geeignete Darstellung der Zahlen in der Ein- und Ausgabe erlaubt ist , zum Beispiel 0=""=(),3="###"=(((()))) usw. Leerraum ist dabei unerheblich.

Regeln können natürlich in beide Richtungen angewendet werden. Ihr Programm muss nicht ausgeben, welche Regel verwendet wird, sondern nur den Ausdruck, der durch die Aktion auf den vorherigen Ausdruck erzeugt wird.

Kürzester Code gewinnt.

Perl, 166 + 1 Bytes

Laufen Sie mit -p(1 Byte Strafe).

$r='\((S*)';(@b,@a)=@a;push@a,$_ while+s/\+S/S+/||s/$r\+\)/$1/||s/$r\*\)//||s/$r\*S(S*)/(($1*$2)+$1/||s/$r\)/$1/;$\.=/[^S]./s;$_=$b[-1]eq$a[-1]?join'',@b,reverse@a:""

Besser lesbar:

                           # implicit: lies eine Eingabezeile in $ _
                           # Wir lassen die Newline auf
$ r = '\ ((S *)'; # Wir verwenden dieses Regex-Fragment häufig, ziehen es heraus
(@b, @a) = @a; # setze @b auf @a, @a auf leer
Drücken Sie @a, $ _, während # jedes Mal, wenn Sie die Schleife durchlaufen, $ _ an @a anhängt
+ s / \ + S / S + / || # Regel 2: Ändere "+ S" in "S +"
s / $ r \ + \) / $ 1 / || # Regel 1: "(X + 0)" in "X" ändern
s / $ r \ * \) // || # Regel 3: Ändern Sie "(X * 0)" in "".
s / $ r \ * S (S *) / (($ 1 * $ 2) + $ 1 / || # Regel 4: Ändere "(X * Y" in "((X * Y) + X"
s / $ r \) / $ 1 /; # Regel 5: Ändere "(X) in" X "
$ \. = / [^ S] ./ s; # füge eine 1 an das Newline-Zeichen an, wenn wir
                           # sehen alle Nicht-S, gefolgt von irgendetwas
$ _ = $ b [-1] eq $ a [-1]? # wenn @b und @a auf die gleiche Weise enden
  join '', @ b, reverse @ a # dann wird $ _ @b gefolgt von (@a rückwärts)
  : "" # sonst leer $ _
                           # implizit: $ _ ausgeben

Das Eingabeformat drückt Zahlen unär als Zeichenfolgen aus Sund erfordert zwei Eingaben in separaten Zeilen (jeweils gefolgt von einer neuen Zeile und einer EOF, nachdem beide angezeigt wurden). Ich habe die Frage so interpretiert, dass Klammern wörtlich ( )und Addition / Multiplikation wörtlich sein müssen + *. Ich kann ein paar Bytes sparen, indem ich weniger Escape-Zeichen verwende, wenn ich andere Entscheidungen treffen darf.

Der Algorithmus vergleicht tatsächlich die erste Eingabezeile mit einer Leerzeile, die zweite mit der ersten, die dritte mit der zweiten usw. Dies erfüllt die Anforderungen der Frage. Hier ist ein Beispiellauf:

Meine Eingabe:

(SS + SS)
(SS * SS)

Programmausgabe:

(SSS + S)
(SSSS +)
SSSS
SSSS
(SSSS +)
((SS +) SS +)
(((SS *) SS +) SS +)
(((SS *) S + S) SS +)
(((SS *) + SS) SS +)
((SS * S) SS +)
((SS * S) S + S)
((SS * S) + SS)

Das Duplizieren SSSSin der Mitte ist ärgerlich, aber ich habe entschieden, dass es nicht gegen die Spezifikation verstößt, und es sind weniger Bytes, um es zu belassen.

Bei ungültiger Eingabe 1hänge ich an das Zeilenvorschubzeichen an, sodass Sie 1am Ende der Ausgabe mit Streusymbolen überhäuft werden.