12
\$\begingroup\$

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 v13 + v23 = v33 (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, x3 = x)

Is not true for ordinary arithmetic (e.g. 23 = 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 , so try to make your program as short as possible!

\$\endgroup\$
  • 1
    \$\begingroup\$ Are variable names always in the format v number? \$\endgroup\$ – Jo King Aug 15 '19 at 1:20
  • 1
    \$\begingroup\$ @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.) \$\endgroup\$ – pommicket Aug 15 '19 at 1:21
  • 1
    \$\begingroup\$ @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. \$\endgroup\$ – pommicket Aug 15 '19 at 1:29
  • 1
    \$\begingroup\$ @UnrelatedString Sure, so long as they can be arbitrarily long. \$\endgroup\$ – pommicket Aug 15 '19 at 3:51
  • 1
    \$\begingroup\$ Can one use 'v number instead of v number' if we choose the prefix-syntax option? \$\endgroup\$ – Mr. Xcoder Aug 15 '19 at 10:40
3
\$\begingroup\$

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"]]]
| improve this answer | |
\$\endgroup\$
  • \$\begingroup\$ 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()))). \$\endgroup\$ – pommicket Aug 15 '19 at 12:09
  • \$\begingroup\$ @LeoTenenbaum Yeah, I had that on the first version, but forgot to add it back in after golfing \$\endgroup\$ – TFeld Aug 15 '19 at 13:31
1
+200
\$\begingroup\$

APL (Dyalog Unicode), 129 bytesSBCS

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

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!

| improve this answer | |
\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.