Interpreter für Zahlentheorie, Modulo n

12

Ein Satz der Zahlentheorie (für unsere Zwecke) ist eine Folge der folgenden Symbole:

  • 0und '(Nachfolger) - Nachfolger bedeutet +1also0'''' = 0 + 1 + 1 + 1 + 1 = 4
  • +(Addition) und *(Multiplikation)
  • = (gleich)
  • (und )(Klammern)
  • der logische Operator nand( a nand bist not (a and b))
  • forall (der universelle Quantifizierer)

  • v0, v1, v2Usw. (Variablen)

    Hier ist ein Beispiel für einen Satz:

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

Hier not xist die Abkürzung für x nand x- der eigentliche Satz würde verwenden (v1*v1*v1 + v2*v2*v2 = v3*v3*v3) nand (v1*v1*v1 + v2*v2*v2 = v3*v3*v3), weil x nand x = not (x and x) = not x.

Dies besagt, dass für jede Kombination von drei natürlichen Zahlen v1, v2und v3es nicht der Fall ist, dass v1 3 + v2 3 = v3 3 (was aufgrund des letzten Satzes von Fermat zutreffen würde, mit Ausnahme der Tatsache, dass es 0 ^ 3 erhalten würde + 0 ^ 3 = 0 ^ 3).

Leider ist es, wie Gödel bewiesen hat, nicht möglich festzustellen, ob ein Satz in der Zahlentheorie wahr ist oder nicht.

Es ist jedoch möglich, wenn wir die Menge der natürlichen Zahlen auf eine endliche Menge beschränken.

Diese Herausforderung besteht also darin, zu bestimmen, ob ein Satz der Zahlentheorie, wenn er modulo genommen wird n , für eine positive ganze Zahl wahr ist oder nicht n. Zum Beispiel der Satz

forall v0 (v0 * v0 * v0 = v0)

(die Aussage, dass für alle Zahlen x x 3 = x ist)

Gilt nicht für normale Rechen (zB 2 3 = 8 ≠ 2), aber ist wahr , wenn genommen Modulo 3:

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

Eingabe- und Ausgabeformat

Die Eingabe ist ein Satz und eine positive Ganzzahl nin einem "vernünftigen" Format. Hier einige Beispiele für sinnvolle Formate für den Satz forall v0 (v0 * v0 * v0 = v0)in Zahlentheorie 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)"

Die Eingabe kann von stdin, einem Befehlszeilenargument, einer Datei usw. erfolgen.

Das Programm kann zwei verschiedene Ausgaben haben, um festzustellen, ob der Satz wahr ist oder nicht, z. B. kann es ausgegeben werden, yeswenn es wahr ist und nowenn es nicht wahr ist.

Sie müssen nicht unterstützen, dass eine Variable forallzweimal Gegenstand einer Variablen ist , z (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0)). Sie können davon ausgehen, dass Ihre Eingabe eine gültige Syntax hat.

Testfälle

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

Dies ist Code-Golf , also versuchen Sie, Ihr Programm so kurz wie möglich zu halten!

code-golf number-theory parsing code-golf kolmogorov-complexity code-golf code-golf array-manipulation matrix code-golf array-manipulation code-golf string code-challenge graphical-output compression code-golf kolmogorov-complexity code-golf sequence array-manipulation code-golf number base-conversion code-golf string decision-problem code-golf string ascii-art code-golf string random code-challenge brainfuck code-generation code-golf code-golf quine code-golf interpreter code-golf interpreter code-golf array-manipulation sorting code-golf halting-problem code-golf javascript code-golf algorithm code-golf arithmetic code-golf math counting code-golf math code-golf decision-problem radiation-hardening code-golf conversion bitwise code-golf number decision-problem code-golf string decision-problem code-golf random game code-golf ascii-art graphical-output code-golf decision-problem binary-tree tree-traversal code-challenge array-manipulation code-challenge graphical-output path-finding test-battery algorithm code-golf integer factorial code-golf binary-tree code-golf grid graph-theory code-golf regular-expression quine code-golf encoding code-golf king-of-the-hill javascript Leo Tenenbaum
quelle
1
Sind Variablennamen immer im Format v number?
Jo King
1
@JoKing Sie können, wenn Sie möchten, dass sie verwendet werden var number, oder sogar nur 1 + number(so 1wäre v0, 2wäre v1usw.)
Leo Tenenbaum
1
@JoKing Sie sollten (theoretisch) eine unendliche Anzahl von Variablen berücksichtigen. Es ist in Ordnung, wenn die maximale Anzahl von Variablen durch die maximale Größe einer Ganzzahl begrenzt ist, aber Sie sollten keine so niedrige Grenze haben. Sie können eines der anderen Eingabeformate auswählen, wenn dies für Sie ein Problem darstellt.
Leo Tenenbaum
1
@UnrelatedString Sicher, solange sie beliebig lang sein können.
Leo Tenenbaum
1
Kann man 'v numberstattdessen verwenden, v number'wenn wir die Präfix-Syntax-Option wählen?
Mr. Xcoder

Antworten:

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

Probieren Sie es online aus!

Übernimmt die Eingabe als verschachtelte Präfixsyntax mit fanstelle von forallund nanstelle von nand:

[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
TFeld
quelle
Im Moment gibt es Python-Code aus, aber es sollte zwei unterschiedliche Ausgaben haben, wenn der Satz wahr oder falsch ist. Sie können verwenden print(eval(g(*input()))).
Leo Tenenbaum
@LeoTenenbaum Ja, ich hatte das auf der ersten Version, aber vergessen, es nach dem Golfen wieder hinzuzufügen
TFeld
1

APL (Dyalog Unicode) , 129 Byte SBCS

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

Probieren Sie es online aus!

Nimmt einen Präfixsyntaxbaum wie in TFelds Python-Antwort , verwendet jedoch eine Ganzzahlcodierung. Die Kodierung ist

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

und jeder Variablen wird eine Nummer ab 8 zugewiesen. Diese Codierung unterscheidet sich geringfügig von der in der folgenden ungolfed-Version verwendeten, da ich sie beim Golfen des Codes angepasst habe.

Die Aufgabe umfasst nur zwei Eingaben (AST und Modulo). Wenn Sie sie jedoch als Operator anstelle einer Funktion schreiben, wird das Modulo nicht oft erwähnt (da es immer über rekursive Aufrufe übertragen wird).

Ungolfed mit Kommentaren

⍝ 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 z←3↑⍵
  zero≤x: ⍵           ⍝ zero or different variable: keep as is
  succ≡x: x(⍺∇y)      ⍝ succ: propagate to y
  forall≡x: 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 z←3↑⍵
  zero≡x:   0
  var≤x:    y                    ⍝ return attached value
  forall≡x: ∧/∇¨y replace∘z¨⍳⍺⍺  ⍝ check all replacements for given var
  succ≡x:   1+∇y
  plus≡x:   (∇y)+∇z
  times≡x:  (∇y)×∇z
  eq≡x:     0=⍺⍺|(∇y)-∇z         ⍝ modulo equality
  nand≡x:   (∇y)⍲∇z              ⍝ nand symbol does nand operation
}

Probieren Sie es online aus!

Bubbler
quelle