Questions tagged [lambda-calculus]

Church's formal system used in computatability, programming languages and proof theory to represent effective functions, programs and their computation, and proofs.

4
votes
2answers
289 views

Is there a systematic method for constructing lambda calculus terms that can distinguish between inputs?

For example, finding terms $\vec{a}$ such that: $\vec{a}(\lambda x.x) = T\\\vec{a}(\lambda xy.x) = F$ Is there a systematic method for finding terms with these types of constraint?
14
votes
1answer
844 views

η-conversion vs extensionality in extensions of lambda-calculus

I'm often confused by the relation between η-conversion and extensionality. Edit: According to comments, it seems I'm also confused about the relation between extensional equivalence and ...
21
votes
1answer
1k views

What is the difference between arrows and exponential objects in a cartesian closed category?

In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object ...
18
votes
3answers
855 views

funsplit and polarity of Pi-types

In a recent thread on the Agda mailing list, the question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark. My understanding is that $\eta$ laws come with negative ...
9
votes
2answers
291 views

What is the benefit of Krivine's notation?

I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ ...
7
votes
3answers
338 views

Are the $\lambda_I$-Calculus and the $\lambda_K$-Calculus equivalent?

I see here and there mention of the $\lambda_I$-Calculus (in which every variable must be used at least once) and the $\lambda_K$-Calculus (in which a variable can also be unused). Are they ...
12
votes
1answer
1k views

Can Scheme's call/cc implement all known control flow structures?

The page "Advanced Scheme: Some Naughty Bits" states: Continuations are a powerful control-flow construct from which nearly any other control-flow structure [...] may be derived. I thought that ...
9
votes
1answer
402 views

A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
18
votes
2answers
531 views

Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?

I know that's impossible to decide $\beta$-equivalence for untyped lambda calculus. Quoting Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984).: If A ...
5
votes
1answer
244 views

Characterizing closure under expansion/reduction for big-step semantics?

Two common ways of formulating operational semantics for programming languages based on lambda-calculus are big-step and small-step semantics. In a big step semantics, you give a relation $e \...
18
votes
0answers
1k views

What's the expressive power of Simply Typed Lambda calculus?

The standard approach to simply typed lambda calculus considers computations over Church numerals. If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) ...
4
votes
1answer
259 views

Exponential blowup in Simple Proof of a theorem of Statman by Mairson

I'm studying "A simple proof of a theorem of Statman" by H.G. Mairson. At page 4, he encodes set/type theory in lambda calculus. In particular, note che "op" trick in the definition of $eq_{k+1}$. ...
11
votes
1answer
385 views

Extensionality of lambda calculus models

I'm translating a book on LISP and naturally it touches some elements of $\lambda$-calculus. So, a notion of extensionality is mentioned there alongside some models of $\lambda$-calculus, namely: $\...
8
votes
1answer
316 views

Reading list on rewriting systems?

I am new to studying rewriting systems as a first year PhD student. I would like to propose a special topics course on rewriting theory, and I want to make sure I don't leave any of the original ...
5
votes
2answers
608 views

Do Higher-Order Functions provide more power to Functional Programming?

My original question was: Is Kappa calculus less powerful than Lambda calculus? Does the lack of Higher-Order functions on a programming language excludes some programs that could only be written in ...
7
votes
1answer
234 views

Origin of Church encodings

In which paper did Alonzo Church first describe Church encoding? I can't find any articles that actually cite the paper, but I am interested in reading it.
3
votes
2answers
181 views

Labels for terms in the lambda calculus

In the lambda calculus, are there commonly accepted names for $x$ and $M$ when they appear in $\lambda x [M]$ ? Something along the lines of "binder" and "bindee"?
15
votes
1answer
909 views

Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
11
votes
6answers
1k views

What is the point of calling $\lambda$-calculus an algebra?

What is the difference of calling $\lambda$-calculus an algebra instead of a calculus? I raise this question because I read somewhere the line "$\lambda$-calculus is not a calculus but an algebra" (...
-6
votes
1answer
248 views

Lambda Calculus - are these two expressions equivalent? [closed]

(λa.(λb.λc.b)) and (λa.λb.λc.b) I was wondering if someone could explain, using mostly English, what that lambda-calculus expression is supposed to mean, and whether there is any difference between ...
3
votes
2answers
343 views

Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?

Normal Order Reduction (NOR) reduce the leftmost, outermost redex. Normal Order Evaluation (NOE) reduce the leftmost, outermost redex, but not within the body of abstractions. So (λw. (λx.x) z) is ...
12
votes
6answers
2k views

Functions that typed lambda calculus cannot compute

I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi. As I am a beginner, some reiteration of background information ...
7
votes
1answer
253 views

How to define eta-equivalence for F-omega types?

There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus: via a plain relation $t_1 = t_2$, via an indexed relation $\Gamma \vdash t_1 = t_2 : T$...
1
vote
1answer
333 views

Can “$x(\lambda y.P\;)z$” be $\beta$-reduced?

Consider the untyped $\lambda$-calculus expression $$x(\lambda y.P\;)z$$ ...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex. Can this expression be $\beta$-reduced? I've ...
6
votes
1answer
373 views

Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus

I'm trying to work through two (non-assessed) class-work questions and am stuck on a question that seems similar to one I could do. The first question was to prove that there does not exist a $\...
13
votes
1answer
411 views

Lambda-Calculus terms that reduce to themselves

In my continuing quest to try to learn lambda calculus, Hindley & Seldin's "Lambda-Calculus and Combinators an Introduction" mentions the following paper (by Bruce Lercher) which proves that the ...
5
votes
3answers
667 views

Why does predecessor(zero) need to be zero in Church numerals?

My question may be similar to: Why naturals instead of integers?, but it is more specific. I am trying to learn lambda calculus. All the books make a big deal about how it was necessary that ...
7
votes
2answers
811 views

Closed term and alpha-conversion

In the simply-typed lambda calculus, do we ever need alpha-conversion in a small-step call-by-value reduction of a term that is closed? The evaluation rule that uses substitution is: $(\lambda x.t_1)~...
12
votes
1answer
374 views

Barendregt's proof of subject reduction for $\lambda2$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types). The last step of the proof (page 60), says: "and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\...
15
votes
3answers
868 views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
18
votes
4answers
3k 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 ...
7
votes
2answers
294 views

Simple model of computation with homoiconicity

Is there a simple model of computation with homoiconicity? It would also be nice if, like beta reduction in lambda calculus, every step in execution yields a new valid program. Besides the lack of ...
6
votes
0answers
417 views

What is the origin and meaning of the phrase “Lambda the ultimate?”

I've been messing around with functional programming languages for a few years, and I keep encountering this phrase. I understand what lambda means, the idea of an anonymous function is both simple ...
9
votes
1answer
442 views

What is the role of the Bicolored Calculus of Constructions?

So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ ...
-3
votes
1answer
313 views

Did someone give a formal definition of normal and applicative order?

In all courses and textbooks I have seen, normal order reduction (NOR) and applicative order reduction (AOR) are defined as reducing respectively the leftmost outermost and rightmost innermost redex. ...
9
votes
2answers
428 views

Are a few hundred reduction steps too many to get the normal form of Y fac ⌜3⌝?

As I have been teaching the basis of λ-calculus lately, I have implemented a simple λ-calculus evaluator in Common Lisp. When I ask the normal form of Y fac 3 in ...
10
votes
1answer
165 views

Reference for the undefinability of modulus of continuity functional in PCF?

Can someone point me to the reference for the non-definability of the modulus of continuity functional in PCF? $\newcommand{\N}{\mathbb{N}}$ $\newcommand{\bool}{\mathsf{bool}}$ Andrej Bauer has ...
13
votes
2answers
428 views

What are the equational laws for zero types?

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory. In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator: $$\frac{\...
7
votes
2answers
757 views

Translation from basic While-language to $\lambda$-calculus

Is there a simple way to translate programs written in a basic "While" language (such as Winskels Imp)? I know about Church numerals and booleans, and I can see how if and while statements can be ...
18
votes
3answers
2k views

Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
14
votes
1answer
418 views

Are innermost reductions perpetual in untyped λ-calculus?

(I have already asked this at MathOverflow, but got no answers there.) Background In the untyped lambda calculus, a term may contain many redexes, and different choices about which one to reduce may ...
26
votes
4answers
1k views

Is there a non Turing-complete model of computation whose halting problem is undecidable?

I cannot think of any such model, maybe some form of typed lambda calculus? some elementary cellular automaton? This would almost disprove Wolfram's "Principle of Computational Equivalence": ...
15
votes
2answers
438 views

Are there intermediate eta theories for the lambda calculus?

There are two main, studied theories of the lambda calculus, the beta theory and its Post-complete extension, the beta-eta theory. Do these two theories have an in-between, a kind of intermediate eta ...
48
votes
2answers
7k views

Realizability theory: difference in power between Lambda calculus and Turing Machines

I have three related subquestions, which are highlighted by bullet points below (no, they could not be split, if you are wondering). Andrej Bauer wrote, here, that some functions are realizable ...
6
votes
3answers
737 views

What does it mean that there are differing views on how computations are represented on the Turing Machine?

For a given algorithm (eg reverse the items in this list) and a given type of Turing machine (eg the 3-state 2-symbol busy beaver reduced to 5-tuples) - is there a single simplest way that this ...
11
votes
2answers
420 views

Does the System F with pairs have the strong normalisation and subject reduction properties?

It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not ...
45
votes
5answers
18k views

Relationship between Turing Machine and Lambda calculus?

Is there a relationship between the Turing Machine and the Lambda calculus - or did they just happen to arise about the same time?
18
votes
3answers
2k views

Why can Lambda Calculus not represent some combinators?

This paper suggests that there are combinators (representing symbolic computations) that can not be represented by the Lambda calculus (if I understand things correctly):
14
votes
1answer
269 views

Characterising invisible equivalences by confluent rewrite rules

In response to another question, Extensions of beta theory of lambda calculus, Evgenij offered the answer: beta + the rule {s = t | s and t are closed unsolvable terms} where a term M is solvable if ...
43
votes
7answers
3k views

Using lambda calculus to derive time complexity?

Are there any benefits to calculating the time complexity of an algorithm using lambda calculus? Or is there another system designed for this purpose? Any references would be appreciated.