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
1 vote
0 answers
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) ...
Bubbler's user avatar
  • 488
0 votes
0 answers
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 ...
Chris Henson's user avatar
0 votes
0 answers
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 ...
tribbloid's user avatar
  • 103
0 votes
1 answer
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: ...
Bogdan Nikolakov's user avatar
0 votes
0 answers
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)...
Jim's user avatar
  • 111
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 ...
Blue Nebula's user avatar
1 vote
1 answer
46 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}\...
user avatar
2 votes
1 answer
43 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 \...
user avatar
1 vote
1 answer
82 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 ...
Fraser's user avatar
  • 11
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 ...
Julius Hamilton's user avatar
0 votes
1 answer
76 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 ...
Julius Hamilton's user avatar
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 ...
Julius Hamilton's user avatar
1 vote
0 answers
37 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 ...
confusedcius's user avatar
1 vote
0 answers
41 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, ...
Danny's user avatar
  • 131
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 ...
Tempestas Ludi's user avatar
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 ...
mjg's user avatar
  • 1
0 votes
1 answer
52 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 ...
Rubus's user avatar
  • 123
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 ...
Tempestas Ludi's user avatar
0 votes
1 answer
53 views

Lambda Calculus vs Turing Machine

How functional programming using lambda calculus is analogous to construction of Turing machine as per computational aspects?
soham singh's user avatar
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 ...
mell_o_tron's user avatar
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 ...
Weier's user avatar
  • 231
8 votes
0 answers
72 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 ...
P.A.R.T.E.I.'s user avatar
2 votes
2 answers
409 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 ...
P.A.R.T.E.I.'s user avatar
0 votes
0 answers
42 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 ...
LivesayEngineer's user avatar
1 vote
2 answers
66 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'...
elsewho's user avatar
  • 11
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: $$...
Antonio Hernando's user avatar
3 votes
1 answer
132 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'...
Vladislav Ihost's user avatar
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 ...
Jeremy Bowens's user avatar
2 votes
1 answer
45 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} ...
Danny's user avatar
  • 131
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} \...
Johan Thiborg-Ericson's user avatar
5 votes
2 answers
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 ...
Raffaele Rossi's user avatar
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 ...
user160762's user avatar
4 votes
1 answer
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,...
Fernando Chu's user avatar
0 votes
1 answer
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,...
wang kai's user avatar
  • 121
1 vote
0 answers
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/...
Noam Hudson's user avatar
3 votes
1 answer
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 ...
Raffaele Rossi's user avatar
0 votes
0 answers
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 ...
yt10's user avatar
  • 1
8 votes
1 answer
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)....
Marta's user avatar
  • 83
2 votes
1 answer
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. ...
Stack Exchange Supports Israel's user avatar
-3 votes
1 answer
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 ...
raoof's user avatar
  • 73
2 votes
1 answer
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 ...
S.I.L.V.E.R.'s user avatar
2 votes
0 answers
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, ...
SEC's user avatar
  • 241
0 votes
1 answer
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 ...
yegor256's user avatar
  • 113
0 votes
1 answer
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: $$...
Cathartic Encephalopathy's user avatar
0 votes
1 answer
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 ...
user avatar
1 vote
1 answer
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 ...
user avatar
0 votes
0 answers
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 ...
geeko's user avatar
  • 109
1 vote
1 answer
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: ...
yegor256's user avatar
  • 113
1 vote
1 answer
53 views

How is the direct product of the functions (A -> B) * (C -> D) equivalent to the function (A * C) -> (B * D)? Is there an error here?

In the simply typed lambda calculus we have type algebra - types can be added, multiplied and exponentiated, where addition corresponds to the sum type, multiplication to the product type, and ...
Wasabi Kurosawa's user avatar
1 vote
1 answer
61 views

On the logical and categorical interpretation of lambda calculi and type systems

There is a well-known Curry-Howard-Lambek correspondence between certain type systems, proof calculi and categories. Some variants of Barendregt's pure type systems have the property of strong ...
Wasabi Kurosawa's user avatar

1
2 3 4 5
12