Interpreter for number theory, modulo n

Question

A sentence of number theory (for our purposes) is a sequence of the following symbols:

• 0 and ' (successor) - successor means +1, so 0'''' = 0 + 1 +たす 1 +たす 1 +たす 1 =わ 4

• + (addition) and * (multiplication)

• = (equal to)

• ( and ) (parentheses)

• the logical operator nand (a nand b is not (a and b))

• forall (the universal quantifier)

• v0, v1, v2, etc. (variables)

  Here is an example of a sentence:

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

Here not x is shorthand for x nand x -- the actual sentence would use (v1*v1*v1 + v2*v2*v2 = v3*v3*v3) nand (v1*v1*v1 + v2*v2*v2 = v3*v3*v3), because x nand x = not (x and x) = not x.

This states that for every combination of three natural numbers v1, v2, and v3, it is not the case that v1³ + v2³ = v3³ (which would be true because of Fermat's Last Theorem, except for the fact that it would get 0^3+0^3=0^3).

Unfortunately, as proved by Gödel, it is not possible to determine whether or not a sentence in number theory is true.

It is possible, however, if we restrict the set of natural numbers to a finite set.

So, this challenge is to determine whether or not a sentence of number theory is true, when taken modulo n, for some positive integer n. For example, the sentence

forall v0 (v0 * v0 * v0 = v0)

(the statement that for all numbers x, x³ = x)

Is not true for ordinary arithmetic (e.g. 2³ = 8 ≠ 2), but is true when taken modulo 3:

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

Input and output format

The input is a sentence and positive integer n in any "reasonable" format. Here are some example of reasonable formats for the sentence forall v0 (v0 * v0 * v0 = v0) in number theory 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)"

Input can be from stdin, a command line argument, a file, etc.

The program can have any two distinct outputs for whether the sentence is true or not, e.g. it could output yes if it's true and no if it's not.

You do not need to support one variable being the subject of a forall twice, e.g. (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0)). You can assume that your input has valid syntax.

Test cases

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

This is code-golf, so try to make your program as short as possible!

• Jo King: Are variable names always in the format v number?
• pommicket: @JoKing They can if you want them to be- you can use var number, or even just 1 + number (so 1 would be v0, 2 would be v1, etc.)
• pommicket: @JoKing You should allow for (theoretically) an infinite number of variables. It's okay if the maximum number of variables is bounded by the maximum size of an integer, but you shouldn't have such a low limit. You can choose one of the other input formats if this is a problem for you.
• pommicket: @UnrelatedString Sure, so long as they can be arbitrarily long.
• Mr. Xcoder: Can one use 'v number instead of v number' if we choose the prefix-syntax option?

Answer 1

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

Try it online!

Takes input as the nested prefix-syntax, with f instead of forall and n instead of nand:

[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]

• pommicket: Right now it's outputting Python code, but it should have two distinct outputs for if the sentence is true or false. You can use print(eval(g(*input()))).
• TFeld: @LeoTenenbaum Yeah, I had that on the first version, but forgot to add it back in after golfing

Answer 2

APL (Dyalog Unicode), 129 bytes^SBCS

{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(×ばつ⍲',⊂'0=⍺⍺|-')∇z}

Try it online!

Takes a prefix syntax tree as in TFeld's python answer, but using an integer encoding. The encoding is

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

and each variable is assigned a number starting from 8. This encoding is slightly different from the one used in the ungolfed version below, because I tweaked it while golfing the code.

The task involves only two inputs (the AST and the modulo), but writing it as an operator instead of a function avoids mentioning the modulo many times (as it is always carried over recursive calls).

Ungolfed with comments

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

Try it online!