# Questions tagged [lambda-calculus]

λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

567 questions
Filter by
Sorted by
Tagged with
1 vote
20 views

### 2-argument combinators and Turing completeness

SK, BCKW, and BAMT combinator systems are known to be Turing-complete and convertible into each other. (BAMT is mentioned in this blog post) ...
• 488
46 views

### Is there a category theory equivalent of pure type systems?

I have seen the correspondence between the simply-typed lambda calculus and Cartesian closed categories, and am curious about how this generalizes to other lambda calculi. I have seen some related ...
• 101
31 views

### In Lafont's interaction net, how to prevent undesirable annihilation?

Here is a simple case, given function f and input x, compute y = f(f(x)): this can be ...
• 103
40 views

### How to write a Y-combinator implementation in javascript that does not exceed maximum stack size

TL;DR: Why applying a javascript implementation of a factorial function with a lazy Y combinator fails with "Maximum call stack size exceeded"? Here is the code: ...
18 views

### Short SK combinator expression with long reduction / Busy Beaver for SK combinators

Question (short and simple version): Can anyone suggest a very short SK combinator expression with a ridiculously long, but still terminating, reduction path (ignoring loops)? Question (longer version)...
• 111
34 views

### Why Normalisation by Evaluation needs to use a different representation of programs?

I'm trying to understand NbE (Normalisation by Evaluation). One thing I don't get is why it uses two different representations of programs: a syntactic and a semantic one. All the implementations of ...
• 201
1 vote
46 views

411 views

### What exactly is delta reduction?

I have found two definitions of delta reduction: Barry Watson defines it as the result of applying a primitive computation to terms in normal forms But in Coq they define it as the substitution of a ...
48 views

### lambda-calculus Church Rosser Theorem and Application Order Reduction

I have a question about an "apparent" contradiction I found in my lesson notes on Application Order Reduction (AOR) and the Church-Rosser Theorem (CRT). I'd like to emphasize that I'm not ...
212 views

### The Kleene–Rosser paradox and the inconsistency of lambda calculus

In many references I find that the simply typed lambda calculus was introduced because the Kleene–Rosser paradox showed that pure/untyped lambda calculus was inconsistent. However, since it is untyped,...
• 143
70 views

### What is lambda caculus's "fix point combinators" corresponding to Turing Machine?

The lambda caculus equals to Turing Machine,so What is lambda caculus's "fix point combinators" corresponding to Turing Machine? according to the paper <Primitive Rec, Ackerman's Function,...
• 121
1 vote
90 views

### Seeking Intuitions about Recursion, Y Combinator and System F

So, as I understand things, System F (polymorphic lambda calculus) doesn't have the Y Combinator and isn't Turing Complete, but it is very expressive. This answer (https://cstheory.stackexchange.com/...
90 views

### Is shadowing of the type variable allowed in System F second order abstraction?

I'm reading Type Theory and Formal Proof by Nederpelt and Geuvers. Chapter 3 is about $\lambda 2$ and $\Pi$-Types (aka System F, I think?) and the derivation rule for 2nd order abstraction seems to ...
53 views

### Why, in principle, can a Turing machine describe any computation or procedure?

Why is it that a Turing machine can perform all kinds of calculations and procedures? As a test, I tried to perform a four-quadratic calculation using a Turing machine myself. However, although I ...
• 1
702 views

### Strictness in both arguments but not in each individually

I'm learning about strict functions in Haskell. A function f is strict if f ⊥ = ⊥ Some functions are strict only in the first argument (for e.g. const), others are strict in the second (for e.g. map)....
• 83
38 views

### Are lambda calculus forms with different variable names the same?

Someone suggested to me that the halting problem could be solved by a lambda calculus "program", which reduces to $\lambda y.y$ if an input program halts and $\lambda n.n$ if it does not. ...
74 views

### Can we solve a decision problem with two identical answers like $false\equiv(\lambda f.\lambda y.y)$ or $0\equiv(\lambda f.\lambda n.n)$?

as the title says Can we solve a decision problem with two identical answers like $false\equiv(\lambda f.\lambda y.y)$ or $0\equiv(\lambda f.\lambda n.n)$? if no why? and if yes then why can't we ...
• 73
203 views

### Why use the term "beta equality"?

In lambda calculus (I will use untyped) if a term containing a redex is beta-reduced to another term, then for some reason they are considered "beta-equal". But the lambda calculus only ...
57 views

### Lambda calculus with unordered application

In lambda calculus, $\lambda xy.\phi$ isn't in general equivalent to $\lambda yx.\phi$. However, it seems possible to imagine a calculus which replaces application with something like specification, ...
• 241
86 views

### How a simple algorithm of adding two numbers can be written in lambda calculus?

It is claimed that "lambda calculus is a universal model of computation that can be used to simulate any Turing machine". How can I, using this universal model, simulate an algorithm of ...
• 113
67 views

### Confusion when composing functions in Lambda expression

$$(\lambda x. x \text{ } x ) ( \lambda x . x \text{ } x )= (\lambda x. x \text{ } x) ( \lambda x . x \text{ } x)$$ Source I am a bit confused on how this composition was done. When I do it, I get: ...
72 views

### How to find a term that proves a given proposition?

I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ...
1 vote
44 views

### Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ...
33 views

### Where can I find a list of logics with their corresponding calculus and computation phenomena?

I was watching some lectures by Prof. Pfenning on Proof Theory. Between 5:30 and 15:00, he gave a list for some different kinds of judgments along with their calculus and computation phenomena that ...
• 109
1 vote
79 views

### How does "+" operator fit into the formal grammar of $\lambda$-calculus?

In Wikipedia I found out that the formal grammar of $\lambda$-calculus is the following: ...
• 113
1 vote