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 :
I.2 - / -conversions, -reduction
<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 }})"/>
Or… in terms of alligators (an idea by Victor Bret)
Eating process ≡ -reduction
-reduction
-reduction
-conversion
-conversion
old alligators ≡ parentheses
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 ?
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
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.