Tutorial 8

Exercise 3

Let $P$ be the SFUN program:

$$\begin{array}{rl}{f}_1& =f_1+1\\ f_2(x)& =1\\ f_3(x)& =x\ast x\end{array}$$

More formally, we can define $f_1$:

• Since $ϵ(f_1)=\text{int}$, then ${⊢}_{ϵ}{f}_1:\text{int}$ and ${⊢}_{ϵ}{f}_1+1:\text{int}$.
• Since $ϵ(f_2)=\text{int}\to \text{int}$. then $x:\text{int}{⊢}_{ϵ}{f}_2(x):\text{int}$ \text{..}$

And $ϵ$ is an environment where:

$$\begin{array}{r}ϵ(f_1)=\text{int}\\ ϵ(f_2)=\text{int}\to \text{int}\\ ϵ(f_3)=\text{int}\to \text{int}\end{array}$$

1. Show $f_2(0)$ is typeable.

$$\frac{t_{ϵ}0=\text{int}}{t_{ϵ}{f}_2(0):\text{int}}ϵf(2)=\text{int}\to \text{int}$$

Exercise 4

Prove by induction that $\text{sumodd }n=n^2$. Base Case: $x=1$ then $1$ [FINISH THIS]