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 ...
- 307
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
4
votes
1
answer
357
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 ...
- 13.7k
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 ...
- 199
-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
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 ....
- 1
-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?
- 199
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
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 ...
- 13.7k
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 - ...
- 28.3k
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 ...
- 221
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
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 ...
- 5,273
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
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: ...
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:
...
- 28.3k
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 ...
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 ...
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 ...
- 32.4k
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 ...
- 2,040
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) ...
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 ...
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:
...
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
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$.
...
- 11.4k
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 ...
- 28.3k
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-...
- 11.4k
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: ...
- 1,444
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 ...
- 1,653
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
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
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.
...
- 28.3k
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{...
- 307
7
votes
1
answer
132
views
Semantic read-back of sharing graphs
A "sharing graph" is a representation of a $\lambda$-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound. They are used ...
10
votes
2
answers
571
views
Is there an efficient beta-equivalence algorithm?
Is there an efficient algorithm to determine if two terms are beta-equivalent? Specifically, I am curious about simply-typed-lambda-calculus, so you can assume both terms are strongly normalizing.
I ...
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
12
votes
1
answer
484
views
Incomplete basis of combinators
This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete?
I believe the answer is ...
- 4,431
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
3
votes
2
answers
593
views
Constructing terms of function types out of the empty type
If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we ...
- 111
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 ...
- 5,273
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 ...
- 32.4k
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