Wyjście pełny formalny puf takich stwierdzeń, takich jak 1+2=3, 2+2=2*(1+1)etc.

Intryga

Jeśli znasz arytmetykę Peano, prawdopodobnie możesz pominąć tę sekcję.

Oto jak definiujemy liczby naturalne:

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

Dlatego na przykład S(S(S(0)))jest liczbą.

Możesz użyć dowolnej równoważnej reprezentacji w kodzie. Na przykład wszystkie są poprawne:

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

Możemy rozszerzyć reguły, aby zdefiniować dodawanie w następujący sposób.

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

Dzięki temu możemy udowodnić 2 + 2 = 4 w następujący sposób

         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

Możemy rozszerzyć te reguły, aby zdefiniować mnożenie w następujący sposób

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

Chociaż, aby to umożliwić, musimy zdefiniować strukturalną rolę nawiasów.

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

Operatory dodawania i mnożenia są ściśle dwójkowe, a nawiasy muszą być zawsze wyraźne. A+B+Cnie jest dobrze zdefiniowane, ale (A+B)+Ci A+(B+C)są.

Przykład

Teraz mamy wystarczająco dużo, aby udowodnić twierdzenie o mnożeniu: 2 + 2 = 2 * 2

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

Wymagania

Dowód, żeA=B jest lista wyrażenia takie, że:

• pierwszy jest A,
• ostatnia to Bi
• każde wyrażenie na liście oprócz pierwszego można uzyskać z poprzedniego, przekształcając je zgodnie z jedną z reguł.

Twój program pobierze dwa prawidłowe wyrażenia jako dane wejściowe , każde wyrażenie zawiera liczby, dodawanie, mnożenie i nawiasy, jak zdefiniowano powyżej.

Twój program wyświetli dowód, listę zdefiniowaną powyżej, że oba wyrażenia są równe, jeśli taki dowód istnieje.

Jeśli dwa wyrażenia nie są równe, twój program nic nie wyświetli.

Udowodnienie lub obalenie jest zawsze możliwe w skończonej liczbie kroków, ponieważ każde wyrażenie można sprowadzić do jednej liczby, a liczby te można w trywialny sposób sprawdzić pod kątem równości.

Jeśli wyrażenia wejściowe są niepoprawne (np. Niezrównoważone nawiasy, zawierają nieliczbowe lub niebinarne operatory), wówczas twój program powinien zakończyć działanie z błędem, zgłosić wyjątek, wydrukować błąd lub w inny sposób wygenerować pewne obserwowalne zachowanie, które różni się od przypadek, w którym dane wejściowe są prawidłowe, ale nie równe .

Podsumowując, normalna wydajność dla dopuszczalnych danych wejściowych to lista równych liczb, w tym danych wejściowych, która jest generowana przez następujące reguły.

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

Każdy odpowiedni reprezentację liczb w wejścia i wyjścia wolno, na przykład 0=""=(), 3="###"=(((())))itp spacje znaczenia.

Reguły można oczywiście stosować w obu kierunkach. Twój program nie musi wypisywać, która reguła jest używana, tylko wyrażenie utworzone przez jego działanie na poprzednim wyrażeniu.

Najkrótszy kod wygrywa.

Perl, 166 + 1 bajtów

Uruchom z -p(1 bajtowa kara).

$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:""

Bardziej czytelny:

                           # niejawne: przeczytaj wiersz danych wejściowych do $ _
                           # pozostawiamy nowy wiersz włączony
$ r = '\ ((S *)'; # często używamy tego fragmentu wyrażenia regularnego, uwzględnij go
(@b, @a) = @a; # ustaw @b na @a, @a, aby opróżnić
Wciśnij @a, $ _ while # za każdym razem w pętli, dodaj $ _ do @a
+ s / \ + S / S + / || # reguła 2: zmień „+ S” na „S +”
s / $ r \ + \) / $ 1 / || # reguła 1: zmień „(X + 0)” na „X”
s / $ r \ * \) // || # zasada 3: zmień „(X * 0)” na „”
s / $ r \ * S (S *) / ((1 $ * 2 $) + 1 $ / || # reguła 4: zmień „(X * Y” na „((X * Y) + X”)
s / $ r \) / $ 1 /; # zasada 5: zmień „(X) na„ X ”
$ \. = / [^ S] ./ s; # dodaj 1 do znaku nowej linii, jeśli my
                           # zobacz dowolne nie-S, po którym następuje cokolwiek
$ _ = $ b [-1] eq $ a [-1]? # jeśli @b i @a kończą się w ten sam sposób
  dołącz '', @ b, odwróć @ a # następnie $ _ staje się @b, a następnie (@a wstecz)
  : „” # poza tym puste $ _
                           # niejawne: wynik $ _

Format wejściowy wyraża liczby jednostkowe jako ciągi znaków Si wymaga dwóch danych wejściowych w osobnych wierszach (po których następuje nowa linia i EOF po tym, jak oba są widoczne). Zinterpretowałem to jako wymaganie, aby nawiasy były dosłownie, ( )a dodawanie / mnożenie powinno być dosłownie + *; Mogę zaoszczędzić kilka bajtów, unikając ucieczki, jeśli będę mógł dokonywać różnych wyborów.

Algorytm faktycznie porównuje pierwszy wiersz wejścia z pustym wierszem, drugi z pierwszym, trzeci z drugim i tak dalej. Spełnia to wymagania pytania. Oto przykładowy przebieg:

Mój wkład:

(SS + SS)
(SS * SS)

Wyjście programu:

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

Duplikowanie SSSSw środku jest denerwujące, ale zdecydowałem, że nie naruszyło specyfikacji i pozostawiło mniej bajtów.

W przypadku nieprawidłowego wprowadzania dołączam 1znak nowego wiersza, więc 1na końcu wyniku są zasypywane zbłąkane znaki .