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

Show that subtraction is primitive recursive

I want to show that subtraction is primitive recursive: $subtract(x,y)=x-y$. To do this, I must first show that pred function: $pred(x)=x-1$ is also primitive recursive. So, let's do that! First, we start with function $f'$ that accepts two…
Logan Lee
  • 249
2
votes
0 answers

Solving Klop's fixed-point operator problem

The following problem is attributed to Klop mentioned in Barendregt's book (as per notes I'm going through). Here's the problem: Show that $\underline{Y_2}$ is a fixed-point operator, where $$ LET \ @ = \lambda abcdefghijklmnopqstuvwxyzr.…
Logan Lee
  • 249
2
votes
1 answer

Prove the existence of $F \in \Lambda$ such that $Fx = xF$ for arbitrary variable $x \in \Lambda$

I recently met the problem as indicated in the title: find an $F \in \Lambda$ such that $Fx = xF$ for arbitrary variable $x \in \Lambda$. I am not only seeking a solution, but also a systematic way to think about such problems. Could someone help?
Ziqi Fan
  • 1,816
2
votes
2 answers

What are free variables in lambda calculus?

I am having trouble understanding the concept of free variables in lambda calculus. How and when should we use them? I read all Church encoding and there is no use of free variables. Natural numbers, arithmetic, pairs... everything is defined…
Oleg Dats
  • 425
2
votes
2 answers

How to Prove a Lemma in Lambda Calculus about Contexts

$ \newcommand{\abstraction}[2]{\lambda #1. #2}$ $\newcommand{\application}[2]{\left(#1 #2\right)}$ $\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$ $ \newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$…
Ziqi Fan
  • 1,816
2
votes
1 answer

Is this $\beta$-reduction step incorrect or not?

The brilliant.org article on Lambda Calculus$^1$ says that the following $\beta$-reduction step is incorrect: \begin{align} & (\lambda x.\lambda y.(xy))(\lambda x.\lambda y.(xy)) \\ & \rightarrow^\beta (\lambda y.((\lambda x.\lambda…
joseville
  • 1,477
2
votes
1 answer

Where and how lambda calculus is used?

So, I have been learning about lambda calculus at university and it seems too abstract and theoretical for me. Is lambda calculus used anywhere practically? P.S. I tried searching Haskell compiler code for anything related to lambda calculus but…
Nick Scriabin
  • 159
2
votes
1 answer

Typed vs untyped lambda calculus in methods for haskell

Expanding a bit on the following questions and their answers: Give Lambda Calculus Term for Haskell Function Infinite lists in Lambda calculus.... I really like the answers to the two questions, but it got me thinking: Is it possible to find a…
gaming4 mining
  • 125
2
votes
1 answer

Side Effects in Lambda Calculus

A simplistic method of creating effects in Lambda calculus is by adding constants: functions that create required effects. For example: we can add a rnd function which represents a random Church numeral, where for every j belonging to every natural…
user156182
2
votes
1 answer

Lambda Calculus: Why is the second equation more general than the first?

I was reading up on lambda calculus from Introduction to Lambda Calculus by Henk Barendregt and Erik Barendsen and came across this: $(λ~x.f[\textbf{x}])\textbf{x} = f[\textbf{x}]$ more generally one has $(λ~x.f[\textbf{x}])\textbf{N} =…
KMR
  • 51
2
votes
1 answer

How the the Identity in Church Numerals not the 'succ' function (ie. x + 1)

I realize this is probably a simple question for most people, but it is something that I am just having a hard time understanding. The numbers 1 and 2 is defined as: $1 = \lambda f. \lambda x. \space \space f \space x$ $2 = \lambda f. \lambda x.…
John
  • 123
2
votes
1 answer

Lambda Calculus: What is the difference between a $\lambda$ term with and w/o parenthesis?

Eg. what is the difference between $(\lambda y.M)[x:=N]$ and $\lambda y.M[x:=N]$?
topkek
  • 31
  • 4
2
votes
1 answer

In Lambda calculus, are there two terms said A, B which are typeable but when they combine, they become not typeable?

I have also provided my own examples and I am wondering if they are correct. Example 1: $A = x$ and $B = x$, they are both typeable but $A B = x x$ which are not typeable(?) Example 2: $A = \lambda x.x$ and $B = x$ so they are both typeable but $A…
Anon1995
  • 21
2
votes
1 answer

Beta-Reduction exercise with pairs in Lambda Calculus

I'm doing some simple exercise about Lambda Calculus but i have doubt about this beta-reduction. Let $$= \lambda p((p)u)v$$ a pair in Lambda Calculus. Prove that for every lambda term M you have that: $$ () \simeq_{\beta}…
Alessandro Recchia
  • 99
2
votes
1 answer

lambda calculus type assigned problem

we have $\lambda xabc.xa(xbc)$ and we should give a type for it can we assign $a$ and $b$ to the same symbol ? like here $a$ and $b$ should be same type for example $\alpha$ so we can continue ? $a,b = \alpha$ $c=\beta$ $x = \alpha \rightarrow \beta…
Mustafa Alahmid
  • 65
1 2 3
…
15 16