Difference between revisions of "Lambda Calculus"
Line 1: | Line 1: | ||
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]]<ref>{{:Video/Dana S. Scott Lambda Calculus, Then and Now}}</ref>. | 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]]<ref>{{:Video/Dana S. Scott Lambda Calculus, Then and Now}}</ref>. | ||
[[wikipedia:Lambda calculus|Lambda calculus]] is a formal language that can serve as a foundation of all general purpose programming languages. It is also a kind of [[Universal Data Abstraction]]. Essentially, a lambda calculus is a recursively defined dictionary with just three branches of possible values. | |||
{| class="wikitable" | |||
|- | |||
! Syntax !! Name !! Description | |||
|- | |||
| ''x'' || Variable || A character or string representing a parameter or mathematical/logical value. | |||
|- | |||
| (λ''x''.''M'') || Abstraction || Function definition (''M'' is a lambda term). The variable ''x'' becomes [[Free variables and bound variables|bound]] in the expression. | |||
|- | |||
| (''M'' ''N'') || Application || Applying a function to an argument. ''M'' and ''N'' are lambda terms. | |||
|} | |||
==Lambda Calculus expressed in Backus-Naur form== | |||
=Relevant Learning Material= | |||
A nice video<ref>{{:Video/Lambda Calculus - Computerphile}}</ref> tutorial by [[Hutton Graham]] is available. An interactive web page to illustrate the working process of [[Lambda calculus]] can be found here: [https://opendsa-server.cs.vt.edu/OpenDSA/Books/PL/html/Syntax.html Syntax of the Lambda Calculus]. | |||
<noinclude> | |||
=References= | |||
<references/> | |||
==Related Pages== | |||
[[Category:Programming Language]] | |||
</noinclude> | |||
=[[Lambda Calculus]] and [[Abstract Syntax Tree]]= | =[[Lambda Calculus]] and [[Abstract Syntax Tree]]= |
Revision as of 14:16, 19 May 2022
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[1].
Lambda calculus is a formal language that can serve as a foundation of all general purpose programming languages. It is also a kind of Universal Data Abstraction. Essentially, a lambda calculus is a recursively defined dictionary with just three branches of possible values.
Syntax | Name | Description |
---|---|---|
x | Variable | A character or string representing a parameter or mathematical/logical value. |
(λx.M) | Abstraction | Function definition (M is a lambda term). The variable x becomes bound in the expression. |
(M N) | Application | Applying a function to an argument. M and N are lambda terms. |
Lambda Calculus expressed in Backus-Naur form
Relevant Learning Material
A nice video[2] tutorial by Hutton Graham is available. An interactive web page to illustrate the working process of Lambda calculus can be found here: Syntax of the Lambda Calculus.
References
- ↑ Scott, Dana (Aug 24, 2012). Dana S. Scott Lambda Calculus, Then and Now. local page: princetonacademics.
- ↑ Graham, Hutton (January 28, 2017). Lambda Calculus - Computerphile. local page: Computerphile.
Related Pages
Lambda Calculus and Abstract Syntax Tree
All decision making procedures can be represented into three major kinds of branching:
Technical Term | Abstraction types | Symbolic representation | Description |
---|---|---|---|
-conversion | Variable | Naming abstraction | A collection of symbols (names) that act as unique identifiers. |
-reduction | Substitution rule | Function evaluations | A template or executable function that can be reused in multiple contexts. |
-composition | Sequential composition | Function composition | The sequential/structural arrangements of known representable data. |
These three types also relate to the reason why Kan Extension is universal. To understand the intricate mechanisms of Lambda calculus, and why and how this simple language can be universal, please read this page:Dana Scott on Lambda Calculus.
Video Playlist
- For people who wants to learn about Lambda Calculus, this video playlist[1] would be very useful.
References
Related Pages
- 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
- Paper/History of Lambda-calculus and Combinatory Logic
- Paper/Outline of a Mathematical Theory of Computation
- 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
- 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