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
19 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}\...
user125234's user avatar
1 vote
1 answer
36 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 \...
user125234's user avatar
1 vote
1 answer
58 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
22 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
39 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
33 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
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, ...
Danny's user avatar
  • 131
2 votes
1 answer
47 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
48 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
43 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
137 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
67 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
61 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
403 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
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 ...
LivesayEngineer's user avatar
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'...
elsewho's user avatar
  • 11
0 votes
0 answers
62 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
116 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
85 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
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} ...
Danny's user avatar
  • 131
0 votes
0 answers
24 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
286 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
47 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
3 votes
1 answer
168 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
69 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
74 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
83 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
694 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
1 vote
1 answer
35 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. ...
user253751's user avatar
  • 1,739
-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
1 vote
1 answer
171 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
73 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
64 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: $$...
tryst with freedom's user avatar
0 votes
1 answer
60 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
32 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
66 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
52 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
58 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 vote
1 answer
37 views

Example of preservation failing in Java - follow up question

This is a follow-up question to my previous question I have been reading this post and it comes up with the following example showing how Java type system is unsound: ...
Node.JS's user avatar
  • 151
1 vote
2 answers
185 views

Example of progress and preservation failing in a commonly used programming language like Java

I am wondering if my solution is correct or I am on the right track. I have searched online and found a paper about Java type system being unsound but that doesn't really answer the progress and ...
Node.JS's user avatar
  • 151
1 vote
0 answers
37 views

Simple Lambda Calculus Question [closed]

For any 2 strongly normalizing terms in the Simply Typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong ...
Abhishek Manikandan's user avatar
1 vote
0 answers
25 views

Is it possible to state strong normalization through set inclusion?

In an abstract rewriting system $\langle A, \rightarrow\rangle$, confluence may be stated by using set inclusion. Namely, a rewriting system is confluent iff ${\leftarrow^*\rightarrow^*}\ {\subseteq}\ ...
paulotorrens's user avatar
1 vote
1 answer
56 views

Instances of simulating lambda calculus?

There are a ton of resources on the web devoted to proving some esoteric language is Turing complete by simulating arbitrary turing machines. I have an esoteric language I want to prove is complete, ...
lightning's user avatar
  • 225
1 vote
0 answers
39 views

Lambda beta-reductions

I am trying to build a parser for lambda expressions. I have implemented a capture-avoiding substitution using the algorithm below ($e[d/x]$ means replace $x$ by $d$ in $e$) $x[d/x] = d$ $y[d/x] = y$ ...
Angela Riley's user avatar

1
2 3 4 5
12