Skip to main content

Questions tagged [lambda-calculus]

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

Filter by
Sorted by
Tagged with
0 votes
0 answers
17 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 ...
0 votes
0 answers
21 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: ...
1 vote
1 answer
165 views

Call by name, lambda calculs. Multiplication

How to multiply in CBN strategy? ...
4 votes
1 answer
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 ...
0 votes
0 answers
17 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)...
1 vote
1 answer
41 views

In what sense do universes solve the problem of not having type $\Pi_{A:\text{Type}}B(A)$?

One motivation for introducing universes, as I see it, is that without universes, we cannot construct types like $\Pi_{A:\text{Type}}B(A)$ because they would require us to have $\Gamma.\text{Type}\...
1 vote
1 answer
78 views

Indexing a list in Lambda calculus

I have tried to implement a list indexing function in lambda calculus and for some reason it is not working. Would anyone be able to point out to me what I am doing wrong? Assuming standard church ...
2 votes
1 answer
42 views

Adding type constructors to universes

Suppse we have a Tarski-style universe $U$, which means, in particular, that the following rules are declared: $$\frac{}{\Gamma \vdash U \text{ type}} \quad \frac{\Gamma \vdash a:U}{\Gamma \vdash \...
5 votes
2 answers
356 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 ...
1 vote
0 answers
23 views

What is a simple explanation of how the calculus of inductive constructions is an extension of simply typed lambda calculus?

I’m doing some basic studying of lambda calculus and Coq and I’d like some supporting explanation about the relationship between lambda calculus and the calculus of inductive constructions. This ...
0 votes
1 answer
62 views

What is a simple explanation and example of de Bruijn indices?

In order to find the recurrence formula for the number of λ-terms of a given size, we make use of the representation of variables in λ-terms by de Bruijn indices. Recall that a de Bruijn index is a ...
1 vote
0 answers
21 views

Why does the presence of bound variables make enumerating the terms of lambda calculus “unsolveable with generating functions/analytic combinatorics?”

…amazingly very little is known about combinatorial aspects of λ-terms, probably because of the intrinsic difficulty of the combinatorial structure of lambda calculus due to the presence of bound ...
1 vote
0 answers
36 views

Analog of semantic paradoxes in type theory?

By semantic paradoxes, I mean like the Liar paradox, Curry paradox, Knower paradox, etc. In classical (logic) settings, we would need to extend the language with a predicate P (truth or is-known ...
2 votes
1 answer
52 views

"union" or "disjunction" in pure untyped lambda calculus

In the untyped lambda calculus (with variables, abstraction and application as the only constructors), we have a "pair" construct, given by $(a, b) = \lambda x, x a b$. The projections are ...
30 votes
3 answers
871 views

Characterization of lambda-terms that have union types

Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping): $$ \dfrac{\...
1 vote
0 answers
40 views

What is the significance of the equation $\langle \pi_1 M, \pi_2 M \rangle = M$ in $\lambda$-calculus?

When extending the simply typed $\lambda$-calculus with products, we extend $\beta$-reduction with the rules $\pi_i \langle M_1, M_2 \rangle \to_\beta M_i$, which makes sense (cf. Sørensen, Urzyczyn, ...
3 votes
1 answer
71 views

What are the fixed-points of the Y combinator?

Since the Y combinator itself is a function (albeit a higher-order one), I was wondering what the fixed-points of Y itself are.
3 votes
1 answer
78 views

Equality of lambda terms which do not have normal form

In the context of lambda calculus, how should one prove $\beta$-equality of terms that do not have normal form? In particular, how to prove that these are different combinators: $$ Y = λf.(λx.f(xx))(...
10 votes
1 answer
192 views

Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection

Suppose we have a System F term $f : \forall \alpha. \alpha\times\alpha\to\alpha$, interpreted in a parametric model which is a bicartesian closed category. I was wondering if in such context it is ...
1 vote
2 answers
1k views

how to solve this lambda expression with free variable/s

Iam a beginner in Lambda Calculus, I have a expression saying (λx.xy) Here y is a free variable and x is a bound variable. My question is what would be the value of the expression (which has free ...
1 vote
2 answers
478 views

When is a variable bound or free in a lambda application?

I am currently reading the book "An Introduction to Functional Programming through Lambda Calculus" (the 2011 edition) and am a bit puzzled by the definitions of free and bound variables ...
3 votes
2 answers
97 views

How is `y λx.x y` parsed using the standard pure untyped lambda calculus conventions?

How would the following term in the pure untyped lambda calculus be parsed: y λx.x y The relevant conventions listed on https://en.wikipedia.org/wiki/...
3 votes
2 answers
153 views

How, if possible, can we efficiently compute with lazy data structures in 𝜆-calculus?

In Haskell, we can use the following code to define fibonacci numbers, fibs = 1 : 1 : zipWith (+) fibs (tail fibs) And its time complexity is linear. I cannot find ...
0 votes
1 answer
61 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 ...
0 votes
0 answers
12 views

Are there non-brute-force algorithms for longest or shortest beta reduction path?

Consider the related problems of, given a strongly normalizing lambda term, computing the longest and shortest paths ending in a normal form. In terms of bits of input the optimal complexity is some ...
0 votes
1 answer
51 views

Is my understanding of Eta reduction correct?

In my script I have the following term: x => y => both (x) (y) This is reduced to both My interpretation is that this function (the whole term) takes two arguments and returns a function and ...
2 votes
2 answers
350 views

Can the Y-combinator really terminate?

My understanding of the Y-combinator is that it never terminates (Yg = g(Yg)). Its termination is only decided externally to the $\lambda$ specification when it has ...
5 votes
2 answers
270 views

Elegant algorithm to semi-decide if two lambda calculus terms are equivalent

Given two lambda terms $t_1$ and $t_2$, it is semi-decidable if they are equivalent (i.e. can be rewritten as each other using alpha, beta, and eta conversions). An algorithm to do this is to try ...
1 vote
0 answers
40 views

The isomorphism in "Scott's representation theorem"

In the essay Relating Theories of the lambda-calculus, Scott constructs (from page 418) a category that exhibits a chosen lambda calculus $ L $ with $ \beta $-equality as the collection(s) of ...
0 votes
1 answer
49 views

Lambda Calculus vs Turing Machine

How functional programming using lambda calculus is analogous to construction of Turing machine as per computational aspects?
2 votes
1 answer
192 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 ...
5 votes
1 answer
141 views

Closures break induction in correctness proof of interpreter

I'm trying to prove the correctness of an interpreter for a simple extension of untyped lambda-calculus with De Bruijn indices. The interpreter is bounded, i.e. in order to ensure its finiteness it ...
6 votes
0 answers
89 views

Is it possible to reduce functional equations to SAT?

The problem of finding a solution for functional equations can be defined as: Let $A_0, A_1, A_2, \dots, A_n, B_0, B_1, B_2, \dots, B_n, X$ be terms of the $\lambda$-calculus, where all terms are ...
0 votes
2 answers
72 views

$xx$ application in lambda calculus

I'm just getting started with lambda calculus and I see that the fixed-point $Y$ combinator is defined as: $Y = \lambda f . (\lambda x . f(x x))(\lambda x . f(x x))$ (*) I read here that something ...
8 votes
0 answers
66 views

When does type inference become undecidable in typed lambda calculus?

To begin with, if I understand correctly, in a simply typed lambda calculus, typing, type checking and type inference are always decidable. In the "full-fledged" polymorphic (terms depend on ...
2 votes
2 answers
408 views

I've heard that it isn't possible to encode product types and sum types in a simply typed lambda calculus, but it seems for me that it's false

Of course, it isn't possible to construct them directly since we hasn't these type constructors, but only function constructor (arrow). But suppose there are 2 types $A$ and $B$, from which we need to ...
0 votes
0 answers
41 views

What are some visual representations of the lambda calculus?

I'm building some teaching tools for teaching the lambda calculus and would like some kind of visual representation of it. I've looked at Alligator Eggs and while it is something very similar to what ...
3 votes
1 answer
120 views

Expression with fastest growth in lambda-calculus

Well-known example of divergent expression in lambda calculus is big-Omega combinator, defined as (λf. f f)(λf. f f). Although big-Omega is divergent expression, it'...
1 vote
2 answers
65 views

(how) is assignment or binding possible in purely functional languages?

i can't seem to find much info on the following question: how (if at all) is the fixing of names to values (by binding or assignment) possible in a purely functional system like the lambda calculus? i'...
0 votes
0 answers
65 views

Representation of pairs in System F

System F defines the data type pair as: $$X\times Y := \Pi Z. (X\to Y \to Z)\to Z$$ with: $$\langle x,y \rangle := \Lambda Z. \lambda p^{X\to Y\to Z}.p \text{ }x\text{ } y$$ Projections are defined: $$...
0 votes
1 answer
86 views

Valid Lambda Expressions

I have two questions about the validity of lambda expressions. First, is a variable on it's own a valid lambda expression (ex: λx) Second, take for example these two lambda expressions (λx.fxya and ...
2 votes
1 answer
44 views

Is it actually the case that $Yg \to_\beta g(Yg)$?

For reference, the $Y$-combinator is the expression $$ Y = \lambda f . (\lambda x . f (xx)) (\lambda x . f (xx)) $$ in the untyped lambda calculus. If $g$ is any lambda expression, then \begin{align} ...
0 votes
0 answers
25 views

Does lambda calculus become covariant if you fix the base type instead of the lambda calculus term?

In category theory, we are taught that polymorphic functions correspond to dinatural transformations, a k a multivariant natural transformations between functors of mixed variance $\operatorname{G} \...
36 votes
7 answers
7k views

Clear, intuitive derivation of the fixed-point combinator (Y combinator)?

The fixed-point combinator FIX (aka the Y combinator) in the (untyped) lambda calculus ($\lambda$) is defined as: FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. ...
5 votes
2 answers
1k views

What is a quotient structure?

I was reading a paper here, and it mentioned "quotient structure" in the following sentence (third page, second paragraph of the paper) In order to obtain a representation of terms truly isomorphic ...
6 votes
2 answers
1k views

How does this left-associative recursive descent parser work?

For personal enlightenment, I'm trying to write a recursive descent parser for lambda calculus without abstraction, i.e., just identifiers and function application. The BNF grammar that describes the ...
-1 votes
1 answer
91 views

Equivalence between Lambda Calculus [Church] and Computable Partial Functions [Godel]

In order to show that Lambda calculus and Turing machines are equivalent it is sufficient to show that you can simulate one in the other [both ways]. We can observe it in action. Can one do the same ...
2 votes
0 answers
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 ...
2 votes
2 answers
190 views

Is this definition of $\alpha$-equivalence correct?

I want to extend $\alpha$-equivalence to cover substitution. That is, I will implement runSubst_Term : Subst -> Tm -> Tm and prove: ...
4 votes
1 answer
202 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,...

1
2 3 4 5
12