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

372 questions
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 ...
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 ...
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”?
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 ...
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 ...
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 ...
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 ...
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 ...
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$), ...
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 ...
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 ...
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 ...
553 views

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:...
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(...
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 ...
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?
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 ...
133 views

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 ...
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:...
75 views

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. ...
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 ...
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 ...
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 ...
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: ...
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 ...
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 ...
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$ ...
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 \...
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 ...
135 views