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
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 ...
- 101
-2
votes
1
answer
117
views
Beta reduction and vacuous lambda abstraction [closed]
Suppose we have the following typed lambda term (where $s$ does not occur in E (which is of type $s \to p$) and $s$ and $s'$ have the same type), and want to apply $\beta$-reduction:
$(\lambda s. E)\, ...
- 3
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
1
vote
0
answers
58
views
A substitution to add variables in the context
I'm doing type-inference in a dependently typed language, using (as is commonly done) a λ-calculus with explicit substitutions like that of Abadi (with a representation based on debruijn indices) in ...
- 390
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
5
votes
1
answer
563
views
Applications of Barendregt–Geuvers–Klop conjecture
I was learning about type systems from Benjamin C. Pierce's Types and Programming Languages and came across the Lambda cube in the chapter on Higher-Order Polymorphism. After reading up more about it ...
- 151
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
1
vote
0
answers
71
views
Other popular lambda calculus encodings besides Church's?
I know once could start from the popular Church encodings of booleans, ints, etc and arbitrarily obfuscate and complicate them to obtain new representations of the same concepts, but are there other ...
- 111
8
votes
1
answer
513
views
PHOAS with extrinsic typing?
Parameterized Higher Order Abstract Syntax (PHOAS) is a representation of syntax trees that allows the host language's binding to be used to represent binding in the language being modelled, while ...
- 2,830
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
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
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 ...
- 675
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
7
votes
2
answers
395
views
Termination checking for Scott-encodings in System F with positive-recursive types
Is there any research on termination analysis on Scott-encodings in System F with positive-recursive types.
All papers I have found use languages with constructors and case analysis (for example ...
- 701
3
votes
1
answer
228
views
Infinite $\beta \eta$-reduction sequence implies infinite $\beta$-reduction sequence
In Sorensen and Urzyczyn's book there is a lemma (1.3.11) which I am having a hard time proving.
1.3.11 Lemma:
If there is an infinite $\beta \eta$-reduction sequence starting with a term $M$ then ...
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
12
votes
1
answer
4k
views
What is the "question" that programming language theory is trying to answer?
I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
- 5,255
1
vote
1
answer
98
views
Extending EAL with recursion makes it incompatible with the abstract algorithm?
A few years ago, I've asked if Elementary Affine Logic can be used as the core type system of a practical programming language. The accepted answer argues that, yes, although such language would be ...
- 3,117
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
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
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
7
votes
3
answers
457
views
When a type is a value?
In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
5
votes
1
answer
471
views
Busy Beaver Equivalent for the Untyped Lambda Calculus
In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus:
Over all terms in the ULC composed of ...
- 776
11
votes
2
answers
438
views
Hereditary substitution with a universe hierarchy
I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types.
I'm wondering, are there any examples of hereditary substitution in ...
- 2,830
11
votes
1
answer
463
views
Understanding the Proof of Strong Normalization of the Calculus of Constructions
I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong ...
- 375
6
votes
2
answers
295
views
Typing of substitution in a bidirectional type system
In most typed lambda calculi, we have the following lemma:
If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
- 2,830
6
votes
2
answers
439
views
Preservation under Substitution with Telescopes
In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":
If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$,
then $\Gamma \...
- 2,830
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
11
votes
3
answers
1k
views
Equivalent formulation of complexity theory in Lambda Calculus?
In complexity theory the definition of time and space complexity both reference a universal Turing machine: resp. the number of steps before halting, and the number of cells on the tape touched.
...
4
votes
1
answer
152
views
Is the church-style affine calculus of constructions with unrestricted recursion consistent?
Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example:
...
- 3,117
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
13
votes
5
answers
600
views
Representing bound variables with a function from uses to binders
The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de ...
- 675
4
votes
1
answer
243
views
Why isn't it "enough" to prove induction with one extra "INat" argument?
It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is,
...
- 3,117
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 ...
- 2,581
7
votes
1
answer
237
views
If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?
Question
If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ...
- 3,117
5
votes
3
answers
303
views
Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation?
Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices:
...
- 3,117
7
votes
1
answer
747
views
Fixed points in dependent type theories
Most dependent type theories aim for some notion of correctness in two respects:
The type system must be decidable.
The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
- 1,141
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 ...
1
vote
1
answer
155
views
What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus?
Let $\Lambda$ be a set of strongly normalizing lambda terms.
Let $\mathtt{NF} : \Lambda \rightarrow \Lambda$ be evaluation to the normal form.
Let $ \lvert x\rvert : \Lambda \rightarrow \mathbb{N}$ be ...
- 1,177
1
vote
0
answers
64
views
Effect handlers, arrows and applicatives
After reading Lindley's paper on effect handlers for arrows and applicatives, I got the gist about dynamic and static flow and that it was added to the effect system and so on. However, I do not ...
- 131
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
0
votes
1
answer
55
views
Head variables of terms after application
We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form $\...
- 259
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
1
vote
1
answer
166
views
How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?
Suppose that we take the Calculus of Constructions as a basis, but take away exponential functions (allowing only linear functions), and add the controlled duplication rules of EAL. That'd, I believe, ...
- 3,117
10
votes
1
answer
247
views
Program inversion algorithms for higher-order programs
The term program inversion
has multiple shades of meaning, but probably got started with
J. McCarthy's 1956 work The Inversion of Functions Defined by Turing Machines in the context of AI. By now ...
- 11.4k
7
votes
1
answer
341
views
Finding a common factor in $\lambda$-terms that agree under certain substitutions
Suppose that $\mathcal{L}$ is the language of a simply typed lambda calculus of two base types, $e$ and $t$, with infinitely many constants at each type.
A substitution $j$ is a mapping from ...
- 443
11
votes
3
answers
315
views
Calculus of Constructions: compress expression to its smallest form
I'm aware that the Calculus of Constructions is strongly normalizing, meaning every expression has a normal for that cannot be beta,eta-reduced further. So in fact this is the most efficient ...
- 213
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 ...
- 701
1
vote
0
answers
47
views
Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?
From this question, the answerer states EAL-based languages can use arbitrary fixpoint types without losing strong normalization, because their normalization (and complexity) properties comes from ...
- 3,117