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