The goal of this chapter is to learn some of the history of Effective Computability and understand the two most important models of computation: the Turing Machine and the Lambda Calculus
After completing this chapter one should understand:
- Lambda Calculus as a formal system for expressing programs
- the substitution model for function application
- applicative vs normal evaluation order
- Church encoding for booleans and numerals
- The Rise and Fall and Rise of Functional Programming
- "Propositions as Types" by Philip Wadler
- David Hilbert
- Entscheidungsproblem
- Kurt Gödel
- Gödel's incompleteness theorems
- Gödel's General recursive function
- Alonzo Church
- Lambda calculus
- Alan Turing
- The Turing Machine
- Church–Turing thesis
- Chapter1. All You Need is Lambda - Christopher Allen, Julie Moronuki - Haskell programming from first principles
- Applicative vs Normal evaluation form
- Normal, Applicative and Lazy Evaluation
- 1.1.5 The substitution model for procedure application
- Church encoding
Optional:
- Fixed-point combinators in JavaScript: Memoizing recursive functions
- SKI combinator calculus with details
- SKI combinator calculus
- SKI combinator calculus
- Book Exercises (Chapter1. All You Need is Lambda)
- See folder
Exercises - Lambda calculi in JS