Lambda Calculus

Lambda calculus is a universal/Turing-complete language specification invented by Alonzo Church, that is considered to be mathematically elegant, due to its small size. Almost all text-based formal languages are defined using Lambda calculus. To learn about its history, it is recommended to watch this video by Dana Scott.

Lambda Calculus and Abstract Syntax Tree

All decision making procedures can be represented into three major kinds of branching:

1. [[$\alpha$ conversion]]:Naming Abstraction
2. [[$\beta$ conversion]]:Branching Abstraction
3. [[$\gamma$ conversion]]:Typing Abstraction

This three types also relates to the reason why Kan Extension is universal.

References

Related Pages

D

• Dana Scott
• Dana Scott on Lambda Calculus

J

• John Shutt

L

• Lambda Calculus
• Lectures/"An Introduction to Combinator Compilers and Graph Reduction Machines" by David Graunke
• Lectures/"Functional distributed systems beyond request/response" by Melinda Lu

P

• Paper/History of Lambda-calculus and Combinatory Logic
• Paper/Outline of a Mathematical Theory of Computation

Q

• Quote/Separation of Church and state

T

• Thesis/Fexprs as the basis of Lisp function application or $vau : the ultimate abstraction

V

• Video/"An Introduction to Combinator Compilers and Graph Reduction Machines" by David Graunke
• Video/"Functional distributed systems beyond request/response" by Melinda Lu
• Video/5 Simple Steps for Solving Any Recursive Problem
• Video/Category Theory for the Working Hacker by Philip Wadler

V cont.

• Video/Dana S. Scott Lambda Calculus, Then and Now
• Video/Dana S. Scott: Seventy Years Using Fixed Points
• Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 1) - λC 2018
• Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 2) - λC 2018
• Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 3) - λC 2018
• Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 4) - λC 2018
• Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 5) - λC 2018
• Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 6) - λC 2018
• Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 1 of 5 - λC 2017
• Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 2 of 5 - λC 2017
• Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5 - λC 2017
• Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 4 of 5 - λC 2017
• Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5 - λC 2017
• Video/Daniel Beskin - Category Theory as a Tool for Thought - Lambda Days 2020

V cont.

• Video/Daniel Beskin- Category Theory as a Tool for Thought- λC 2019
• Video/Foundations of Programming Languages: Typed and Untyped Lambda-Calculus - Paul Downen - OPLSS 2018
• Video/Hey Underscore, You're Doing It Wrong!
• Video/Lambda Calculus - Computerphile
• Video/Lambda Calculus - Fundamentals of Lambda Calculus & Functional Programming in JavaScript
• Video/Prof. Dana Scott - Geometry Without Points
• Video/Programming Loops vs Recursion - Computerphile
• Video/Some analogies between arithmetic and topology - Tony Feng
• Video/Steven Syrek - Category Theory for People who Can't be Bothered to Learn It (Part 1) - λC 2018
• Video/Steven Syrek - Category Theory for People who Can't be Bothered to Learn It (Part 2) - λC 2018
• Video/Stochastic Lambda-Calculus
• Video/Unleashing Algebraic Metaprogramming in Julia with Metatheory.jl JuliaCon2021
• Video/Why Elixir Matters: A Genealogy of Functional Programming