Una oración de teoría de números (para nuestros propósitos) es una secuencia de los siguientes símbolos:
0
y'
(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 b
esnot (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 x
está 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
, v2
y 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 n
en 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 yes
si es verdadera y no
si no lo es.
No necesita admitir que una variable sea objeto de forall
dos 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 código de golf , así que trate de hacer su programa lo más corto posible
fuente
v number
?var number
, o incluso solo1 + number
(así1
seríav0
,2
seríav1
, etc.)'v number
lugar dev number'
si elegimos la opción de sintaxis de prefijo?Respuestas:
Python 2 ,
252236 bytesPruébalo en línea!
Toma la entrada como la sintaxis de prefijo anidado, con en
f
lugar deforall
y enn
lugar denand
:fuente
print(eval(g(*input())))
.APL (Dyalog Unicode) , SBCS de 129 bytes
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
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
Pruébalo en línea!
fuente