Intérprete para teoria dos números, módulo n

12

Uma frase da teoria dos números (para nossos propósitos) é uma sequência dos seguintes símbolos:

  • 0e '(sucessor) - sucessor significa +1, então0'''' = 0 + 1 + 1 + 1 + 1 = 4
  • +(adição) e *(multiplicação)
  • = (igual a)
  • (e )(parênteses)
  • o operador lógico nand( a nand bé not (a and b))
  • forall (o quantificador universal)
  • v0, v1, v2, Etc. (variáveis)

    Aqui está um exemplo de uma frase:

forall v1 (forall v2 (forall v3 (not (v1*v1*v1 + v2*v2*v2 = v3*v3*v3))))

Aqui not xestá uma abreviação de x nand x- a frase real usaria (v1*v1*v1 + v2*v2*v2 = v3*v3*v3) nand (v1*v1*v1 + v2*v2*v2 = v3*v3*v3), porque x nand x = not (x and x) = not x.

Isto indica que para cada combinação de três números naturais v1, v2e v3, não é o caso que v1 3 + v2 3 = v3 3 (o que seria verdade, porque de último teorema de Fermat, exceto pelo fato de que ele iria ficar 0 ^ 3 + 0 ^ 3 = 0 ^ 3).

Infelizmente, como provado por Gödel, não é possível determinar se uma sentença na teoria dos números é verdadeira ou não.

Ele é possível, no entanto, se restringir o conjunto dos números naturais para um conjunto finito.

Portanto, esse desafio é determinar se uma sentença da teoria dos números é verdadeira ou não, quando usada no módulo n , para um número inteiro positivo n. Por exemplo, a frase

forall v0 (v0 * v0 * v0 = v0)

(a declaração de que, para todos os números x, x 3 = x)

Não é verdadeiro para aritmética comum (por exemplo, 2 3 = 8 ≠ 2), mas é verdadeiro quando usado no módulo 3:

0 * 0 * 0 ≡ 0 (mod 3)
1 * 1 * 1 ≡ 1 (mod 3)
2 * 2 * 2 ≡ 8 ≡ 2 (mod 3)

Formato de entrada e saída

A entrada é uma sentença e um número inteiro positivo nem qualquer formato "razoável". Aqui estão alguns exemplos de formatos razoáveis ​​para a frase forall v0 (v0 * v0 * v0 = v0)no módulo de teoria dos números 3:

("forall v0 (v0 * v0 * v0 = v0)", 3)
"3:forall v0 (((v0 * v0) * v0) = v0)"
"(forall v0)(((v0 * v0) * v0) = v0) mod 3" 
[3, "forall", "v0", "(", "(", "(", "v0", "*", "v0", ")", "*", "v0", ")", "=", "v0", ")"]
(3, [8, 9, 5, 5, 5, 9, 3, 9, 6, 3, 9, 6, 4, 9, 6]) (the sentence above, but with each symbol replaced with a unique number)
"f v0 = * * v0 v0 v0 v0"
[3, ["forall", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
"3.v0((v0 * (v0 * v0)) = v0)"

A entrada pode ser de stdin, um argumento de linha de comando, um arquivo etc.

O programa pode ter duas saídas distintas para saber se a sentença é verdadeira ou não, por exemplo, pode gerar yesse for verdadeira e nose não for.

Você não precisa suportar uma variável que é objeto de forallduas vezes, por exemplo (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0)). Você pode assumir que sua entrada possui sintaxe válida.

Casos de teste

forall v0 (v0 * v0 * v0 = v0) mod 3
true

forall v0 (v0 * v0 * v0 = v0) mod 4
false (2 * 2 * 2 = 8 ≡ 0 mod 4)

forall v0 (v0 = 0) mod 1
true (all numbers are 0 modulo 1)

0 = 0 mod 8
true

0''' = 0 mod 3
true

0''' = 0 mod 4
false

forall v0 (v0' = v0') mod 1428374
true

forall v0 (v0 = 0) nand forall v1 (v1 = 0) mod 2
true (this is False nand False, which is true)

forall v0 ((v0 = 0 nand v0 = 0) nand ((forall v1 (v0 * v1 = 0' nand v0 * v1 = 0') nand forall v2 (v0 * v2 = 0' nand v0 * v2 = 0')) nand (forall v3 (v0 * v3 = 0' nand v0 * v3 = 0') nand forall v4 (v0 * v4 = 0' nand v0 * v4 = 0')))) mod 7
true
(equivalent to "forall v0 (v0 =/= 0 implies exists v1 (v0 * v1 = 0)), which states that every number has a multiplicative inverse modulo n, which is only true if n is 1 or prime)

forall v0 ((v0 = 0 nand v0 = 0) nand ((forall v1 (v0 * v1 = 0' nand v0 * v1 = 0') nand forall v2 (v0 * v2 = 0' nand v0 * v2 = 0')) nand (forall v3 (v0 * v3 = 0' nand v0 * v3 = 0') nand forall v4 (v0 * v4 = 0' nand v0 * v4 = 0')))) mod 4
false

Isso é , então tente tornar o seu programa o mais curto possível!

Leo Tenenbaum
fonte
11
Os nomes das variáveis ​​estão sempre no formato v number?
Jo rei
11
@JoKing Eles podem se você quer que eles ser- você pode usar var number, ou mesmo apenas 1 + number(assim 1seria v0, 2seria v1, etc.)
Leo Tenenbaum
11
@JoKing Você deve permitir (teoricamente) um número infinito de variáveis. Tudo bem se o número máximo de variáveis ​​estiver delimitado pelo tamanho máximo de um número inteiro, mas você não deve ter um limite tão baixo. Você pode escolher um dos outros formatos de entrada se isso for um problema para você.
Leo Tenenbaum
11
@UnrelatedString Claro, desde que eles possam ser arbitrariamente longos.
Leo Tenenbaum
11
Pode-se usar em 'v numbervez de v number'escolhermos a opção prefixo-sintaxe?
Mr. Xcoder

Respostas:

3

Python 2 , 252 236 bytes

def g(n,s):
 if str(s)==s:return s.replace("'","+1")
 o,l,r=map(g,[n]*3,s);return['all((%s)for %s in range(%d))'%(r,l,n),'not((%s)*(%s))'%(l,r),'(%s)%%%d==(%s)%%%d'%(l,n,r,n),'(%s)%s(%s)'%(l,o,r)]['fn=+'.find(o)]
print eval(g(*input()))

Experimente online!

Recebe a entrada como prefixo-sintaxe aninhada, com em fvez de foralle em nvez de nand:

[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
TFeld
fonte
No momento, está produzindo código Python, mas deve ter duas saídas distintas, se a sentença for verdadeira ou falsa. Você pode usar print(eval(g(*input()))).
Leo Tenenbaum
@LeoTenenbaum Sim, eu tive que na primeira versão, mas esqueceu-se de adicioná-lo de volta depois de golfe
TFeld
1

APL (Dyalog Unicode) , 129 bytes SBCS

{x y z3↑⍵⋄7x:y×7<x5x:∧/∇¨y{⍵≡⍺⍺:⍵⍺⋄x y z3↑⍵⋄7x:⍵⋄6x:x(⍺∇y)⋄x(⍺∇⍣(5x)⊢y)(⍺∇z)}∘z¨⍳⍺⍺⋄y←∇y6x:1+yy(⍎x'+×⍲',⊂'0=⍺⍺|-')∇z}

Experimente online!

Toma uma árvore de sintaxe de prefixo, como na resposta python do TFeld , mas usando uma codificação inteira. A codificação é

plus times nand eq forall succ zero  1 2 3 4 5 6 7

e a cada variável é atribuído um número a partir de 8. Essa codificação é um pouco diferente da usada na versão sem golf abaixo, porque eu a aprimorei enquanto jogava o código.

A tarefa envolve apenas duas entradas (o AST e o módulo), mas escrevê-lo como um operador em vez de uma função evita mencionar o módulo muitas vezes (como sempre é realizado em chamadas recursivas).

Ungolfed com comentários

 node types; anything 8 will be considered a var
plus times eq nand forall succ zero var←⍳8
 AST nodes have 1~3 length, 1st being the node type
 zero  zero, succ  succ arg, var  var | var value (respectively)

 to (from replace) AST  transform AST so that 'from' var has the value 'to' attached
replace←{
  ⍵≡⍺⍺:⍵⍺              variable found, attach the value
  x y z3↑⍵
  zerox:             zero or different variable: keep as is
  succx: x(⍺∇y)       succ: propagate to y
  forallx: x y(⍺∇z)   forall: propagate to z
  x(⍺∇y)(⍺∇z)          plus, times, eq, nand: propagate to both args
}
 (mod eval) AST  evaluate AST with the given modulo
eval←{
  x y z3↑⍵
  zerox:   0
  varx:    y                     return attached value
  forallx: ∧/∇¨y replacez¨⍳⍺⍺   check all replacements for given var
  succx:   1+∇y
  plusx:   (∇y)+∇z
  timesx:  (∇y)×∇z
  eqx:     0=⍺⍺|(∇y)-∇z          modulo equality
  nandx:   (∇y)⍲∇z               nand symbol does nand operation
}

Experimente online!

Bubbler
fonte