2 minute read

Partial FunctionsPermalink

System T, F are total languages.

PCF (Programming Language for Computable Functions) (By Gordon Plotkin) - E. col. of partial languages.

Idea: Extending the theory of computability to HIGHER TYPE. Standard computability courses only talk about computation over N, but nothing beyond that.

e.g. gcd is defined by the following (recursive) equations:

gcd(m,n)=m if m=ngcd(m,n)=gcd(mn,n) if m>ngcd(m,n)=gcd(m,nm)ow

We can transcribe the above in a real programming language (ML, Haskell) in an evident way.

We call it “Recursive function” in a typical course - it is using recursion.

Then the next typical topic would be about “stack”.

Recursion has nothing to do with the stack. (One obvious example is flip-flop with two NOR gates.)

Better idea (correct idea): simultaneous equations in the variable gcd. Solve for gcd!

We want: gcd s.t. gcd=G(gcd) where G is the function of definition my gcd. We are looking for a FIXED POINT.

The equations only make sense (solution exists) with computable partial functions.

Recursive Programs in Plotkin PCFPermalink

( means partial functions)

τ:=nat|τ1τ2 e:=x|z|s(e)|ifz(e,e2,x.e1)|λx:τ.e|e1(e2)|fix{τ}(x.e)(written as fix x is e)

fix is called general recursion.

Examples of equations:

gcd(m,n)=gcd(m,n) gcd(m,n)=1+gcd(m,n)

Both equations have solutions (only in the context of partial function, 2nd won’t work for total setting becuase it’s like x=x+1): totally undefined function!

fix x is e is the solution to x=ex

τ=fix{τ}(x.x) ( is called bottom (the least element in a certain pre-order)) (This is undefined, which mean it has no value)

Then we can define gcdfix{natnat}(x.G(x)) (Note: There is not occurrence of gcd on the right hand side! It is solving a fixed point equation!)

Why do we have partial functionsPermalink

  1. Challenge: Try to define gcd in GodelsT (using products, sums, subtractions, equality/ inequality). This is hard! Because you must bake the termination proof into the code (not your head).
  2. Blum Size Theorm: Fix an expansion factor, say 22n, there is a function f:NN whose shortest program in T (or any total language) is 22n longer than it’s code in PCF.

StaticsPermalink

Γ,x:τe:τΓfix{τ}(x.e):τ

(Note: All τ’’s are the same! The crucial thing: you assume what you are trying prove!) In other words, you assume what you are trying to prove, and you are showing that assumption is tenable (show that nothing contradicts that fact), then it just is the case! I don’t show anything absolutely outright. I just assume what I am trying to prove and consider that sufficient to be true because I don’t care if thing diverges like in partial maps.

DynamicsPermalink

fix{τ}(x.e)[fix{τ}(x.e)/x]e

(It’s just “F[F/x]e”) It’s called “unrolling recursion”.

There is no stack in the dynamics! :)

EquivalencePermalink

Main theormPermalink

If e:τ then eτe

Fixed point inductionPermalink

For admissible relations only:

To show:

fix(x.e)τfix(x.e)

It’s suffice to show:

n0 fix(n)(x.e)τfix(n)(x.e)

(fix(n) means the n-fold unrolling of the fix)

Comments