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.

202 questions
136 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 ...
278 views

Resources for Church's paper “An Unsolvable Problem of Elementary Number Theory”?

I'm trying to understand and breakdown into simple English Church's paper for "An Unsolvable Problem of Elementary Number Theory" but I'm not finding anything useful online, only citations and links ...
87 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$ ...
79 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 ...
510 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 ...
291 views

What is the benefit of Krivine's notation?

I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ ...
47 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 ...
563 views

Weakly normalizing + confluent = strongly normalizing?

I was reading this abstract and saw that they prove weak normalization and confluence. My limited understanding suggests that those two properties should provide strong normalization, which then ...
77 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 ...
92 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, ...
128 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 ...
5k 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 ...
295 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 ...
125 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 ...
208 views

Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?

If we extend the Calculus of Constructions with Fix, we gain a lot of expressivity for barely no added complexity. That includes being able to derive induction, perform large eliminations, prove ...
248 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 ...
305 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 ...
2k views

Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
182 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 ...
184 views

36 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 ...
319 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 ...
218 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. ...
911 views

Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
98 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: ...
366 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 ...
43 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 ...
177 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, ...
571 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 ...
163 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 ...
262 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 ...
870 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: ...
153 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 ...
139 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: ...
89 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 ...
44 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 ...
78 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 ...
269 views

Is there a “lambda cube” for interaction nets?

The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about ...
855 views

How is Lambda Calculus a specific type of Term Writing system?

Now we can see that 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 ...
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 ...
252 views

How to translate general recursion into a set of $\mu$-recursive operator applications?

I'm trying to find a scheme to translate a functional language with let rec into a set of primitives called "generalized arrows", i.e. $\kappa$-calculus with ...
48 views

3k views

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
124 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, ...
71 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 ...