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.
265
questions
4
votes
0
answers
466
views
Defining a calculation-reversing function in the lambda calculus
Obviously, lambda calculus functions are not in general invertible. That is, there is no lambda function $V$ (for inVerse) such that
$$
(V\; A)\; (A\; B) \to B
$$
for every $A$ and $B$ such that $(A\; ...
- 699
21
votes
1
answer
622
views
A Lambda calculus for invertible (r-Turing computable) functions
I'm interested in the concept of "r-Turing completeness", as defined by Axelsen and Glück (2011). A system is r-Turing complete if it can compute the same set of functions as a reversible Turing ...
- 699
-2
votes
1
answer
473
views
Are two unbound variables alpha-equivalent? [closed]
Let's say we have the following cases:
$a =_\alpha b$
$a =_\alpha a$
Which of the above cases are $\alpha$-equivalent? Or does $\alpha$-equivalence has no meaning in the context of just variables? ...
- 147
12
votes
3
answers
2k
views
How to make the Lambda Calculus strong normalizing without a type system?
Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
- 3,117
2
votes
0
answers
190
views
Evaluation contexts: outside-in vs inside-out
I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
- 2,775
9
votes
3
answers
4k
views
Implementation of alpha equivalence
I'm reading through "Type Theory & Functional Programming" by Simon Thompson and it says
We shall not distinguish between expressions which are equivalent up to change of bound variable names ...
- 201
15
votes
2
answers
2k
views
Why is lambda calculus a "calculus"?
The only definition of "calculus" I'm aware of is the study of limits, derivatives, integrals, etc. in analysis. In what sense is lambda calculus (or things like mu calculus) a "calculus"? How does it ...
- 269
5
votes
1
answer
194
views
Is combinatory strong reduction equivalent to lambda beta-eta reduction?
I'm familiar with the correspondence between combinatory logic and $\lambda$-calculus at equality level, ie $=_{\beta\eta}$ corresponds to $=_s$ (the equivalence relation generated by strong reduction)...
- 51
9
votes
1
answer
415
views
Regular languages in lambda calculus
With Turing machines, by imposing certain restrictions on the form of the transition function, one can get a machine that accepts only regular languages. I am wondering what is the counterpart in ...
- 296
3
votes
2
answers
906
views
Is there a space efficient way to represent numbers on the lambda calculus?
This is something I've been thinking. While it is agreed that Lambda Calculus is equivalent to a Turing Machine in power, is it actually so? Church Numerals are not very space efficient and I'm not ...
- 3,117
1
vote
3
answers
393
views
"lambda" term usage in programming
could any one please let me know what is the relation between "lambda" and anonymous functions in programming?
in other words why we say lambda function to an anonymous function?
I am here trying to ...
- 145
1
vote
1
answer
265
views
A few questions about ISWIM
I recently read Landin's paper "The Next 700 Programming Languages". But I was a bit confused by ISWIM. In particular, are functions first-class objects in ISWIM? It seems not because every ...
- 2,775
8
votes
8
answers
8k
views
What are the simplest turing-complete systems? [closed]
Lambda Calculus is very simple. Are there even simpler turing-complete systems? Which is the simplest of them all?
- 121
4
votes
2
answers
373
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?
- 43
14
votes
1
answer
1k
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 ...
- 2,049
22
votes
1
answer
2k
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 ...
- 2,775
18
votes
3
answers
1k
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
...
- 478
9
votes
2
answers
340
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$ ...
- 2,775
9
votes
3
answers
506
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 ...
- 2,775
13
votes
1
answer
2k
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 ...
- 133
10
votes
1
answer
599
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 ...
- 2,571
18
votes
2
answers
781
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 ...
- 2,571
5
votes
1
answer
271
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 \...
- 32.4k
25
votes
1
answer
2k
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) ...
- 411
4
votes
1
answer
371
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}$.
...
- 411
11
votes
1
answer
524
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: $\...
- 113
9
votes
1
answer
351
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
2
answers
669
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 ...
- 161
9
votes
1
answer
272
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.
- 193
3
votes
2
answers
193
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"?
- 133
16
votes
1
answer
1k
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.
...
- 261
16
votes
6
answers
2k
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" (...
- 2,775
-6
votes
1
answer
260
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 ...
- 11
3
votes
2
answers
425
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 ...
- 149
13
votes
6
answers
3k
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 ...
- 201
7
votes
1
answer
327
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,310
1
vote
1
answer
343
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 ...
- 531
6
votes
1
answer
436
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 $\...
14
votes
1
answer
509
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 ...
- 191
5
votes
3
answers
876
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 ...
- 191
8
votes
2
answers
971
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)~...
- 181
12
votes
1
answer
459
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\...
- 701
16
votes
3
answers
1k
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 ...
user6892
23
votes
4
answers
4k
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 ...
- 604
9
votes
3
answers
415
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 ...
oozer
6
votes
0
answers
425
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 ...
- 263
9
votes
1
answer
568
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}$ ...
- 710
-3
votes
1
answer
327
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. ...
- 195
9
votes
2
answers
461
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 ...
- 195
10
votes
1
answer
193
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 ...
- 32.4k