# 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
Filter by
Sorted by
Tagged with
113 views

### Can you assign a type to any term of the λEA-calculus?

The untyped language of System-F and similar is the λ-calculus. That language has terms that can't be typed on System-F, λx.(x x) λx.(x x) being the most obvious ...
349 views

### Eta expansion in the pattern lambda calculus

Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns. http://www.sciencedirect.com/science/article/pii/S0304397508000571 In some sense, a pattern is a tree of variables ...
303 views

### Resources (books, etc) to learn about concurrency theory

I want to know more about concurrency theory from a formal/mathematical point of view, I know there are a lot of computer science branches that relates to concurrency theory like process algebra, ...
172 views

### Krivine's notation for lambda-terms [duplicate]

Krivine in his book (Lambda-calculus: Types and Models) introduces the grammar of lambda-terms and then abbreviations to denote them. The grammar itself is not ambiguous: Lambda-terms are obtained by ...
715 views

### Wouldn't the calculus of constructions with linear types be a simple functional core that is consistent and expressive?

I have recently asked if there is a simple functional core that is consistent and expressive. In another question, cody pointed out that this is an open problem to have a language that is: Consistent/...
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 ...
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 ...
285 views

### What, in simple terms, are the restrictions imposed by Elementary Affine Logic?

The answer to my last question on the subject made several insightful points on how EAL could be used as the basis of a practical programming language, which, in turn, could be evaluated using the ...
123 views

### Inference in typed lambda calculus theories

I'd like to do automated inference, say solving word problems or reducing to normal form, in an equational theory of the typed lambda calculus (with product and unit types). Equivalently, in category-...
291 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 ...
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, ...
1 vote
233 views

### Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?

What is the proof that the calculus of constructions, extended with recursive types (i.e., Fix at the type-level) isn't strongly normalizing?
1 vote
3k views

### Is iszero of the untyped lambda calculus sound and complete? [closed]

I am using the following definitions in the notation of Haskell. In case it matters, I would like to use only the $\alpha,\beta,\eta$ reductions rather than the Haskell evaluation rules. ...
113 views

### Can a fixed point combinator find the fixed point of a function that has no fixed point? [closed]

A fixed point combinator is supposed to find the fixed point of any function. Yet I am wondering what if a function happens to have no fixed point, such as the add1 ...
189 views

### Why is the multi-step reduction of semantics reflexive?

I was reading Programming Languages and Lambda Calculi, which defines the multi-step reduction to be the reflexive-transitive closure of the one-step reduction. (Page 15, $\twoheadrightarrow_r$ is the ...
900 views

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 ...
132 views

### Composition in explicit substitutions

In the classical λσ calculus of explicit substitutions, there is the following rewrite rule: (a[s])[t] ==> a[s ∘ t] where ...
267 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 ...
430 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 ...
356 views

### What type system fits the subclass of λ-terms that can be reduced optimally?

There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
543 views

### Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the ...
843 views

### What are the negative consequences of extending CIC with axioms?

Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term ...
477 views

### Church-Rosser property for dependently typed lambda calculus?

It is well-known that the Church-Rosser property holds for $\beta \eta$-reduction in simply-typed lambda calculus. This implies that the calculus is consistent, in the sense that not all equations ...
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 ...
1k views

### Are optimal evaluators actually optimal?

The following term (using bruijn-indexes): BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0))))))))) ...
101 views

### Is it possible to evaluate interaction combinators efficiently using a path-traveling strategy?

Interaction combinators can be evaluated using a path traversing strategy. That is, instead of applying annihilation/commutation rules to active pairs, one simply walks through the graph using a 2-...
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, ...
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 ...
In the paper Discriminating coded lambda terms - Henk Barendregt a coding $\ulcorner M \urcorner$ of a lambda term $M$ is a term such that $M$ (and its parts) can be reconstructed from it in a lambda-...