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
1
answer
142
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 ...
- 619
2
votes
0
answers
42
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
0
votes
0
answers
79
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 ...
- 129
-1
votes
1
answer
74
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
124
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
-1
votes
1
answer
73
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
309
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 ...
- 377
1
vote
1
answer
82
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 - ...
- 125
2
votes
1
answer
535
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 ...
- 212
1
vote
0
answers
64
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:
...
- 73
5
votes
2
answers
324
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 ...
- 381
0
votes
0
answers
139
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
89
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 ...
6
votes
1
answer
305
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 ...
- 73
5
votes
2
answers
255
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
67
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
190
views
2
votes
0
answers
144
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$.
...
- 121
2
votes
2
answers
353
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: ...
- 23
2
votes
1
answer
78
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 ...
- 133
1
vote
1
answer
60
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
4
votes
1
answer
156
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 ....
- 143
7
votes
1
answer
285
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-...
- 81
3
votes
0
answers
104
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
9
votes
1
answer
154
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 ...
- 377
2
votes
1
answer
171
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
79
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 ...
- 653
2
votes
0
answers
64
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 ...
- 121
5
votes
1
answer
88
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:
...
- 916
0
votes
0
answers
163
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 ...
- 3,117
7
votes
0
answers
137
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{...
- 556
1
vote
0
answers
99
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?
- 119
7
votes
0
answers
186
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 ...
- 443
3
votes
1
answer
321
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 ...
- 143
5
votes
1
answer
141
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 ...
- 61
10
votes
0
answers
212
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 ...
- 2,040
5
votes
1
answer
253
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).
...
- 59
3
votes
2
answers
503
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, ...
- 212
2
votes
1
answer
107
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-...
user61651
3
votes
0
answers
104
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
161
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 ...
- 185
2
votes
1
answer
83
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,830
2
votes
1
answer
142
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
164
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 ...
- 556
16
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&...
- 3,117
1
vote
0
answers
81
views
What is the time complexity of substitution algorithms(normalization by evaluation, explicit subtitution)?
I'm studying the substitution algorithms of lambda calculus. I think now I understand how they work, but I couldn't find any materials about their time complexity yet.
This is what I've thought about ...
- 119
-2
votes
1
answer
81
views
Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs
Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union.
For example, $S$ ...
- 105
0
votes
0
answers
87
views
Is this a reader monad?
I'm unsure whether the following three equations constitute a valid instance of a reader/environment monad on the simply-typed lambda calculus, where $\alpha$ is any type (I subscript some terms with ...
- 105
7
votes
0
answers
234
views
Category theory lambda cube?
If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to?
https://en.m.wikipedia.org/wiki/Lambda_cube
- 163
5
votes
2
answers
252
views
Categorical equivalent of higher order logic
From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.
- 921