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.
64
questions with no upvoted or accepted answers
14
votes
0
answers
419
views
Are there simple core languages which are consistent and expressive?
The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
- 3,117
14
votes
0
answers
257
views
historical question: earliest description of beta-normal terms together with "neutral" terms in lambda calculus?
A bit of "folklore" in lambda calculus is the idea of characterizing the class of $\beta$-normal terms inductively as a syntactic category ($R$) defined in mutual induction with an auxiliary syntactic ...
- 4,431
11
votes
0
answers
304
views
A bijection between ordered lambda terms and rooted planar maps?
Consider the following recurrence in two parameters $n$ and $k$:
\begin{aligned}
NF(0,k) &= 0 \\
NF(n,k) &= Neu(n,k) + NF(n-1,k+1) \\
Neu(n,k) &= [n=1 \wedge k=1] + \sum_{l=1}^{n-1}\sum_{...
- 4,431
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
10
votes
0
answers
420
views
Typed Lambda Calculus models and denotations
I'm trying to draw a general mental picture about the models and the
denotational semantics of the typed lambda calculus, in its different
variants.
I'm particularly interested in how the semantics ...
- 668
8
votes
0
answers
65
views
Relationship between lambda-definability, specification and definability in model theory
I am new to lambda calculus and definability theory, and I am trying to clarify my understanding of the relationship among the following concepts:
An element $a$ in the domain of a type $A_\sigma$ is ...
- 243
8
votes
0
answers
179
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 ...
- 4,431
8
votes
0
answers
362
views
Denotational semantics of System $F_\omega$ with recursive types and general recursion
Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion?
I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]...
- 161
8
votes
0
answers
95
views
Decidability of equality between higher-kinded equirecursive types (or: between nonregular Böhm trees)
In §3 of Polytypic values possess polykinded types, Ralf Hinze described a calculus of types with higher-kinded recursive types. There is a fixed-point combinator $$\mu_\kappa : (\kappa \rightarrow \...
- 161
8
votes
0
answers
507
views
Complete combinator basis for System F-omega
The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
- 1,141
8
votes
0
answers
181
views
Equivalence of categories of directed complete posets
I asked this question there: https://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets.
Since I had no answer, I try here.
In the book ``Domains and Lambda-...
- 181
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
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
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
6
votes
0
answers
166
views
Locally-nameless representation: normal order & opening with a bound variable
This question concerns the representation used in Arthur Charguéraud's paper “The locally nameless representation” and is somehow a follow-up on this question, where it is asked about the ...
- 229
6
votes
0
answers
148
views
Is higher-order unification decidable for terms without abstractions within applications?
Consider the problem of higher order unification - that is, finding a substitution for the equation a = b, where a and ...
- 3,117
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
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
5
votes
0
answers
167
views
Upward confluence in the interaction calculus
The lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations $c_1$ and $c_2$ such ...
5
votes
0
answers
104
views
Characterisation of the BCIW definable functions
Given a full model of the simply typed lambda calculus, it's possible to characterise the lambda definable functions as those that are invariant under every "Kripke logical relation". (See here.)
I ...
- 443
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
4
votes
0
answers
118
views
Proof that CIC or Dybjer-style eliminators are strongly-normalizing?
Related to this question
I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
- 2,830
4
votes
0
answers
169
views
Hereditary Substitution with Inductives and Eliminators?
I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators?
In particular, normalizing the application of an eliminator to an ...
- 2,830
4
votes
0
answers
519
views
Is it possible to derive induction by extending CoC with recursion?
Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms:
...
- 3,117
4
votes
0
answers
86
views
Can any Calculus of Construction term be built up from application of a finite number of terms?
Can we form a finite set of well typed calculus of construction terms such that any closed term can be built up from them (plus the type of large types) using only application?
I conjecture that the ...
- 471
4
votes
0
answers
65
views
Finite intersection property of polymorphic type families
Let $\Phi$ be a type functor definable in polymorphic lambda calculus:
$$ \alpha : * \vdash \Phi(\alpha) : * $$
$$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$
Suppose further ...
- 611
4
votes
0
answers
341
views
Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking
I need an extension of System $F_\omega$ with subtyping, and where the variance of type constructors is reflected in their kind. Unfortunately, System $F^\omega_{<:}$, as defined in chapter 31 of ...
- 501
4
votes
0
answers
266
views
Is it possible to implement tail recursion inside a lambda calculus built on top of functions?
Inside a lambda calculus implementation for ECMASCript 6, we are trying to implement new constructs such as type tags for strong typing, and conditionals such as the ...
- 141
4
votes
0
answers
67
views
Is the question about closed reduction using token-passing nets still open?
The question about possible implementation of closed reduction using token-passing nets is asked on page 17 in Token-passing Nets for Functional Languages by Jose Bacelar Almeida, Jorge Sousa Pinto, ...
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
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
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
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
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 ...
3
votes
0
answers
134
views
Would it be possible to derive `transp` natively from Path, Interval and typecase?
Assume for a moment that we extended Agda with an Interval and a Path type, but not transp (which is a primitive currently). I'm ...
- 3,117
3
votes
0
answers
154
views
Set:Set or Negative Inductives in a Total Language?
In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (...
- 2,830
3
votes
0
answers
166
views
Type System Of $\lambda\mu$-Calculus
reading this paper on CPS-tranformation from the $\lambda\mu$-calculus, I'm a bit confused about the type system presented:
Why second-order formulas in the types? Is this according to the Curry-...
- 139
3
votes
0
answers
117
views
Metrics for modelling convergence in the lambda-calculus
I wonder if there have been efforts to reconcile the measure approach to termination and Scott's domain theory or other topological models of computation. In other words, can we translate this measure ...
- 921
3
votes
0
answers
395
views
Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?
If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack.
For example:
...
- 701
3
votes
0
answers
368
views
Is it possible to check equality of equi-recursive types, or recursive λ-terms?
Can we determine if two λ-terms are equal?
Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
- 3,117
3
votes
0
answers
88
views
Is there any dataset of lambda terms?
I'm experimenting with optimizing reduction strategies for the untyped lambda calculus. Is there any (publicly available) dataset of (terminating) lambda terms I could use?
Maybe it would be ...
- 131
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
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
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
2
votes
0
answers
64
views
Church numerals and Kleene numerals
Church numerals $\overline{0} = \lambda fx. x$ and $\overline{n} = \lambda f x. f^n x$ are provisions for applying a function $n$ times to an argument. An alternate system of numerals, possibly ...
- 113
2
votes
0
answers
468
views
Is Combinatory Logic (CL) still relevant for programming language theory?
I've been reading up on R. Smullyan's "To Mock a Mockingbird" and Hindley's "Lambda-Calculus and Combinators: An Introduction". I've even read Schonfinkel's 1924 paper introducing the idea of ...
- 5,255
2
votes
0
answers
178
views
Connection between nonmonotonic logic and type theory (lambda calculus)
There is known connection between classical and modal logics and type theory (lambda calculus), but are there connections between nonmonotonic logics (e.g. defeasible logic) and type theory (lambda ...
- 409
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
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
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