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.
273
questions
2
votes
0
answers
81
views
When is an upper bound on the longest irreducible program outputting something computable?
This is a repost of this mathoverflow question.
Given some way to to encode programs to strings with a finite alphabet, which we assume has a computable translation to/from Turing machines, a program ...
- 567
1
vote
1
answer
122
views
Are Turing Machines Models?
I am wondering whether it is correct to say that Turing machines are models of, say, the lambda calculus, in the model theoretical sense. Lambda calculus and Turing machines are equivalent ...
6
votes
1
answer
121
views
Are there any books or articles that contain information on the P weak omega or second order predicate calculi?
I have been trying to learn about the lambda cube, but cannot find any sources covering the P weak omega and P2 nodes. Is the problem that these nodes are not frequently used/ offer little benefits ...
- 14k
5
votes
2
answers
218
views
An untyped lambda calculus for explicit memory management
I am trying to find resources on a lambda calculus one would use for explicit memory management, assuming there is such a calculus.
The concept is as follows: one takes untyped lambda calculus, ...
6
votes
0
answers
71
views
Böhm tree with pairs (product types)
I am looking for references for a notion of Böhm tree for the λ-calculus with pairs and projections (and the reduction rule $\pi_i\, \langle t_1, t_2\rangle \longrightarrow t_i$).
I'm only aware of ...
15
votes
3
answers
585
views
(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?
From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to ...
- 2,786
8
votes
1
answer
225
views
deciding $\beta$-equality of planar lambda terms
Mairson showed that the problem of computing the $\beta$-normal form of a linear lambda term (or equivalently, computing its principal type) is complete for polynomial time.
Harry Mairson. Linear ...
2
votes
2
answers
297
views
Algorithm for extensional equality in combinator calculus
I'm dealing with combinator calculus, using the $S$ and $K$ combinators as a basis. Sometimes my code generates expressions that define equivalent functions, such as
$$
(S\, K\, K) \qquad\text{and}\...
- 121
3
votes
1
answer
142
views
Is there a full abstraction result for an untyped lambda calculus?
Famously, the denotational semantics of PCF in Scott domains is not fully abstract. But by adding the parallel or construct to PCF, a fully abstract semantics can be obtained.
Is there an analogous ...
2
votes
2
answers
343
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 ...
- 161
6
votes
1
answer
2k
views
Is a CEK machine an implementation of a CESK machine?
We know that a CESK machine can be defined as:
a state-machine in which each state has four components: a (C)ontrol component, an (E)nvironment, a (S)tore and a (K)ontinuation. One might imagine ...
- 103
2
votes
1
answer
131
views
Is beta normalization used for program optimization?
Beta normalization reduces a lambda term to its beta normal form, if it exists. The beta normal form is a computationally equivalent term with no "redundant" computation, in a sense; for ...
11
votes
2
answers
388
views
What are pertinent references to cite on Scott domains?
Scott domains are often presented as having been introduced in 1969. However, the first (but numerous!) papers are from the 1970s, so it is not easy to know what the pertinent references are. My two ...
- 509
7
votes
3
answers
682
views
Example of a term in system F which is not typable in the simply typed lambda calculus
What is the simplest possible example of a (correctly typed) term in system F that does not correspond to any correctly typed term in the simply typed λ-calculus?
More precisely, I am looking for a ...
- 5,598
21
votes
3
answers
2k
views
Smallest possible universal combinator
I am looking for the smallest possible universal combinator, measured by the number of abstractions and applications required to specify such a combinator in the lambda calculus. Examples of universal ...
- 281
2
votes
0
answers
97
views
Variable opening in locally-nameless representation
Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's ...
- 121
4
votes
1
answer
215
views
Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic
What is the precise connection between:
strong normalization of the simply typed $\lambda$-calculus, and
cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent ...
- 317
4
votes
1
answer
387
views
Locally-nameless normalization
This paper on locally-nameless (Charguéraud, Arthur: The locally nameless representation, Journal of Automated Reasoning (2012): 1-46) describes how to perform beta-reduction by "opening", but it's ...
- 14k
0
votes
0
answers
97
views
Can lambda-calculus, or other formal systems / calculi, be represented using set theory?
Background: I'm a fresh grad student looking into interesting ideas I have. I do not have any theoretical computer science background beyond basic Theory of Computation stuff from undergrad.
If I have ...
- 171
-1
votes
1
answer
88
views
What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?
I was given an exercise that asked me to assign a simple type to the lambda term:
$$
\lambda a.a(\lambda yt.t)(ya)
$$
but I couldn't find one, furthermore, the lambda term seems untypable to me ...
- 509
-1
votes
1
answer
210
views
Locally nameless representation implementation
ORIGINAL: I am programming a functional compiler and found out about locally nameless representation (using de brujin indeces for bound variables and names for free variables). I just don't understand ...
- 9
4
votes
1
answer
164
views
Is there a standard way to "point" at subterms in a lambda expression?
Let's say I have a lambda expression
$$ (\lambda x . (\lambda w.ww)x) y $$
There are a bunch of subterms:
$(\lambda x . (\lambda w.ww)x) y$
$\lambda x . (\lambda w.ww)x$
$(\lambda w.ww)x$
$\lambda w ....
- 1
-1
votes
1
answer
139
views
Is it necessary to apply alpha conversion in this term to perform beta reduction in lambda calculus?
I am trying to prove that the expression ((λx.(λx.x))(ab)) does not require alpha conversion for beta reduction since there is no variable overlap, but how could I demonstrate this more formally?
- 509
4
votes
0
answers
325
views
How to prove that a language that allows infinite loops is still not Turing-complete?
CPS translations will always use pairs, either explictly or by currying. Though I can't find a reference for that, I'm assuming this is a necessary condition (I'd appreciate a reference if someone has ...
- 387
10
votes
1
answer
619
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 ...
- 14k
1
vote
1
answer
107
views
Intuition behind UTT's internal logic
The "internal logic" of type theory UTT is defined in LF as follows:
What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
- 29.4k
2
votes
1
answer
589
views
Is classical lambda calculus grammar an `LL(k)` one?
I am playing with a lambda calculus and faced a question I find hard to reason about.
On the screenshot you may find the lambda calculus grammar. Is it an instance of the ...
- 283
10
votes
1
answer
178
views
What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?
I've seem two different notions of operational equivalence being used for the $\lambda$-lalculus, i.e., an equivalence stating that "if we replace term $a$ with a term $b$ in a program, the ...
- 387
5
votes
2
answers
366
views
Lambda-calculus: Beta-equivalent terms have the same type
In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type?
My guess is that I should use the subject reduction, and maybe the ...
- 5,598
1
vote
0
answers
94
views
Is it possible to define beta reduction for PHOAS?
I'm using Parametric Higher-Order Abstract Syntax (PHOAS) as a representation for untyped lambda calculus in OCaml:
...
- 105
0
votes
0
answers
155
views
On the use of Turing machines for computational complexity
Almost always in the study of computational complexity, the Turing machine is used as a model. On the other hand, the untyped lambda calculus is in a sense "simpler" than any Turing machine: ...
21
votes
1
answer
2k
views
Why it's impossible to declare an induction principle for Church numerals
Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way:
...
- 29.4k
0
votes
0
answers
95
views
Simple Lambda Calculus Question
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 ...
44
votes
3
answers
7k
views
P and NP classes explanation through lambda-calculus
In the introduction and explanation P and NP complexity classes often given through Turing machine.
One of the model of computation is the lambda-calculus.
I understand, that all of models of ...
7
votes
1
answer
514
views
The precise definition of Normalization By Evaluation?
The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language:
The ...
- 32.8k
5
votes
2
answers
284
views
Complexity of convertibility in simply typed λ-calculus with sums
For the simply typed λ-calculus with only the function type →, the complexity of deciding βη-equivalence is well-understood: it's TOWER-complete (as mentioned here). I expect the same should be true ...
- 2,040
24
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) ...
9
votes
1
answer
461
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 ...
2
votes
1
answer
94
views
Nominal Tree Languages i.e. with Binders and Infinite Symbols?
I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence.
I've found so far:
...
23
votes
4
answers
1k
views
Can typed lambda calculi express *all* algorithms below a given complexity?
I know that the complexity of most varieties of typed lambda calculi without the Y combinator primitive is bounded, i.e. only functions of bounded complexity can be expressed, with the bound becoming ...
1
vote
0
answers
69
views
Interpretation of the degree of a redex
In Girard Proofs and Types, The degree of a type is defined as follows
$$\begin{align*}\partial(T_i)&=1\text{ if }T_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &=\max(\...
- 11
0
votes
1
answer
220
views
2
votes
0
answers
150
views
How to implement the next type inference algorithm?
Here I mean only simple typed Lambda calculus / Combinatory logic.
Notation: Combinatory logic terms: $F, X_i, Y_i$. Term application: $(F*X_1)$. Type variables $x_i,y_i$. Type assignment: $X:x_i$.
...
- 11.5k
17
votes
2
answers
2k
views
How is Lambda Calculus a specific type of Term Writing system?
Church was associated with the Simply Typed Lambda Calculus. Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda Calculus.
When John ...
- 29.4k
8
votes
1
answer
398
views
What are the application of Scott-Topology in theoretical computer science?
During a work I came across the Scott-Topology and I see that Scott-continuous functions show up in the study of models for lambda calculi. What I cannot understand is how this enrich the lambda-...
- 11.5k
2
votes
2
answers
533
views
What is the computational power of the Calculus of Constructions?
The calculus of constructions (CoC) without fix is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: ...
- 1,639
2
votes
1
answer
80
views
Question about "Free-ness" of Free SCWF
In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF.
My ...
- 1,695
1
vote
1
answer
77
views
Question in relating STLC and Free CCC
In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph)
My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
- 133
3
votes
0
answers
111
views
Call-by-value solvability
Background
There are two fairly common definitions of solvability. The general one states that the term can be used to get any chosen result (i.e. normal form):$$T\text{ solvable} \overset{\text{def}}{...
- 556
2
votes
1
answer
192
views
Intuitive way to handle variable binding
Suppose we have an algebraic datatype parameterised by a type variable name, e.g.
...
- 29.4k