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

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

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

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

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:
...

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 "...

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

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

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

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

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

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 (...

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

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

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

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$...

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

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

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

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

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

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 $\...

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

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

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

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

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

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

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

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

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

#### Related Tags

lambda-calculus × 81lo.logic × 39

computer-science × 19

type-theory × 19

ct.category-theory × 14

computability-theory × 11

reference-request × 8

cartesian-closed-categories × 6

graph-theory × 5

proof-theory × 5

monads × 5

automata-theory × 5

linear-logic × 5

normalization × 4

combinatory-algebra × 3

soft-question × 2

ho.history-overview × 2

textbook-recommendation × 2

formal-languages × 2

homotopy-type-theory × 2

modal-logic × 2

co.combinatorics × 1

fa.functional-analysis × 1

dg.differential-geometry × 1

gr.group-theory × 1