I am currently going through Philip Walder's ["Proposition as Types"](http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf) and a passage of the introduction has struck me:



> 
> for each way to simplify a proof
>  there is a corresponding way to evaluate a program
> 
> 
> 


What does *simplify a proof* means here? I have searched in my logic textbook and on the Internet but surprisingly enough I could not find any direct, informal explanation.



What does "simplification of proofs as evaluation of programs" mean?
There are two inference rule of propositional logic involving implication (which I write using $\to$ instead of $\Rightarrow$):


1. The *introduction* rule says that we can prove $A \to B$ if we derive $B$ from the assumption $A$ (there are brackets around $[A]$ because $A$ here is a "temporary" assumption which is "discharged" by $A \to B$):
$$\frac{\begin{matrix}[A]\\ \vdots \\ B\\\end{matrix}}{A \to B}$$
2. The *elimination* rule says that from $A \to B$ and $A$ we may derive $B$:
$$\frac{A \to B\qquad A}{B}$$


Now consider what happens if we prove $A \to B$ in the elimination rule using the introduction rule. We get a derivation that looks like this:
$$\frac{\displaystyle
 \frac{\begin{matrix}[A]\\ \vdots \\ B\\\end{matrix}}{A \to B} \qquad
 \frac{\begin{matrix} \\ \\ \vdots \\\end{matrix}}{A}
 }{B}$$
In words this proof would go as follows:


* Show that $B$ follows from the assumption $A$, thereby conclude $A \to B$.
* Prove $A$.
* Combine the previous two steps to conclude $B$.


We can transform the proof into a simpler one: step one already contains the proof of $B$, except that it relies on the assumption $A$. But we can get rid of the assumption by replacing it with the proof of $A$ whenever it gets used. So our new proof will look like this:
$$
\begin{matrix}\vdots \\ A\\ \vdots \\ B\\\end{matrix}
$$
This is what is meant by proof *simpliication*. It is a transformation of a proof in which an introduction rule is immediately followed by an elimination rule. Another example is this:
$$\frac{\displaystyle
\frac{A \qquad B}{A \land B}
}
{A}
$$
There is no point in first proving $A \land B$ and then forgetting about the proof of $B$ – we can just directly go for the upper-left part, which is a proof of $A$.


These proof transformations correspond precisely to computation steps in a functional programming language. The first example is the $\beta$-rule
$$(\lambda x : A \,.\, e\_1) \, e\_2 \leadsto e\_1[e\_2/x]$$
which reads: "a function mapping $x$ of type $A$ to an expression $e\_1$ of type $B$ applied to an expression $e\_2$ of type $A$ equals the expression $e\_1$ with $x$ replaced by $e\_2$". By the Curry-Howard correspondence $x$ is the assumption $A$, $e\_1$ is the proof that $B$ follows from $A$, $\lambda x : A \,.\, e\_1$ is the proof of the implication $A \to B$, $e\_2$ is the proof of $A$, and $e\_1[e\_2/x]$ is the "simplified" (logicians say "reduced" or "normalized") proof of $B$ in which the assumption $x$ was replaced by $e\_2$.


The second example corresponds to the rule for computng the first component of a pair:
$$\pi\_1 \langle e\_1, e\_2 \rangle \leadsto e\_1.$$


