Mathematics Stack Exchange
Mathematics Stack Exchange

Questions tagged [lambda-calculus]

For questions on the formal system in mathematical logic for expressing computation using abstract notions of functions and combining them through binding and substitution.

Lambda calculus (also written as λ-calculus) is a formal system in mathematical and theoretical for expressing computation based on function abstraction and application using variable binding and substitution. Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote binding a variable in a function.

It was first introduced by mathematician Alonzo Church in the 1930s as part of his research of the of mathematics. The original system was shown to be logically inconsistent because of the Kleene–Rosser paradox. Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus.

Untyped lambda calculus is Turing complete, that is, it is a universal model of computation that can be used to simulate any (see ). It may be used to model booleans, arithmetic, data structures and recursion.

Lambda calculus may be untyped or typed. In typed lambda calculus (see ), functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are weaker than the untyped lambda calculus, in the sense that typed lambda calculi can express less than the untyped calculus can, but on the other hand typed lambda calculi allow more things to be proved; in the simply typed lambda calculus it is for example a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate. One reason there are many different typed lambda calculi has been the desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus.

Typed lambda calculi are closely related to mathematical and via the Curry–Howard isomorphism: types correspond to logic formulas, lambda-terms correspond to derivations in a logic system (depending on the kind of typed lambda calculus) and computation steps in the lambda calculus correspond to normalization (i.e. cut-elimination) steps for derivations.

Lambda calculus has applications in many different areas in mathematics, philosophy, linguistics, and computer science. Lambda calculus has played an important role in the development of the theory of languages, since functional programming languages implement the lambda calculus. Lambda calculus also is a current research topic in .

655 questions
1
vote
0 answers

Equivalence in lambda calculus

As far as I know, two lambda terms are equal if and only if their normal forms can be $\alpha$ converted to each other. However, for expressions that do not have a normal form (such as expressions involving a Y combinator), are there any rules to…
creaple
  • 68
1
vote
0 answers

How to prove that Lambda Calculus term does not have normal form?

In 1958 Curry proved that if the leftmost reduction of a λ-term $X_1$ is infinite, then all reductions starting at X1 can be continued for ever, i.e. $X_1$ has no normal form. How to show that the leftmost reduction is infinite? Do I understand…
Oleg Dats
  • 425
1
vote
1 answer

How to implement an algorithm to separate lambda calculus terms using Böhm's theorem?

Theorem 1 (Böhm, 1968) Let $Λ$ be the set of closed normal forms, and let $S1$ and $S2$ be arbitrary λ-terms. For any non η-equivalent terms $T1, T2 ∈ Λ$ there exists a λ-term $∆$ such that the application of $∆$ to $T1$ evaluates to $S1$ and the…
Oleg Dats
  • 425
1
vote
1 answer

Is there a lambda calculus term $s$ such that $s(tu)$ is $\beta$-equal to $u$ for all untyped lambda calculus terms $u$ and $t$

Is it possible to find a lambda term $s$ such that for all terms $t$ and $u$ (of untyped lambda calculus) , $s(tu) = u $ where the equality refers to $\beta$-equality? I thought that no such $s$ should exist since I don't see how any beta reduction…
Sam Pine
  • 21
1
vote
0 answers

SKI combinator calculus of `2 = λf.λx.f(f x)`

EDIT: refactored this question into a slightly different, but related one: Rules for converting lambda calculus expressions to SKI combinator calculus expression? Which rule(s) is/are incorrect? learnxinyminutes.com defines $I$, $K$, and $S$ as…
joseville
  • 1,477
1
vote
0 answers

Is the untyped lambda calculus consistent if equations containing non-β-normal forms are void?

Consider the function $f = \lambda x \mapsto \neg (x\ x)$ where $\neg$ is negation. It then follows that $$ f\ f = \neg (f\ f) $$ Thus proving a contradiction, but $(f\ f)$ is an expression that does not have a $\beta$-normal form. This expression…
user132716
1
vote
1 answer

Lambda Calculus Church Encoding Successor Function

I'm slightly confused by the successor function for Church numerals. Written down in my textbook it is defined as follows: $$succ = \lambda n. \lambda f. \lambda x. n \;f \; (f \; x) $$ Therefore incrementing a number $n$ by one works as follows: $$…
George Herbert
  • 11
1
vote
1 answer

Lambda application terms MN where M is not a Lambda abstraction term?

I believe such terms are syntactically legal in (untyped) lambda calculus (see below), but the motivation for including them is not very clear to this newbie (e.g. because MN has no potential for reducibility). Perhaps I am hung up on the fact that…
JRC
  • 516
1
vote
1 answer

Lambda Calculus: What does $\lambda x.(\lambda xy.xy)(xx)$ or $\lambda x.\lambda y(xx)y$ mean?

I'm trying to understand fixpoints in the Lambda Calculus with the example of computing the fixpoint of $\lambda xy.xy$. I might have a vague intuition what $\lambda x.(\lambda xy.xy)(xx)$ means/does but I cannot go any further. What does $\lambda…
topkek
  • 31
  • 4
1
vote
2 answers

Identifying All Redexes in Lambda Expression

I am self-studying Lambda calculus and have encountered a question where I need to identify all the redexes of the following expression: (λu.(λx.u)u)((λy.y)(λw.(λv.v)w)). Here are all the ones I've come up with, but I'm not sure if they are valid…
John Roberts
  • 273
1
vote
1 answer

How to reduce these equations with beta reduction - lambda calculus

How do I beta reduce these equations. My attempts are below the questions. (λy.zy)a = λy[y:=a].zy = λa.za (λz . zz)(λy . yy) = λz[z:=λy . yy].z z = (λy . yy)(λy . yy) = (λy[y:=λy . yy].yy) = (λy . yy)y = λy[y:=y]y (λx.x)(λx.x) =…
llamaro25
  • 289
1
vote
1 answer

Show that there does not exist $F$ such that $F(MN) = M$ for all $M$ and $N$.

This is for Exercise 2.4.6 of Barengredt's "Lambda Calculus - It's Syntax and Semantics" and the exact statement from the book is to "Show that $\neg \ \exists \ F \ \forall \ MN \ F(MN) = M$". My solution is as follows, and I was wondering if there…
Anonymous
  • 13
  • 3
1
vote
1 answer

Is it appropriate to do alpha reduction before substitution?

In the lambda expression (λx. (λy. y z)(λw. w) z x)[z→y], I'm inclined to change y to another variable, then perform the substitution. Is this the correct way to approach this problem? Also, if that's the case, and you can just alpha-reduce back,…
Ross Verry
  • 13
1
vote
1 answer

Don't understand unbound variables in a lambda calculus expression

I'm learning lambda calculus. I came across this lambda expression: lambda f s e . e f s When I pass arguments 1 and 2 to the expression, it should return 1 2 but I cannot figure out how is that possible. The way I tried to expand this: (lambda f s…
T.Poe
  • 147
  • 8
1
vote
1 answer

Are these 2 lambda calculus terms equivalent?

I have 2 lambda terms and I am not sure whether the rules of bounded variables in the lambda calculus imply that these 2 terms are equivalent or not. They are: $λc.λc.bc$ $λc.λa.ba$ I know that in the first of the 2 terms the c's in $\dots λ…
D.Yvel
  • 13
1 2 3
…
15 16