Intérprete para teoría de números, módulo n

12

Una oración de teoría de números (para nuestros propósitos) es una secuencia de los siguientes símbolos:

  • 0y '(sucesor) - sucesor significa +1, entonces0'''' = 0 + 1 + 1 + 1 + 1 = 4
  • +(suma) y *(multiplicación)
  • = (igual a)
  • (y )(paréntesis)
  • el operador lógico nand( a nand bes not (a and b))
  • forall (el cuantificador universal)
  • v0, v1, v2, Etc. (variables)

    Aquí hay un ejemplo de una oración:

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

Aquí not xestá la abreviatura de x nand x: la oración real se usaría (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.

Esto indica que por cada combinación de tres números naturales v1, v2y v3, no es el caso que v1 3 + v2 3 = v3 3 (que sería cierto debido último teorema de Fermat, excepto por el hecho de que obtendría 0 ^ 3 + 0 ^ 3 = 0 ^ 3).

Desafortunadamente, como lo demostró Gödel, no es posible determinar si una oración en la teoría de números es verdadera o no.

Sin embargo, es posible si restringimos el conjunto de números naturales a un conjunto finito.

Entonces, este desafío es determinar si una oración de la teoría de números es verdadera, cuando se toma un módulo n , para algún número entero positivo n. Por ejemplo, la oración

forall v0 (v0 * v0 * v0 = v0)

(la afirmación de que para todos los números x, x 3 = x)

No es cierto para la aritmética ordinaria (por ejemplo, 2 3 = 8 ≠ 2), pero es cierto cuando se toma el 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 y salida.

La entrada es una oración y un entero positivo nen cualquier formato "razonable". Aquí hay algunos ejemplos de formatos razonables para la oración forall v0 (v0 * v0 * v0 = v0)en la teoría de números módulo 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)"

La entrada puede ser de stdin, un argumento de línea de comando, un archivo, etc.

El programa puede tener dos salidas distintas para saber si la oración es verdadera o no, por ejemplo, podría salir yessi es verdadera y nosi no lo es.

No necesita admitir que una variable sea objeto de foralldos veces, por ejemplo (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0)). Puede suponer que su entrada tiene una sintaxis válida.

Casos de prueba

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

Este es el , así que trate de hacer su programa lo más corto posible

Leo Tenenbaum
fuente
1
¿Los nombres de las variables están siempre en el formato v number?
Jo King
1
@JoKing Pueden hacerlo si quieres que sean, puedes usar var number, o incluso solo 1 + number(así 1sería v0, 2sería v1, etc.)
Leo Tenenbaum
1
@JoKing Debe permitir (teóricamente) un número infinito de variables. Está bien si el número máximo de variables está limitado por el tamaño máximo de un número entero, pero no debería tener un límite tan bajo. Puede elegir uno de los otros formatos de entrada si esto es un problema para usted.
Leo Tenenbaum
1
@UnrelatedString Claro, siempre que puedan ser arbitrariamente largos.
Leo Tenenbaum
1
¿Se puede usar en 'v numberlugar de v number'si elegimos la opción de sintaxis de prefijo?
Sr. Xcoder

Respuestas:

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

Pruébalo en línea!

Toma la entrada como la sintaxis de prefijo anidado, con en flugar de forally en nlugar de nand:

[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
TFeld
fuente
En este momento está generando código Python, pero debería tener dos salidas distintas para si la oración es verdadera o falsa. Puedes usar print(eval(g(*input()))).
Leo Tenenbaum
@LeoTenenbaum Sí, tuve eso en la primera versión, pero olvidé agregarlo nuevamente después del golf
TFeld
1

APL (Dyalog Unicode) , SBCS de 129 bytes

{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}

Pruébalo en línea!

Toma un árbol de sintaxis de prefijos como en la respuesta de Python de TFeld , pero usando una codificación entera. La codificación es

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

y a cada variable se le asigna un número a partir de 8. Esta codificación es ligeramente diferente de la que se usa en la siguiente versión no protegida, porque la modifiqué mientras jugaba el código.

La tarea involucra solo dos entradas (el AST y el módulo), pero escribirlo como un operador en lugar de una función evita mencionar el módulo muchas veces (ya que siempre se realiza a través de llamadas recursivas).

Ungolfed con comentarios

 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
}

Pruébalo en línea!

Bubbler
fuente