Functional Programming, Haskell, Computer Science, Lambda Calculus, Algorithms.
Calculus of Constructions (Morte): λ (a : Nat) -> λ (b : Nat) -> λ (P : *) -> λ (S : P -> P) -> λ (z : P) -> a P S (b P S) As you can see, the later is much simpler. 3. A new option: rethink the λ-calculus? So, extending the Abstract Algorithm to cover all lambda terms ruins its efficiency, and