숫자 이론 (우리의 목적을 위해) 의 문장 은 다음과 같은 일련의 기호입니다.
0
그리고'
(후임자)-후속 수단+1
, 그래서0'''' = 0 + 1 + 1 + 1 + 1 = 4
+
(더하기)와*
(곱하기)=
(동일)(
그리고)
(괄호)- 논리 연산자
nand
(a nand b
isnot (a and b)
) forall
(범용 정량 자)-
v0
,v1
,v2
, 등 (변수)다음은 문장의 예입니다.
forall v1 (forall v2 (forall v3 (not (v1*v1*v1 + v2*v2*v2 = v3*v3*v3))))
여기 not x
에 대한 약칭 x nand x
이 있습니다 (v1*v1*v1 + v2*v2*v2 = v3*v3*v3) nand (v1*v1*v1 + v2*v2*v2 = v3*v3*v3)
. 왜냐하면 실제 문장이 사용 하기 때문 x nand x = not (x and x) = not x
입니다.
세 자연수의 모든 조합에 대한 것으로이 상태 v1
, v2
그리고 v3
, 그것은 V1하는 경우가 아니라 3 + V2 3 = V3 3 (그것을 얻을 것이라는 사실을 제외하고, 때문에 페르마의 마지막 정리의 사실이 될 것이다 0 ^ 3 + 0 ^ 3 = 0 ^ 3).
불행히도, 고델 (Gödel)에 의해 증명 된 바와 같이, 수 이론의 문장이 참인지 아닌지를 판단하는 것은 불가능합니다.
그것은 이다 우리는 유한 집합으로 자연수의 집합을 제한 할 경우, 그러나, 수.
따라서이 과제는 모듈러스를 취했을 때 n
어떤 양의 정수에 대해 수론의 문장이 참인지 아닌지를 결정하는 것 n
입니다. 예를 들어, 문장
forall v0 (v0 * v0 * v0 = v0)
(모든 숫자 x, x 3 = x에 대한 진술 )
일반적인 산술에는 해당되지 않지만 (예 : 2 3 = 8 ≠ 2) 모듈로 3을 사용하는 경우 에는 적용됩니다.
0 * 0 * 0 ≡ 0 (mod 3)
1 * 1 * 1 ≡ 1 (mod 3)
2 * 2 * 2 ≡ 8 ≡ 2 (mod 3)
입력 및 출력 형식
입력은 n
“합리적인”형식 의 문장과 양의 정수 입니다. 다음은 forall v0 (v0 * v0 * v0 = v0)
수론 모듈로 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)"
입력은 stdin, 명령 행 인수, 파일 등이 될 수 있습니다.
이 프로그램은 문장이 출력 할 수 예, 사실 여부에 대해 어떤 두 가지 출력을 할 수 있습니다 yes
그것은 사실 경우 no
가 아니라면.
forall
예를 들어 , 두 번의 주제가되는 하나의 변수를 지원할 필요는 없습니다 (forall v0 (v0 = 0)) nand (forall v0 (v0 = 0))
. 입력에 유효한 구문이 있다고 가정 할 수 있습니다.
테스트 사례
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
이것은 코드 골프 이므로 가능한 한 프로그램을 짧게 만드십시오!
답변
파이썬 2 , 252 236 바이트
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()))
와 중첩 프리픽스 구문으로서 입력을 받아 f
대신 forall
하고 n
대신 nand
:
[3, ["f", "v0", ["=", ["*", "v0", ["*", "v0", "v0"]], "v0"]]]
답변
APL (Dyalog Unicode) , 129 바이트 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}
TFeld의 python answer 에서와 같이 접두어 구문 트리를 사용하지만 정수 인코딩을 사용합니다. 인코딩은
plus times nand eq forall succ zero ← 1 2 3 4 5 6 7
각 변수에는 8부터 시작하는 숫자가 할당됩니다.이 인코딩은 코드를 골프를 타는 동안 수정했기 때문에 아래의 ungolfed 버전에서 사용 된 것과 약간 다릅니다.
이 작업에는 두 개의 입력 (AST 및 모듈로) 만 포함되지만 함수 대신 연산자로 입력하면 모듈러스를 여러 번 언급하지 않아도됩니다 (항상 재귀 호출을 통해 수행됨).
주석이 달린 골퍼
⍝ 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
}