# -Calculus & Curry-Howard correspondence ###### Younesse Kaddar

## I. -Calculus

1) Definition 2) , -conversions and -reduction 3) Alligators

## II. Fixed-point combinator

1) Turing-completeness of -calculus 2) Curry and Turing combinators 3) Curry-Howard correspondence

## I.1 - -Calculus : definition

Let be a fixed set of variables

expressions :

: <p align="center"></p> the smallest set of functions such that

• Application :
• -abstraction :
> **NB** : *Such a set exists* : apply Knaster-Tarski to the following monotonic function in the complete lattice , where

## I.2 - / -conversions, -reduction

-conversion : :

<img src="https://latex.codecogs.com/gif.latex?\lambda x. u= _\alpha \lambda y. (\underbrace{u[x :=y]}_{\text{all instances of in are replaced by }})"/>

> ![/!\\](warning_icon.svg ) OR and , as illustrated by these examples : > > || > |-|- > |
-reduction : :

-conversion : : *If does not appear free in * :

## Or… in terms of alligators (an idea by Victor Bret)

![Alligator family](families_3.png )

### Eating process ≡ -reduction

![](eating_1.png )
⇓ ![](eating_3.png )
![](eating_4.png ) ⟹ ![](eating_5.png )
⇓ ![](eating_6.png )
![](eating_7.png ) ⟹ ![](eating_9.png )
⇓ ![](eating_10.png )

## -reduction

1. ![](eatingrule_2.png )
⇓ 2. ![](eatingrule_3.png )

## -reduction

3. ![](eatingrule_4.png )

## -conversion

1. ![](eatingrule_4.png )
⇓ 2. ![](colorrule_1.png )

## -conversion

3. ![](colorrule_2.png )

## old alligators ≡ parentheses

![](old_1.png )
⇓ ![](old_3.png ) ⟹ ![](old_4.png )

## II.1 - Turing-completeness of -calclus

Church Numerals :

• Constant function : <p align="center"></p>

• Successor function S :

• Projection function :

## II.1 - Turing-completeness of -calculus

Operators:

• Composition operator : -abstraction

Now, what about :

• the primitive recursion operator :

• the minimisation operator :

?

## II.1 - Turing-completeness of -calculus

If

then :

But… what about recursion ?

![](descartes.png )
![](escher-hands.gif )

## II.2 - Fixed-point combinators

Astounding fact : each -term actually has a fixed point !

and there even exist fixed-point combinators :

The Curry combinator :

: <p align="center"></p>

The Turing combinator :

: <p align="center"></p>

## II.3 - Curry-Howard isomorphism

It’s great, but… you can’t do that in Haskell (for example) :

y :: (a -> a) -> a
y = \f -> (\x -> f (x x)) (\x -> f (x x))


Occurs check: cannot construct the infinite type: r0 ~ r0 -> t
Expected type: r0 -> t
Actual type: (r0 -> t) -> t

![WHY?](rage-why.png )

Because Haskell (and other functional programming languages such as OCaml, Lisp, Clojure, etc…) is strongly typed.

What is a type ? :

: A type is a property of a program.

Ex :

• the type of the -term can be be thought as “Integer” : int.
• the program takes a natural number and produces another natural number : its type is

The CURRY-HOWARD CORRESPONDENCE :

Proofs can be represented as programs (-terms), and the formulas it prove are the types for the program

Intuitionistic implicational natural deduction Lambda calculus type assignment rules
<p align="center"></p> <p align="center"></p>
<p align="center"></p> <p align="center"></p>
<p align="center"></p> <p align="center"></p>

From a logical standpoint, the combinator corresponds to the Curry paradox.

“If this sentence is true then I am an alligator” is true : why ?

Let’s suppose that the sentence is true : it must be shown that I am an alligator.

But since the sentence is true, modus ponens can be applied, which yields the conclusion.