Interprète pour la théorie des nombres, modulo n

12

Une phrase de la théorie des nombres (pour nos besoins) est une séquence des symboles suivants:

  • 0et '(successeur) - successeur signifie +1, donc0'''' = 0 + 1 + 1 + 1 + 1 = 4
  • +(addition) et *(multiplication)
  • = (égal à)
  • (et )(parenthèses)
  • l'opérateur logique nand( a nand best not (a and b))
  • forall (le quantificateur universel)
  • v0, v1, v2, Etc. (variables)

    Voici un exemple de phrase:

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

Voici un not xraccourci pour x nand x- la phrase réelle utiliserait (v1*v1*v1 + v2*v2*v2 = v3*v3*v3) nand (v1*v1*v1 + v2*v2*v2 = v3*v3*v3), car x nand x = not (x and x) = not x.

Cet article stipule que pour chaque combinaison de trois nombres naturels v1, v2et v3, il est pas le cas que v1 3 + v2 3 = v3 3 ( ce qui serait vrai à cause du dernier théorème de Fermat, à l' exception du fait qu'il obtiendrait 0 ^ 3 + 0 ^ 3 = 0 ^ 3).

Malheureusement, comme l'a prouvé Gödel, il n'est pas possible de déterminer si une phrase de la théorie des nombres est vraie ou non.

Il est possible, cependant, si nous limitons l'ensemble des nombres naturels à un ensemble fini.

Donc, ce défi consiste à déterminer si une phrase de la théorie des nombres est vraie, lorsqu'elle est prise modulo n , pour un entier positif n. Par exemple, la phrase

forall v0 (v0 * v0 * v0 = v0)

(la déclaration que pour tous les nombres x, x 3 = x)

N'est pas vrai pour l'arithmétique ordinaire (par exemple 2 3 = 8 ≠ 2), mais est vrai lorsqu'il est pris modulo 3:

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

Format d'entrée et de sortie

L'entrée est une phrase et un entier positif ndans n'importe quel format "raisonnable". Voici quelques exemples de formats raisonnables pour la phrase forall v0 (v0 * v0 * v0 = v0)dans la théorie des nombres modulo 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)"

L'entrée peut provenir de stdin, d'un argument de ligne de commande, d'un fichier, etc.

Le programme peut avoir deux sorties distinctes pour savoir si la phrase est vraie ou non, par exemple, il pourrait sortir yessi c'est vrai et nosi ce n'est pas le cas.

Vous n'avez pas besoin de prendre en charge une variable faisant l'objet d'un foralldouble, par exemple (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0)). Vous pouvez supposer que votre entrée a une syntaxe valide.

Cas de test

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

Il s'agit de , alors essayez de rendre votre programme le plus court possible!

Leo Tenenbaum
la source
1
Les noms de variables sont-ils toujours au format v number?
Jo King
1
@JoKing Ils peuvent si vous voulez qu'ils soient - vous pouvez utiliser var number, ou même simplement 1 + number(ce 1serait le cas v0, le 2serait v1, etc.)
Leo Tenenbaum
1
@JoKing Vous devez autoriser (théoriquement) un nombre infini de variables. Ce n'est pas grave si le nombre maximal de variables est limité par la taille maximale d'un entier, mais vous ne devriez pas avoir une limite aussi basse. Vous pouvez choisir l'un des autres formats d'entrée si cela vous pose problème.
Leo Tenenbaum
1
@UnrelatedString Bien sûr, tant qu'ils peuvent être arbitrairement longs.
Leo Tenenbaum
1
Peut-on utiliser à la 'v numberplace de v number'si on choisit l'option préfixe-syntaxe?
M. Xcoder du

Réponses:

3

Python 2 , 252 236 octets

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

Essayez-le en ligne!

Prend l'entrée comme syntaxe de préfixe imbriquée, avec fau lieu de forallet nau lieu de nand:

[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
TFeld
la source
En ce moment, il génère du code Python, mais il devrait avoir deux sorties distinctes pour si la phrase est vraie ou fausse. Vous pouvez utiliser print(eval(g(*input()))).
Leo Tenenbaum
@LeoTenenbaum Oui, je l'avais sur la première version, mais j'ai oublié de l'ajouter après le golf
TFeld
1

APL (Dyalog Unicode) , 129 octets 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}

Essayez-le en ligne!

Prend un arbre de syntaxe de préfixe comme dans la réponse python de TFeld , mais en utilisant un codage entier. L'encodage est

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

et chaque variable se voit attribuer un numéro à partir de 8. Cet encodage est légèrement différent de celui utilisé dans la version non golfée ci-dessous, car je l'ai modifié pendant que je jouais au code.

La tâche n'implique que deux entrées (l'AST et le modulo), mais l'écrire en tant qu'opérateur au lieu d'une fonction évite de mentionner le modulo plusieurs fois (car il est toujours reporté sur les appels récursifs).

Non golfé avec des commentaires

 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
}

Essayez-le en ligne!

Bubbler
la source