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
0
votes
0 answers

Behaviour of successor function that is composition

I want to show that $$ S^{m} \underline{n} = \underline{n+m} $$ where $S$ is successor function and $\underline{m},\underline{n}$ are Church numerals. Note that $S^m (x) = \underbrace{S(S(..(S}_\text{m-times}x)..))$. Also successor function S is…
Logan Lee
  • 249
0
votes
0 answers

Generalizing lambda or expression

I want to generalize $$ \underline{or} = \lambda xy. (x \to \underline{true} | y) $$ to $\lambda AB. (A \to (\underline{true} \to ...) | B \to ...)$. Here's my try: Cases: If A: If B: $\underline{true} \to Axy \to x$ If $\underline{not}$ B:…
Logan Lee
  • 249
0
votes
1 answer

Is there a valid application where variables are not distinct and occur free in operand

Consider $$ (\lambda V_1..V_n. E)E_1..E_n $$ Is there a case where application of this form is valid if not all $V_i$ are distinct and some $V_i$ occur free in $E_i$? Here's an example where it is not valid. $$ (\lambda xx. \underline{sum} \…
Logan Lee
  • 249
0
votes
1 answer

Definition of variable V occurring free in lambda expression E

What does the following mean? $$ (\lambda V_1 V_2.E) E_1 E_2 $$ "$V_2$ occurs free in $E_1$." Does this mean $E_1$ contains references to $V_2$? Could you explain with examples? Thanks a bunch!
Logan Lee
  • 249
0
votes
3 answers

Lambda calculus Clarification about free and bound variables

In $(\lambda x.yx)$ y is free. How about in $(\lambda x.xy)$ is y bound here? Some googling I've found that y is actually free, but isn't y in the scope of $\lambda x$? Thanks!
Logan Lee
  • 249
0
votes
2 answers

Rules for beta conversion passing abstraction as parameter

Can you tell me why the following reduction is true? $$ (\lambda x.yx)(\lambda y.xy)=yx $$ I'm not quite sure about the rules to follow when abstraction $(\lambda y.xy)$ is applied to $(\lambda x.yx)$. Thanks.
Logan Lee
  • 249
0
votes
1 answer

Evaluation of $\beta$-reduction of $~\left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right)$

$$\begin{align} \Delta&:= \lambda x ~.~x~x~x\\ \Delta\Delta&\rightarrow_\beta\Delta\Delta\Delta\\ \left(\lambda x ~.~x~x~x \right) \left(\lambda x ~.~x~x~x \right)&\rightarrow_\beta \left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x…
electrical apprentice
  • 1,519
0
votes
1 answer

Function subscript notation in Types and Programming Language

In Pierce, Types and Programming Languages, Chapter 6, the reader is asked to define a function $removenames_\Gamma(t)$ where $\Gamma$ is a naming context and $t$ is a term with some number of free variables less than $dom(\Gamma)$ and the function…
sam256
  • 121
0
votes
1 answer

Barendregt Recursion encoding

There is a definition in "Lambda Calculi with Types" by Henk Barendregt (pdf) that I am really struggling with. There are seemingly no examples of it, and I can't find anyone else on the internet using it. Is this a number? I can try and use this…
marcopopo
  • 73
0
votes
1 answer

How do I prove "1 not True == False" in Lambda Calculus?

I have to prove "1 not True == False" in Lambda Calculus which is (left side of eq): (λs.λz.s z) (λx.x (λt.λf.f)(λt.λf.t))(λt.λf.t) I come to this step: (which I know is still correct, just brackets could be wrong but I would not know how do get…
Peybro
  • 103
0
votes
2 answers

Significance of the inner parentheses in this lambda expression? $(\lambda xyz.xy(zx)) \;1\; 2\; 3$

I have this lambda expression $$(\lambda xyz.xy(zx)) \;1\; 2\; 3$$ or $$(\lambda x. (\lambda y. (\lambda z.xy(zx))))\;1\;2\;3$$ $$(\lambda y. (\lambda z.1y(z1))))\;2\;3$$ $$(\lambda z.12(z1))))\;3$$ $$1\;2\;(3\;1)$$ What exactly is the point of the…
147pm
  • 920
0
votes
1 answer

Lambda Calculus syntax: multiplication is or isn't implied?

If I have this $$(\lambda xy.xy)\; 1 \; 2$$ does this beta reduce to ($1 \; 2$) or is multiplication finally implied ($1 \cdot 2$), i.e., $2$ -- the former being just $1$ then $2$ beside it, not interacting?
147pm
  • 920
0
votes
0 answers

Lambda Calculus Extended/Revised substitution rule

Wikipedia's Lambda Calculus article defines the substitution, $M[x:=N]$ by recursion as follows: $x[x:=N] = N$ $y[x:=N] = y$, if $x \not =y$ $(M_1M_2)[x:=N]=(M_1[x:=N])(M_2[x:=N])$ $(\lambda x.M)[x:=N] = \lambda x.M$ $(\lambda y.M)[x:=N] = \lambda…
joseville
  • 1,477
0
votes
2 answers

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 follows: I x = x K x y = x S x y z = x z (y z) Then they give the following correspondences to aid in the conversion between lambda calculus and SKI combinator calculus: λx.x = I EDIT: λx.c = Kc…
joseville
  • 1,477
0
votes
1 answer

λ-calculus: When is it possible to split a term into two or more expressions, so that each can be used in separate β-reductions?

In the $\lambda$-calculus expression: $$ (\lambda x.\lambda y.xy)(f(f(a))) $$ Can the subexpression $(f(f(a))$ be split into two terms, $M$ and $N$? (Maybe, via $\alpha$-conversion?) If so, what could those two terms be? $f$ and $fa$? $ff$ and…
joseville
  • 1,477
1 2 3
…
15 16