The lambda-calculus tag has no wiki summary.
7
votes
0answers
69 views
η-conversion vs extensionality in extensions of lambda-calculus
I'm often confused by the relation between η-conversion and extensionality.
In the untyped lambda-calculus, the eta-rule gives the same proof system as the extensionality rule, as proven by ...
0
votes
0answers
68 views
What is, exactly, $\lambda$-calculus? [migrated]
I'm starting an undergraduate computer science course next fall, but I can't really understand λ-calculus in the context of functional programming. I may be misinterpreting this completely, but based ...
9
votes
1answer
152 views
What is the difference between arrows and exponential types in the 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 ...
12
votes
3answers
321 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
...
6
votes
1answer
120 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$ ...
4
votes
3answers
137 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 ...
11
votes
1answer
345 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 ...
9
votes
1answer
109 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 ...
14
votes
2answers
203 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
157 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 ...
6
votes
0answers
207 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) ...
2
votes
1answer
152 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}$.
...
9
votes
1answer
201 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 with some models of $\lambda$-calculus, namely: ...
7
votes
1answer
216 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
438 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 ...
6
votes
1answer
163 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
144 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"?
8
votes
0answers
359 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.
...
10
votes
6answers
622 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" ...
-7
votes
1answer
148 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
291 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 ...
5
votes
6answers
1k 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
141 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 : ...
1
vote
1answer
286 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
228 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 ...
10
votes
1answer
241 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
377 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
640 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 ...
12
votes
1answer
219 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), ...
12
votes
3answers
439 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 ...
10
votes
4answers
703 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 ...
6
votes
2answers
244 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
284 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 ...
6
votes
1answer
237 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
216 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
367 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 ...
9
votes
1answer
139 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 ...
12
votes
2answers
319 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:
...
7
votes
2answers
536 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 ...
9
votes
3answers
524 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 ...
12
votes
1answer
298 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 ...
16
votes
2answers
644 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":
...
12
votes
2answers
316 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.
Is there something in between these two theories, a kind of ...
13
votes
2answers
982 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 ...
4
votes
3answers
412 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 ...
10
votes
2answers
322 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 ...
14
votes
5answers
3k 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?
12
votes
3answers
710 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):
13
votes
1answer
223 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 ...
22
votes
6answers
1k 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.
