Interpreter teorii liczb, moduł n

12

Zdanie teoretycznej ± (naszych celów) jest sekwencją następującymi symbolami:

  • 0i '(następca) - następca oznacza +1, więc0'''' = 0 + 1 + 1 + 1 + 1 = 4
  • +(dodawanie) i *(mnożenie)
  • = (równy)
  • (i )(nawiasy)
  • operator logiczny nand( a nand bjest not (a and b))
  • forall (uniwersalny kwantyfikator)
  • v0, v1, v2Itd (zmienne)

    Oto przykład zdania:

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

Oto not xskrót x nand x- użyte byłoby właściwe zdanie (v1*v1*v1 + v2*v2*v2 = v3*v3*v3) nand (v1*v1*v1 + v2*v2*v2 = v3*v3*v3), ponieważ x nand x = not (x and x) = not x.

Stwierdza, że dla każdej kombinacji trzech liczb naturalnych v1, v2i v3to nie jest tak, że v1 3 + v2 3 = v3 3 (co byłoby prawdziwe, ponieważ Wielkie Twierdzenie Fermata, z wyjątkiem faktu, że to się 0 ^ 3 + 0 ^ 3 = 0 ^ 3).

Niestety, jak udowodnił Gödel, nie można ustalić, czy zdanie w teorii liczb jest prawdziwe.

Jest to jednak możliwe, jeśli ograniczymy zbiór liczb naturalnych do zbioru skończonego.

Tak więc wyzwanie polega na ustaleniu, czy zdanie teorii liczb jest prawdziwe, gdy jest brane modulo n , dla pewnej dodatniej liczby całkowitej n. Na przykład zdanie

forall v0 (v0 * v0 * v0 = v0)

(stwierdzenie, że dla wszystkich liczb x, x 3 = x)

Nie jest prawdziwe w przypadku zwykłej arytmetyki (np. 2 3 = 8 ≠ 2), ale jest prawdziwe, gdy weźmie się modulo 3:

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

Format wejściowy i wyjściowy

Dane wejściowe to zdanie i dodatnia liczba całkowita nw dowolnym „rozsądnym” formacie. Oto kilka przykładów rozsądnych formatów zdania forall v0 (v0 * v0 * v0 = v0)w teorii liczb 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)"

Dane wejściowe mogą pochodzić ze standardowego wejścia, argumentu wiersza poleceń, pliku itp.

Program może mieć dowolne dwa różne wyniki dla tego, czy zdanie jest prawdziwe, czy nie, np. Może wypisać, yesjeśli jest prawdziwe, a nojeśli nie.

Nie musisz obsługiwać jednej zmiennej będącej przedmiotem forallpodwójnej, np (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0)). Możesz założyć, że dane wejściowe mają poprawną składnię.

Przypadki testowe

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

To jest , więc postaraj się, aby twój program był jak najkrótszy!

Leo Tenenbaum
źródło
1
Czy nazwy zmiennych są zawsze w formacie v number?
Jo King
1
@JoKing Mogą, jeśli chcesz, aby były - możesz użyć var number, a nawet po prostu 1 + number(tak 1byłoby v0, 2byłoby v1itd.)
Leo Tenenbaum
1
@JoKing Powinieneś pozwolić (teoretycznie) na nieskończoną liczbę zmiennych. Jest w porządku, jeśli maksymalna liczba zmiennych jest ograniczona przez maksymalny rozmiar liczby całkowitej, ale nie powinieneś mieć tak niskiego limitu. Możesz wybrać jeden z pozostałych formatów wejściowych, jeśli jest to dla Ciebie problem.
Leo Tenenbaum,
1
@UnrelatedString Pewnie, o ile mogą być dowolnie długie.
Leo Tenenbaum,
1
Czy można użyć 'v numberzamiast, v number'jeśli wybieramy opcję prefiks-składnia?
Pan Xcoder,

Odpowiedzi:

3

Python 2 , 252 236 bajtów

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

Wypróbuj online!

Pobiera dane wejściowe jako zagnieżdżoną składnię prefiksu, z fzamiast foralli nzamiast nand:

[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
TFeld
źródło
W tej chwili wypisuje kod Pythona, ale powinien mieć dwa różne wyniki, jeśli zdanie jest prawdziwe lub fałszywe. Możesz użyć print(eval(g(*input()))).
Leo Tenenbaum
@LeoTenenbaum Tak, miałem to w pierwszej wersji, ale zapomniałem dodać ją ponownie po
grze
1

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

Wypróbuj online!

Pobiera drzewo składni prefiksu jak w odpowiedzi na python TFeld , ale używając kodowania liczb całkowitych. Kodowanie to

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

a każdej zmiennej przypisuje się liczbę zaczynającą się od 8. To kodowanie różni się nieco od kodu używanego w wersji bez golfa poniżej, ponieważ poprawiłem go podczas gry w golfa.

Zadanie obejmuje tylko dwa dane wejściowe (AST i modulo), ale zapisanie go jako operatora zamiast funkcji pozwala uniknąć wielokrotnego wspominania o module (ponieważ jest zawsze przenoszone przez wywołania rekurencyjne).

Niegolfowany z komentarzami

 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
}

Wypróbuj online!

Bubbler
źródło