Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit 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.

114
votes
9answers
26k views

Learning Lambda Calculus

What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus? Specifically, I am interested in the following areas: Untyped lambda calculus ...
45
votes
2answers
7k views

Why isn't lambda notation popular among mathematicians?

I am relatively new to the world of academical mathematics, but I have noticed that most, if not all, mathematical textbooks that I've had the chance to come across, seem completely oblivious to the ...
37
votes
4answers
5k views

Why is lambda calculus named after that specific Greek letter? Why not “rho calculus”, for example?

Where does the choice of the Greek letter $\lambda$ in the name of “lambda calculus” come from? Why isn't it, for example, “rho calculus”?
27
votes
2answers
5k views

Can someone explain the Y Combinator?

The Y combinator is a concept in functional programming, borrowed from the lambda calculus. It is a fixed-point combinator. A fixed point combinator $G$ is a higher-order function (a functional, in ...
23
votes
2answers
9k views

What's the point of eta-conversion in lambda calculus?

I think I'm not understanding it, but eta-conversion looks to me as a beta-conversion that does nothing, a special case of beta-conversion where the result is just the term in the lambda abstraction ...
19
votes
4answers
1k views

The “functions” of untyped lambda calculus are not (set theoretic) functions so what are they?

You can't model $\lambda$ functions as set functions because the domain of a $\lambda$ function includes that function itself. This violates foundation. However they clearly are some sort of ...
14
votes
1answer
2k views

lambda calculus and category theory

I am not particularly knowledgeable in either lambda calculus or category theory, but I am starting to learn Haskell so I would like to ask: are there connections between category theory and lambda ...
14
votes
1answer
2k views

The Power of Lambda Calculi

A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions. What are the advantages of typed lambda calculus over untyped lambda calculus in terms ...
12
votes
4answers
2k views

How do lambda calculus most basic definitions work?

Good afternoon, I'm trying to learn lambda calculus, and I do understand the notation (it's not hard, $f=\lambda a_1.\cdots\lambda a_n.x=\lambda a_1\cdots a_n.x\Leftrightarrow f(a_1;\cdots;a_n)=x$), ...
12
votes
1answer
1k views

If $f(x)=g(x)$ for all $x:A$, why is it not true that $\lambda x{.}f(x)=\lambda x{.}g(x)$?

There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily ...
12
votes
0answers
633 views

Why can't we formalize the lambda calculus in first order logic?

I'm reading through Hindley and Seldin's book about the lambda calculus and combinatory logic. In the book, the authors express that, though combinatory logic can be expressed as an equational theory ...
11
votes
4answers
507 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
10
votes
2answers
553 views

What is the shortest function of lambda calculus that generates all functions of lambda calculus?

I suspect there's a good chance the answer to this is unknown and hard (or at least extremely tedious), but I figured it would be worth asking. It's well known that the functions $K:=\lambda x.\...
10
votes
0answers
418 views

Fixed points in computability and logic

I asked this question on CS.SE, too: https://cstheory.stackexchange.com/questions/27322/fixed-points-in-computability-and-logic I would like to understand better the relation between fixed point ...
9
votes
1answer
770 views

Proving that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus

I am trying to prove that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus. Surprisingly, different textbooks and lecture notes do not contain that proof, ...
8
votes
1answer
1k views

What breaks the Turing Completeness of simply typed lambda calculus?

On the Wikipedia page about Turing Completeness, we can read that: Although (untyped) lambda calculus is Turing-complete, simply typed lambda calculus is not. I am curious as to what exactly makes ...
8
votes
1answer
188 views

How to prove that these are the only type inhabitants?

Consider a type $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$ with its two inhabitants \begin{align} \mathrm{tt} &= \lambda x.\ \lambda y.\ x \\ \mathrm{ff} &= \lambda x....
7
votes
2answers
10k views

Lambda Calc: bound and free variables?

I'm trying to work through "Elements of Functional Languages" by Martin Henson. On p. 17 he says: $v$ occurs free in $v$, $(\lambda v.v)v$, $vw$ and $(\lambda w.v)$ but not in $\lambda v.v$ or in $\...
7
votes
2answers
451 views

How does second-order logic relate to lambda calculus?

How does second-order arithmetic/logic relate to lambda calculus? By lambda calculus, I mean both typed and untyped. And is there any relationship with recursive and recursively enumerable sets? Edit:...
7
votes
1answer
5k views

How to multiply in Lambda Calculus?

I have trouble, when attempting to multiply Church numerals with lambda. First, does this work? MULT := $\lambda$mnfx.m ( PLUS n ) MULT := $\lambda$mnfx.m ( m SUCC n ) MULT := $\lambda$mnfx.m(m f(...
7
votes
1answer
3k views

Use of parenthesis in lambda calculus

As a summer project I am trying to learn lambda calculus. I am not that good with math but I have learned myself several programming languages and somehow got the idea that learning lambda calculus ...
7
votes
2answers
761 views

What's the definition of equational theory? Why is λ logic free?

A book says that "λ is logic free: it is an equational theory." But I don't understand the "logic free" and "equational theory". Can you help me?
7
votes
1answer
285 views

What is the actual significance of the lambda calculus for the formalization of math?

The Simply Typed Lambda Calculus was proposed initially as a foundational system for the formalization of mathematics. As such, I would expect that soon there would be attempts to implement most of ...
7
votes
0answers
133 views

Equivalence of categories of directed complete posets

In the book ``Domains and Lambda-Calculi'' by Amadio and Curien, there is the following exercise: Define an equivalence between the category of partial morphisms generated by $(\mathcal{M}_S, \textbf{...
6
votes
2answers
1k views

Is this formula really the nine axioms?

I was reading a note from guardian.uk called What lurks beneath a scientist's lab coat?, a little gallery of geeky-tattoos. However, number 11 in the series has the following image and caption text: ...
6
votes
2answers
124 views

Problem with a basic lemma in Lambda Calculus

I have some serious problems with Lambda Calculus. In an introduction by Barendregt and Barendsen at page 11 there is the following lemma, whose proof I do not completely get. $\mathbf{\lambda} \...
6
votes
1answer
591 views

Fixed point combinator (Y) and fixed point equation

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states: In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$ can ...
6
votes
2answers
1k views

Representing lists and trees in System F

System F (also known as second-order lambda calculus or polymorphic lambda calculus) is defined as follows. Types are defined starting from type variables $X, Y, Z, \ldots$ by means of two operations:...
6
votes
2answers
75 views

In rewiring systems do definitions creates new rewrite laws or an alias? And is this a meaningful question?

Lambda calculus is often introduced as a rewriting or substitution system. Where $\beta$ reduction is described as replacing bound variables with the value that variable is bound to. For example $(\...
6
votes
2answers
1k views

Krivine Machine

Can someone please point out online resources to learn about Krivine Machine? My professor briefly touched it while teaching a course in Computer logic. google did not turn up much except some papers ...
6
votes
1answer
76 views

What categories are described by relational programming languages?

I know that lambda calculus is the language of cartesian closed categories. As I understand it, relational programming systems (that, as the name implies describe a computation in terms of relations) ...
5
votes
2answers
938 views

Understanding η-conversion (Lambda Calculus)

Let $h \in A\rightarrow (B\rightarrow C)$ I'm trying to understand the following reduction: $$\lambda x\in A. \lambda y \in B.(h(x))(y) \\= \lambda x\in A.h(x) \\= h$$ Apparently, this is done by ...
5
votes
2answers
1k views

Relation between Cartesian closed category and Lambda Calculus

I am programmer (from the object oriented world) and currently getting my head around functional programming. I was looking to get some basics right. I understand what category theory and lambda ...
5
votes
2answers
849 views

In what sense is the S-combinator “substitution”?

According to the Wikipedia page on SKI-combinator calculus, I is the identity function, K is the constant function, and S is "substitution". I understand the first two, but I don't see what S has to ...
5
votes
1answer
377 views

Book on Curry-Howard Isomorphisms

I would like to learn about Curry-Howard Isomorphism because I want to know more about connections between computability and logic. I have already read book on first order logic and I know about ...
5
votes
1answer
96 views

Is there a standard notation for the pre-composition operator?

Let $X_1$, $X_2$, and $V$ be sets. Is there a standard name and a standard notation for the pre-composition operator $F$ that takes as input a function $\varphi:X_2^{X_1}$ and returns the operator $F_{...
5
votes
2answers
3k views

Substitution in lambda calculus

I have just started reading lambda calculus. In substitution it says $(\lambda x.M)N= [N/x]M$ (means all the free occurrences of $x$ in $M$ will be substituted by $N$) But $x$ is a bound variable. ...
5
votes
2answers
75 views

Can all mathematical operations be encoded with a Turing Complete language?

In High School Computing I was taught the Structured Program Theorem - that you could implement any mathematical operation using: Sequence Selection Iteration After completing a Computer Science ...
5
votes
2answers
1k views

Types versus kinds and sorts

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type? My raw guess if that a kind is the higher level ...
5
votes
1answer
517 views

Wikipedia's explanation of the lambda-calclulus form of Curry's paradox makes no sense

Wikipedia gives multiple explanations of Curry's paradox, one of which is expressed via lambda calculus. However, the explanation doesn't look like any lambda calculus I've ever seen, and there's an ...
5
votes
1answer
39 views

Beta reduction for expression

I'm given the following where: TRUE = λxy.x FALSE = λxy.y IF = λbtf. b t f OR = λxy. IF x TRUE y and I'm trying to evaluate: ...
5
votes
0answers
160 views

Injections between distinct models of the simply typed lambda calculus

Let a model of the simply typed lambda calculus be a Cartesian-closed functor from $C_T$ to Set, where $C_T$ is a free CCC (as in e.g. this reference, p. 83.) The simple case of one or two primitive ...
5
votes
0answers
112 views

Is there any elegant formalization of fractional numbers?

The question is just what is on the title, but I'll describe the context for completion: Natural numbers can be encoded quite elegantly on the Lambda Calculus as church numbers, that is, a function ...
4
votes
2answers
213 views

Currying and Uncurrying of logical formulas, is $(A \land B) \to C \leftrightarrow (A\to B)\to C$

With a truth table its easy to see that the two formulae $A\land B \to C$ and $A \to B \to C$ are not equivalent, for example, if $A = B = C = 0$, than the first evaluates to $1$ and the second to $0$ ...
4
votes
1answer
207 views

Is Lambda calculus a purely equational theory?

In a previous question I have been told that lambda calculs is pure syntax. I see that Lambda calculus is introduced inductively, but I don't see from what axioms it follows that: $$(\lambda x.x) M \...
4
votes
2answers
1k views

Encode lambda calculus in arithmetic?

There is plenty of information about how to encode arithmetic given the lambda calculus. The wikipedia article on Church Encoding seems complete to my inexpert eye. My question is "how about the ...
4
votes
1answer
135 views

$\beta$ inequality in $\lambda$-calculus

Prerequisites Consider the $\lambda$-calculus where terms are equivalence classes over the $\alpha$-equality. We define $\to_\beta$-reduction in the usual way, i.e. the least congruent relation on $...
4
votes
2answers
47 views

Help understand beta reduction example

I am currently reading a text book on distributed computing systems that includes a short introduction to $\lambda$-calculus. There is an example of evaluating the sequence $(((if \space \space true) ...
4
votes
3answers
325 views

What's a good resource to learn about the simply typed lambda calculus?

I've read An Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to ...
4
votes
3answers
757 views

Book on lambda calculus logic and type theory

Can someone recommend me a book for self study which will cover topics of logic, lambda calculus and type theory. I know about "Computability and Logic" written by Bolos but it describe recursive ...