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.
269
questions
3
votes
1
answer
121
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 ...
1
vote
1
answer
59
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 ...
10
votes
2
answers
348
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 ...
7
votes
3
answers
615
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 ...
2
votes
1
answer
110
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 ...
4
votes
1
answer
176
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 ...
2
votes
0
answers
87
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 ...
0
votes
0
answers
87
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 ...
-1
votes
1
answer
81
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 ...
-1
votes
1
answer
141
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 ...
-1
votes
1
answer
95
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?
4
votes
0
answers
315
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 ...
1
vote
1
answer
91
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 - ...
2
votes
1
answer
559
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 ...
1
vote
0
answers
71
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:
...
5
votes
2
answers
332
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 ...
0
votes
0
answers
147
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: ...
0
votes
0
answers
91
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 ...
7
votes
1
answer
379
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 ...
5
votes
2
answers
264
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 ...
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(\...
0
votes
1
answer
202
views
Fixed-point combinator on arithmetic functions
The question is about this Racket program:
...
2
votes
0
answers
147
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$.
...
2
votes
2
answers
409
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: ...
2
votes
1
answer
79
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
vote
1
answer
69
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 ...
4
votes
1
answer
158
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 ....
8
votes
1
answer
317
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-...
3
votes
0
answers
107
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}}{...
9
votes
1
answer
163
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 ...
2
votes
1
answer
176
views
Intuitive way to handle variable binding
Suppose we have an algebraic datatype parameterised by a type variable name, e.g.
...
3
votes
0
answers
83
views
Expressive power of lambda-calculus with restricted application
Consider a syntactic restriction of the (untyped) $\lambda$-calculus in which an application cannot have another application as an immediate subterm. More precisely, restricted terms ($R,S,...$) and ...
2
votes
0
answers
66
views
Are there any references for this theorem of Lercher?
Let $\Delta = \lambda x.(x)x$ and consider $\Omega = (\Delta)\Delta$. Then $\Omega$ is exactly the only $\lambda$-term of the form $(\lambda x.t)v$ such that $(\lambda x.t)v=t\{v\ /\ x\}$.
Does ...
5
votes
1
answer
90
views
Can a normal form term be extensionally equivalent to a term with no WHNF?
For convenience I'm using using the combinators SKIBCMTV
I notice that it's possible to have a normal-form term extensionally equivalent to a term which has no normal form:
...
0
votes
0
answers
168
views
What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?
There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ...
7
votes
0
answers
139
views
Are the non-lazy / non-weak semantics of the $\lambda$-calculus related to weak evaluation?
Vague question
The most common semantics of the call-by-name $\lambda$-calculus (Hyland/Wadsworth’s observational equivalence $\approx_\text{HNF}$ and Morris’s observational equivalence $\approx_\text{...
1
vote
0
answers
102
views
Is there some n such that lambda calculus with only n variables is Turing-complete?
Typically in lambda calculus you have an infinite stock of variables. Could we get away with a finite set?
8
votes
0
answers
189
views
$\lambda$-definability and structure preserved by homomorphisms
I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it.
Some prelimary definitions.
A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for ...
3
votes
1
answer
349
views
Fixed points of fixed-point combinator?
A fixed point f of a fixed-point combinator would be a function that has itself as a fixed point: f(f) = f. The only such ...
5
votes
1
answer
151
views
$\eta$-reduction not locally confluent on well-typed terms
This paper says: "In the presence of a unit type, $\eta$-reduction is not even locally confluent on well-typed terms [20]."
[20] is a reference to a 300-page book with no further details and ...
10
votes
0
answers
218
views
What is the "standard" lambda-calculus model for bicartesian closed categories?
(I'm familiar with the lambda-calculus, less so with its categorical models.)
It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
5
votes
1
answer
262
views
Alternatives to Normalization by Evaluation
Reading about lambda calculus I got the impression that normalization is evaluation.
So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel).
...
3
votes
2
answers
548
views
Are there strongly normalizing lambda terms that cannot be given a System F type?
I know that all well-typed System F terms are strongly normalizing, but is the converse true as well? In other words, does System F typeability precisely characterize program termination? (And if so, ...
2
votes
1
answer
109
views
Typing inference as a map on abstract syntax trees
Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-...
3
votes
0
answers
106
views
CCCs, computational calculi and point-surjectivity
The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $U$ that has some relationship to its exponential object $U^U$ e.g. a retraction ...
4
votes
1
answer
164
views
Structural normalization algorithm for the simply typed lambda calculus
I would like to know if there is a (piecewise) structural normalization algorithm for the simply typed lambda calculus. By structural I mean a recursive function that only calls itself on subterms of ...
2
votes
1
answer
85
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:
...
2
votes
1
answer
145
views
Phonology and lambda calculus
I wonder whether there is any relationship between lambda calculus and phonology (study of phonemes). Specifically, how one would use the concepts of lambda calculus (typed or untyped) in the study of ...
5
votes
0
answers
174
views
Applications of solvability in the λ-calculus
What are applications of solvability / unsolvability, and of operational characterizations of solvability?
Solvability
In the (untyped pure call-by-name) $\lambda$-calculus, a closed term is said to ...
17
votes
1
answer
1k
views
Can we derive Cubical Type Theory from Self-Types?
Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...