# Recursive Programs

# Partial Functions

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 $\mathbb{N}$, but nothing beyond that.

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

\[gcd(m,n) = m\ if\ m=n\\ gcd(m,n) = gcd(m-n,n)\ if\ m>n\\ gcd(m,n) = gcd(m,n-m) 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 PCF

($\rightharpoonup$ means *partial functions*)

\(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=e_x$

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

Then we can define \(gcd \triangleq fix\{nat\rightarrow nat\}(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 functions

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

## Statics

\[\frac{\Gamma,x:\tau\vdash e:\tau}{\Gamma\vdash fix\{\tau\}(x.e):\tau}\](Note: All $\tau$’’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.

## Dynamics

\[\frac{}{fix\{\tau\}(x.e)\mapsto[fix\{\tau\}(x.e)/x]e}\](It’s just “$F\mapsto[F/x]e$”) It’s called “unrolling recursion”.

*There is no stack in the dynamics! :)*

## Equivalence

### Main theorm

\[If\ e:\tau\ then\ e\sim_{\tau}e\]### Fixed point induction

For **admissible relations only**:

To show:

\[fix(x.e)\sim_\tau fix(x.e')\]It’s suffice to show:

\[\forall n\ge 0\ fix^{(n)}(x.e)\sim_\tau fix^{(n)}(x.e')\](\(fix^{(n)}\) means the n-fold unrolling of the fix)