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.

202 questions
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?
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 ...
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 ...
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 ...
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$ ...
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 ...
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 ...
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 ...
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 ...
244 views

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}$. ...
385 views

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 ...
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 ...
811 views

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 ...
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 ...
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 ...
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 ...
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}$ ...
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. ...
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 ...
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 ...
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{\...
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 ...
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 ...
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 ...
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": ...
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 ...
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 ...
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 ...
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 ...
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?
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):