#triplet #recursion #universality [[Lambda calculus]] ([[Lambda Calculus|λ-Calculus]]) is a formal system in mathematical logic and computer science that was developed by [[Alonzo Church]] in the 1930s. It is a universal model of computation, meaning that any computable function can be represented and evaluated within the lambda calculus. At its core, lambda calculus is based on the concept of functions and function application. It uses lambda expressions, which are anonymous functions that can take one or more arguments and return a result. These expressions consist of three elements: variables, abstraction, and application. Variables in lambda calculus are placeholders for values or arguments. Abstraction allows the creation of lambda expressions by binding variables within a function. The syntax for abstraction is λx.M, where x represents the variable being bound and M represents the body of the function. The most fundamental operation in lambda calculus is application. It allows the evaluation of a function with specific arguments by replacing variables in an expression with those arguments. The syntax for application is (λx.M) N, where (λx.M) represents a lambda expression and N represents an argument or value to be substituted into it. # The Ultimate Functional Model Lambda calculus has no built-in data types or constants; everything is expressed through functions and their applications. This simplicity makes it an ideal model for studying computation at its most fundamental level. In fact, lambda calculus forms the basis of functional programming languages like Haskell and forms an important part of modern computer science theory. ## Three Kinds of Abstractions Please talk about Lambda Calculus' alpha, beta and eta abstractions/conversions Lambda Calculus consists of three fundamental operations: alpha conversion, beta reduction, and eta conversion. 1. [[Alpha Conversion]]: Alpha conversion is a renaming operation that allows us to change the names of bound variables in a lambda expression without altering its meaning. In Lambda Calculus, the names of variables are not important; only their scope matters. For example, given the lambda expression (λx.x), we can perform an alpha conversion and rename the bound variable x to y, resulting in (λy.y). Both expressions represent the same function that takes an argument and returns it unchanged. 2. [[Beta Reduction]]: Beta reduction is the process of applying a lambda expression to an argument by substituting occurrences of bound variables with their corresponding values. It represents function application in Lambda Calculus. For example, given the lambda expression ((λx.x) y), we can perform a beta reduction and substitute y for x, resulting in y. The result is obtained by applying the identity function (λx.x) to the argument y. 3. [[Eta Conversion]]: Eta conversion is a rule that allows us to eliminate unnecessary abstraction from a lambda expression. It states that if we have a lambda expression (λx.f x), where f is another function that uses its argument exactly once, we can simplify it to f. This rule captures the concept of extensionality in Lambda Calculus, where two functions are considered equal if they produce identical results for all possible arguments. These three operations – alpha conversion, beta reduction, and eta conversion – form the basis for manipulating lambda expressions in Lambda Calculus. They allow us to reason about functions and computations purely based on their structure and behavior without relying on any specific implementation details or programming language constructs. ## Define Recursion in Lambda Calculus One notable feature of lambda calculus is its ability to define recursive functions using fixed-point combinators. These combinators allow self-reference within a function definition, enabling recursion without explicit naming. Also see [[Y Combinator]]. Lambda calculus also supports higher-order functions, which means that functions can take other functions as arguments or return them as results. This higher-order functionality allows for powerful abstractions and modular programming techniques. ![[Backus-Naur Form#How is BNF related to lambda calculus?]] ![[symmetric monoidal category#SMC in Lambda Calculus?]] # Conclusion Overall, lambda calculus provides a theoretical framework for understanding computation through pure functional programming principles. Its simplicity yet expressive power has made it influential in various areas such as programming language design, type theory, and formal verification. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Lambda Calculus") or contains(title, "Lambda Calculus") or contains(title, "Lambda") or contains(subject, "Lambda Grammar") or contains(title, "Lambda Grammar") or contains(subject, "firstness") ```