Gödel arithmetization applet details

The arithmetization applet 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 that WF1 ∧ WF2 ∧ ...∧ WFn becomes ¬(WF1 ⇒(WF2 ⇒(...⇒ ¬WFn)...)
• ∃v WF(v) ≡ ¬∀v ¬WF(v)
• x<y ≡ ∃z (y=x+z')

Haskell is a functional programming language, and so as you might expect there are plenty of functions defined in a typical Haskell program. How are these translated into the sparse arithmetical language, which has no notion of a function? A simple function such as f(x)=x² could simply be replaced by its result every time it occured, but this would not make sense for the complicated functions which occur in a typical program. The solution is via Gödel's beta function, defined as β(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 N_f on the size of parameter of an function f(p) then there exist numbers Y_f,Z_f such that f(p)=β(Yf,Zf,p) for all p<N_f. Note that it is not necessary to calculate what Y_f, Z_f 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 N_f=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.

Since the idea of this program is to convert to statements of integer arithmetic, the 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

To simplify the implementation, these rules are added as predefined conditions, rather than being written in Haskell.

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.

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

Functions in Haskell are generally defined in a recursive manner, rather than using loops. Thus f(n)=2ⁿ might be defined as

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)

The applet only implements those parts of Haskell that are necessary to deal with the Godel2.hs program, so it is very restricted compared to a typical Haskell implementation. If you want to try out the applet on other programs then you should take note of the following information:

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.