Gödel arithmetization applet details
Godel3
translates a program written in Haskell into the language of arithmetic formulae. Specifically it translates a statement involving Haskell functions (such as y=f(x)) into a number representing an arithmetic formula. Note that whilst this is similar to the action of a compiler, in a sense it is simpler, since both the input and the output express a collection of relationships between variables.
The arithmetic formulae are expressed in terms of the system described in Gödel numbering applet. This is a sparse system, and does not include the symbols ∧, ∨ ∃
or <
. These can be defined in terms of the given symbols in the following way:
WF1 ∨ WF2 ≡ (¬WF1) ⇒ WF2
WF1 ∧ WF2 ≡ ¬(WF1 ⇒(¬ WF2))
Note thatWF1 ∧ WF2 ∧ ...∧ WFn
becomes¬(WF1 ⇒(WF2 ⇒(...⇒ ¬WFn)...)
∃v WF(v) ≡ ¬∀v ¬WF(v)
x<y ≡ ∃z (y=x+z')
Functions
Some related reading |
---|
This book describes the construction of a computer based proof of Gödel's incompleteness theorem, based on the LISP programming language |
My Review of Metamathematics, machines, and Gödel's proof |
β(a,b,x)=b % (1+(x+1)a)
where %
is the modulo operator. Note that this function can be translated into arithmetic statements as follows:
Suppose we have vx=β(a,b,vp)
. This is equivalent to
∃q ∃v (v=(1+(vp+1)*a)∧ b=q*v+vx ∧ vx<v)
Now for the clever bit. It is possible to show that given a sequence of natural numbers a1 .. an
there exist numbers Y and Z such that ai=β(Y,Z,i)
for all i in [0..n]. So if you put a limit Nf on the size of parameter of an function f(p) then there exist numbers Yf,Zf such that f(p)=β(Yf,Zf,p)
for all p<Nf. Note that it is not necessary to calculate what Yf, Zf actually are, it is enough to state that such numbers exist. Then f can be replaced by a corresponding expression using Gödel's beta function, both for the definition of f and when it is used as part of an expression. This applet will typically deal with an expression such as y=f(x)
, for which we can put Nf=x+1.Hence for the expression y=f(x)
, where f(p) is defined as some expression expr(p) we get the code:
∃Nf,Yf,Zf (∀vp,p ((vp=p ∧ vp <Nf)
⇒ ∃vr (vr=βf(vp) ∧ (vr=expr(p)))) ∧ (y=βf(x) ∧ x<Nf ))
The function f will be defined in terms of other functions, but their parameters will depend on x, and so will have a limit. Thus, going through the definitions of each of the functions we can see that there will be a bound to the parameters, and so the functions can be expressed in terms of the Gödel β function.
Data Types and Operators
Integer
type is essentially the only one implemented, although pairs (Integer,Integer)
and lists [Integer]
are also allowed. Note that the arbitrary size Integer
is used, rather than Int
, since the arithmetic formulae apply to any size integer. This does mean that the Haskell code has had toInteger
and FromInteger
added where an Int
is required, so that it will compile in a normal Haskell environment. (This implementation ignores these functions).
Pairs of integers are implemented using the function J(a,b)=(a+b)2+a+1
. This is a 1-to-1 function, and so means that two integers, (Integer,Integer)
, can be represented as one. Repeated use of this function means that a number of integers can be combined into one, and this is used to convert several parameters of a function into a single one. Lists, [Integer]
, are dealt with a bit differently. It isn't actually necessary to specify how they are implemented, all that is needed is to specify what rules operators (:)
and !!
and functions must obey. Thus we have
(x:y)!!0=x
(x:y)!!n'=y!!n
length []=0
length (x:y)=(length l)'
tail (x:y)=y
The operators *, `div`, `mod`, +, -, ==, /=, <, >, <=, >=, ||, &&
convert fairly directly into their equivalents in arithmetic formulae.
Boolean expressions may occur as the result of relational operators, but boolean variables or functions cannot be defined.
Program structures
if, case
and let
statements are implemented. These are dealt with as follows:
v=if boolexp then expr1 else expr2
becomes(boolexp⇒v=expr1) ∧ (¬boolexp⇒v=expr2)
-
v=let {x=expr1}in expr2
becomes∃x (x=expr1 ∧ v=expr2)
(where expr2 is an expression involving x) v= case expr of {
c1->expr1
..
cn->exprn;
_->defexpr;}
becomes
∃x (x=expr ∧ (x=c1 ⇒ v=expr1) ∧.. ∧ (x=cn ⇒ v=exprn) ∧(((¬(x=c1))∧..∧(¬(x=cn)))⇒v=defexpr)
An example arithmetization of a recursive function
f n =if n==0 then 1 else 2*(f (n-1))
Using the beta function we can then convert m=2n
into:
∃ Yf,Zf (m=β(Yf,Zf,n) ∧ (0<i<m ⇒ β(Yf,Zf,i)=2*β(Yf,Zf,i-1))∧β(Yf,Zf,0)=1)
Notes of the subset of Haskell implemented
The program should be of the form MODULE name WHERE {function definitions}
. The layout rule is not implemented - you need to have all the {'s and semicolons. There may also be an IMPORT statement before the function definitions, although this is ignored by the program. Note that if a function name is used without being defined then the program looks for a function with that name with a ' added. This means that a function such as shift
can be imported from another module for use when the program is run in a normal Haskell environment, whilst the applet will find the function shift'
instead.
Each function must have a function type declaration before it is used, and have a separate function binding. Recursive functions may be used, but mutual recursion is not allowed. The program doesn't do any form of pattern matching, and it is not possible to define new data types.
if, case
and let
are the only statements which can be used. where
is not implemented, and neither are do
or monadic programming.