Crie um poof formal completo de declarações como 1+2=3, 2+2=2*(1+1)etc.

Introução

Se você conhece o Peano Arithmetic, provavelmente pode pular esta seção.

Veja como definimos os números naturais:

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

Portanto, por exemplo, S(S(S(0)))é um número.

Você pode usar qualquer representação equivalente no seu código. Por exemplo, todos estes são válidos:

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

Podemos estender as regras para definir a adição da seguinte maneira.

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

Com isso, podemos provar 2 + 2 = 4 da seguinte maneira

         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

Podemos estender essas regras para definir a multiplicação da seguinte maneira

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

Embora para permitir isso, precisamos definir o papel estrutural dos parênteses.

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

Os operadores de adição e multiplicação são estritamente binários e os parênteses devem sempre ser explícitos. A+B+Cnão é bem definido, mas (A+B)+Ce A+(B+C)é.

Exemplo

Agora temos o suficiente para provar um teorema da multiplicação: 2 + 2 = 2 * 2

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

Exigências

Uma prova queA=B é uma lista de expressões como:

• a primeira é A,
• o último é Be
• cada expressão da lista, além da primeira, pode ser obtida da anterior, transformando-a em uma das regras.

Seu programa terá duas expressões válidas como entrada , cada expressão contém números, adição, multiplicação e parênteses, conforme definido acima.

Seu programa produzirá uma prova, uma lista como definida acima, de que as duas expressões são iguais, se essa prova existir.

Se as duas expressões não forem iguais, seu programa não produzirá nada.

É sempre possível provar ou refutar em um número finito de etapas, porque cada expressão pode ser reduzida a um único número e esses números podem ser testados trivialmente quanto à igualdade.

Se as expressões de entrada não forem válidas (por exemplo, parênteses desequilibrados, contenham números ou operadores não binários), seu programa deverá sair com erro, gerar uma exceção, imprimir um erro ou produzir algum comportamento observável distinto do caso em que as entradas são válidas, mas não iguais .

Em resumo, a saída normal para entradas admissíveis é uma lista de números iguais, incluindo as entradas, produzida pelas seguintes regras.

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

Qualquer representação adequada dos números na entrada e saída é permitida, por exemplo 0=""=(), 3="###"=(((()))), etc espaços em branco é irrelevante.

As regras podem, é claro, ser aplicadas em qualquer direção. Seu programa não precisa exibir qual regra é usada, apenas a expressão produzida por sua ação na expressão anterior.

O menor código vence.

Perl, 166 + 1 bytes

Corra com -p(penalidade de 1 byte).

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

Mais legível:

                           # implícito: leia uma linha de entrada em $ _
                           # deixamos a nova linha ativada
$ r = '\ ((S *)'; # usamos muito esse fragmento de expressão regular, fatorando-o
(@b, @a) = @a; # defina @b para @a, @a para esvaziar
pressione @a, $ _ enquanto # toda vez que fizer o loop, acrescente $ _ a @a
+ s / \ + S / S + / || # regra 2: altere "+ S" para "S +"
s / $ r \ + \) / $ 1 / || # regra 1: altere "(X + 0)" para "X"
s / $ r \ * \) // || # regra 3: altere "(X * 0)" para ""
s / $ r \ * S (S *) / (($ 1 * $ 2) + $ 1 / || # regra 4: altere "(X * Y" para "((X * Y) + X"
s / $ r \) / $ 1 /; # regra 5: altere "(X) para" X "
$ \. = / [^ S] ./ s; # anexa um 1 ao caractere de nova linha se
                           # vê qualquer não-S seguido por qualquer coisa
$ _ = $ b [-1] eq $ a [-1]? # if @b e @a terminam da mesma maneira
  junção '', @ b, inverter @ a #, em seguida, $ _ se torna @b seguido por (@a para trás)
  : "" # vazio, caso contrário, $ _
                           # implícito: output $ _

O formato de entrada expressa números em unário como cadeias de caracteres Se requer as duas entradas em linhas separadas (cada uma seguida por uma nova linha e um EOF depois que ambas são vistas). Interpretei a pergunta como exigindo que os parênteses sejam literalmente ( )e a adição / multiplicação seja literal + *; Eu posso salvar alguns bytes através de menos escape se me for permitido fazer escolhas diferentes.

Na verdade, o algoritmo compara a primeira linha de entrada com uma linha vazia, a segunda com a primeira, a terceira com a segunda e assim por diante. Isso cumpre os requisitos da pergunta. Aqui está um exemplo de execução:

Minha entrada:

(SS + SS)
(SS * SS)

Saída do programa:

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

A duplicação SSSSno meio é irritante, mas eu decidi que não violava a especificação, e há menos bytes para deixá-la.

Na entrada inválida, acrescento 1o caractere de nova linha, para que você fique disperso 1no final da saída.