27 votes
Accepted

How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

The simply-typed $\lambda$-calculus is not stronger than second-order logic. The simply-typed $\lambda$-calculus has: product types $A \times B$, with corresponding term formers (pairing and ...
Andrej Bauer's user avatar
  • 47.7k
26 votes

Do combinatory logic bases need a function of 3 variables?

A Basis Result in Combinatory Logic, Remi Legrand, J. Symb. Logic 53.4 (1988), pp. 1224-1226. The aim of this article is to show that a basis for combinatory logic must contain at least one ...
Peter Taylor's user avatar
  • 6,516
18 votes

Do combinatory logic bases need a function of 3 variables?

@PeterTaylor’s excellent answer points to exactly the result wanted. But the proof there can be streamlined a bit, and may be paywalled for some readers, so I’ll write it out here for accessibility. ...
Peter LeFanu Lumsdaine's user avatar
16 votes
Accepted

What is Chemlambda? In which ways could it be interesting for a mathematician?

UPDATE (2020) There is now chemlambda.github.io which collects all the chemlambda related projects and articles. For the history of chemlambda see arXiv:2007.10288 or the associated html version Graph ...
Marius Buliga's user avatar
16 votes
Accepted

Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?

The point is that the reflection rule makes $p = \mathsf{refl}_x$ a well-formed expression. This turns out to be incredibly dangerous: now we can prove it by induction on equality. More precisely: ...
Zhen Lin's user avatar
  • 14.9k
14 votes

Is there a proof of strong normalisation that uses ordinal numbers?

I believe that Chapter 4 of Girard's Proofs and Types proves weak normalization for typed $\lambda$-calculus in this way, using ordinals up to $\omega^2$. He first assigns a natural number "...
Mike Shulman's user avatar
9 votes
Accepted

Easier Girard's paradox in a circular pure type system (PTS)

I feel like most of my posts on mathoverflow and cstheory.stackexchange consist of this answer, but the most perspicuous (in my opinion) proof of inconsistency of U and $*:*$ is a construction by ...
cody's user avatar
  • 1,080
8 votes
Accepted

How to handle sums in Tait's reducibility proof of strong normalisation?

The typical strategy when you're building a model to perform normalisation by evaluation (i.e. the computational part of Tait's method, see [1]) with sum types is to have as a semantics for ...
gallais's user avatar
  • 455
8 votes
Accepted

Relationship of lambda calculus to the rest of math

The question you are trying to ask is "What is a denotational semantics for the untyped lambda calculus?" This is a difficult problem because, as Bjorn Kjos-Hanssen said in his answer, if you try and ...
Justin Hilburn's user avatar
8 votes

Is there a proof of strong normalisation that uses ordinal numbers?

As far as I know, such a strong normalization proof is not known even for the simply-typed $\lambda$-calculus. It is mentioned as Problem 26 in the TLCA List of Open Problems. (It must be noted ...
Damiano Mazza's user avatar
8 votes

An overview of mathematical-logical approaches in formalizing natural languages

Here is what I answered in Math.SE: If you haven't read it already, I highly recommend reading L. T. F. Gamut's Logic, Language, and Meaning. If you already know some logic (say, up to first-order ...
Nagase's user avatar
  • 181
7 votes
Accepted

Consistency in pure type systems

I think this awkwardness is coming from your “principle of constants”, which is not standard, and doesn’t seem justified by the motivation you give. You say it’s meant to correspond to the practice (...
Peter LeFanu Lumsdaine's user avatar
7 votes
Accepted

Is every total computable function definable by a normalizing lambda term?

Yes, you can actually encode all computable functions by normalizable terms since it is always possible to turn a term into a normal form which computes the same function on Church's numerals. We just ...
Valery Isaev's user avatar
  • 4,410
6 votes

Scott on the consistency of the lambda calculus

Not exactly λ-calculus, but untyped formalisms in general. Here is an excerpt from the introduction of A type-theoretical alternative to ISWIM, CUCH, OWHY (bold emphasis is mine): No matter how ...
kirelagin's user avatar
  • 163
6 votes

Is simply typed lambda calculus with fixed-point combinator Turing-complete?

Damiano is right, the answer is no: it is not Turing complete. Supposing to define natural numbers as some type (o->o)->o->o, even with fixpoints you cannot define the predecessor (that would be ...
Andrea Asperti's user avatar
6 votes
Accepted

Is simply typed lambda calculus with fixed-point combinator Turing-complete?

The simply-typed $\lambda$-calculus with the fixpoint combinator but without a primitive integer type is not Turing-complete, at least not in the usual sense (Church integers and computation as $\beta$...
Damiano Mazza's user avatar
6 votes

How to handle sums in Tait's reducibility proof of strong normalisation?

Let me add to the above (perfectly correct) answers that there is a more general perspective, which works for all positive connectives, of which sums are a special case. The fundamental insight is ...
Damiano Mazza's user avatar
6 votes
Accepted

Internal language proof of Lawvere's fixed point theorem for cartesian closed categories

You're right that the statement of the theorem, and the entirety of the proof, don't fit inside the internal logic of a CCC. However, once given $f:B\to B$, the definition of $q$ and the proof that ...
Mike Shulman's user avatar
5 votes

How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

Simply typed lambda calculus and simple type theory are not equivalent. The former only has rules for alpha- and beta-reduction, the latter also has rules for Modus Ponens, extensionality and the ...
lambda.xy.x's user avatar
5 votes

An overview of mathematical-logical approaches in formalizing natural languages

This is a really a question about linguistics rather than mathematics, so you might be better off asking your question on Linguistics StackExchange rather than here. But anyway, I think what you're ...
Timothy Chow's user avatar
  • 78.1k
5 votes
Accepted

Selection terms in the untyped lambda calculus

No such terms can exist. Here's a proof, way too convoluted for my tastes, but I don't have time to find a better one. The proof uses a lot the so-called Genericity Lemma, a standard result the proof ...
Damiano Mazza's user avatar
4 votes

What, mathematically speaking, does it mean to say that the continuation monad can simulate all monads?

If I understand this paper correctly, the construction in full generality might not really involve the continuation passing monad as such. It is easy to see that if $M$ is an internal monad and $\...
Will Sawin's user avatar
  • 135k
4 votes

How to handle sums in Tait's reducibility proof of strong normalisation?

Guillaume's answer is correct, that is you may define the candidate for $A+B$ as the smallest set containing $$ \mathrm{inl}(a)\ a\in R_A(a)$$ $$ \mathrm{inr}(b)\ b\in R_B(b)$$ and which is a ...
cody's user avatar
  • 1,080
3 votes

Is lambda calculus polymorphism a type of generalized monad?

Short answer: Unfortunately, no. Long answer: It would seem the author of this question (me) has confused the concepts monoids and monoidal structures in a category. Given a Category $\mathbf{C}$ and ...
Johan Thiborg-Ericson's user avatar
2 votes

Relationship of lambda calculus to the rest of math

In the standard set theoretical setup, a function cannot have itself as an input. This is because the rank of the function is strictly larger than that of its inputs and outputs. https://en.m....
Bjørn Kjos-Hanssen's user avatar
2 votes

Does substitution on named terms correspond to substitution on de Bruijn terms?

See the 2021-present work of Joshua Grosso, who formalised the paper in Coq, correcting some errors in the process (last update 3 weeks ago). However, Grosso wrote: To our knowledge, all of the main ...
David Roberts's user avatar
  • 33.8k
2 votes

Where can I learn about Cartesian closed functors between categories of simply typed lambda calculus?

If I understand correctly, you are considering simple types over $\to,\times$ as objects, $\beta$-normal, $\eta$-long $\lambda$-terms as arrows, and substitution plus normalization as composition. In ...
Damiano Mazza's user avatar
1 vote

Semiring axioms which almost implement inverse, searching for domains other than lambda calculus

This is a sort of strained example but there is certain resemblance to differential operators: Let $i=0\dots p-2$ and $\mathbb F_p[x_0,\dots x_{p-2}]$ the algebra of polynomials over a finite field. ...
Dmitrii Korshunov's user avatar
1 vote

Criterion for the consistency of pure type systems

I'll write some fragment of thoughts here. First some known results. All the lambda cube is consistent (and normalizing, though I didn't mention it in the question, I'm also interested in that). A ...
Trebor's user avatar
  • 1,011
1 vote

Relationship of lambda calculus to the rest of math

First, these are not functions. These are lambda expressions that can be artistically interpreted as functions. If you want to model lambda theory in a theory where functions are a part of the ...
Vlad Patryshev's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible