All Questions
Tagged with lambda-calculus lo.logic
41 questions
6
votes
1
answer
273
views
Consistency in pure type systems
Summary
My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm ...
CommunityBot
- 1
1
vote
0
answers
122
views
How could I formally express: System F cannot express universal quantification over things that are not types? [closed]
I'm trying to understand exactly why it is that https://ncatlab.org/nlab/show/computational+trilogy states that quantification requires dependent types, and why this wouldn't be possible to achieve ...
- 113
11
votes
3
answers
1k
views
How to handle sums in Tait's reducibility proof of strong normalisation?
I've been reading Girard et al's 'Proofs and Types', which in Chapter 6 presents a proof of strong normalisation for the simply typed lambda calculus with products and base types. The proof is based ...
- 1,094
24
votes
0
answers
3k
views
What's the smallest $\lambda$-calculus term not known to have a normal form?
For Turing Machines, the question of halting behavior of small TMs has been well studied in the context of the Busy Beaver function, which maps n to the longest output or running time of any halting n ...
- 1,734
16
votes
2
answers
3k
views
Why is there no product type in simply typed lambda-calculus?
$\DeclareMathOperator\Pair{Pair}\DeclareMathOperator\First{First}\DeclareMathOperator\Second{Second}\DeclareMathOperator\Left{Left}\DeclareMathOperator\Right{Right}\DeclareMathOperator\Choice{Choice}$...
- 12.9k
12
votes
2
answers
931
views
An overview of mathematical-logical approaches in formalizing natural languages
Crossposted on Mathematics SE
I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach),...
- 4,786
11
votes
4
answers
1k
views
Why is alpha-equivalence in untyped $\lambda$-calculus substitutive?
This is something all introductory texts seem to avoid proving, and many even avoid stating.
We consider untyped $\lambda$-terms on some countably infinite alphabet. If $x$ is a variable and $p$ is ...
- 4,713
7
votes
1
answer
375
views
Criterion for the consistency of pure type systems
Pure type systems are characterized in an almost combinatorial way: a set of axioms $\star_i : \star_j$, and a set of triples $(\star_i, \star_j, \star_k)$ saying when the dependent product $\prod_{x :...
CommunityBot
- 1
12
votes
2
answers
3k
views
How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?
It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...
- 103
12
votes
2
answers
1k
views
Is there a proof of strong normalisation that uses ordinal numbers?
I am currently trying to find a proof for strong normalisation of an extension of $\lambda$-calculus.
I've tried several approaches and one would be to assign an ordinal number $\operatorname{cs}(t)$ ...
- 255
4
votes
0
answers
95
views
$\omega$ incompleteness of $\lambda$ calculus
In Plotkin's 'The $\lambda$-Calculus is $\omega$-Incomplete' (The Journal of Symbolic Logic Vol. 39, No. 2 (Jun., 1974), pp. 313-317), an example is given of two (untyped) $\lambda$-terms $M$ and $N$ ...
- 358
19
votes
2
answers
1k
views
Do combinatory logic bases need a function of 3 variables?
All the known bases of combinatory logic, such as $\{S,K\}$, or $\{K,W,B,C\}$,
have one or more combinators using 3 variables:
\begin{align*}
S ={} & \lambda x\lambda y\lambda z. x z(y z), \\
B ={}...
- 21.3k
5
votes
1
answer
264
views
Internal language proof of Lawvere's fixed point theorem for cartesian closed categories
This proof of Lawvere's fixed point theorem suggests (since it uses $\lambda$ notation) that it is written in the internal language of cartesian closed categories (which is the $\lambda$-calculus, as ...
- 66.8k
3
votes
0
answers
206
views
What is the connection between these proofs of strong normalization in $\lambda^\to$ and LK?
In Ralph Loader's lecture notes on lambda calculus (section 3.3), he states that a combinatorial proof of the SN of simply typed lambda calculus uses a technique that is "in essence that used by ...
- 1,262
1
vote
0
answers
219
views
What is the proof theoretic strength of PCF?
Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic ...
- 482
0
votes
0
answers
110
views
Expressing a model transformation by using monads in the simply-typed lambda calculus
In https://link.springer.com/content/pdf/10.1007/s10670-019-00128-z.pdf , page 16, the following clause is given for a modal operator $\langle R_k \rangle$ (see definition 4.2 for the definition of a ...
- 639
20
votes
5
answers
3k
views
[solved] sequent calculus as programming language
intuitionistic logic ~ programming
natural deduction ~ lambda-calculus
Hilbert system ~ combinatory logic {S, K}
Gentzen system=sequent calculus ~ ?
What would you write in place of the question ...
3
votes
0
answers
264
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 ...
8
votes
1
answer
813
views
Easier Girard's paradox in a circular pure type system (PTS)
System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox.
One-...
- 1,452
9
votes
0
answers
539
views
The Curry Howard Isomorphism and models for an intuitionistic modal logic and its bimodal translation
My question regards the Curry Howard Isomorphism and how it constrains models in the case of a particular logic.
Consider quantified Lax Logic $QLL$.
https://pdfs.semanticscholar.org/468e/...
- 639
2
votes
0
answers
183
views
Notation in 'The lambda calculus, its syntax and semantics' by H.P. Barendregt
I'm reading the book 'The lambda calculus its syntax and semantics'. In part 5, chapter 19: Local structure of Models, more specifically 19.2 Local structure of $D_\infty$, the notation $D_\infty \...
- 21.3k
8
votes
0
answers
155
views
Is every total computable function definable by a strongly total lambda term?
Every computable (total) function $f : \mathbb{N} \to \mathbb{N}$ is definable in untyped pure lambda calculus in the sense that there is a term $F$ such that, for every Church's numeral $c_n = \...
- 4,459
8
votes
1
answer
321
views
Is every total computable function definable by a normalizing lambda term?
$\newcommand{\nat}{\mathbb{N}}$
$\newcommand{\then}{\ \Longrightarrow\ }$
A partial function $f : \mathbb{N} \to \mathbb{N}$ is said to be $\lambda$-definable if there is a term $F \in \Lambda$ such ...
- 4,459
12
votes
7
answers
17k
views
What is some good introduction to lambda calculus?
I have some background in set theory and automata and I am looking for a good place to start with lambda calculus.
- 53.3k
10
votes
2
answers
2k
views
Scott on the consistency of the lambda calculus
I have twice heard it attributed to Dana Scott that he said something to the effect that the consistency of the lambda-calculus was an accident.
Does anyone have a reasonable-sounding source for this?...
- 163
5
votes
0
answers
228
views
Proper full submodels of full models of type theory
Let $N$ be the standard full model of the simply typed lambda calculus with infinite base type $o$ and let $X$ be an infinite and coinfinite subset of $N(o)$. I want to know if there's a full ...
- 357
8
votes
3
answers
662
views
Models of intuitionistic linear logic that reflect the resource interpretation
I am interested in models of intuitionistic linear logic, that is, the logic that you get if you take classical linear logic and restrict the set of operators to $\otimes$, $1$, $\multimap$, $\times$, ...
3
votes
1
answer
404
views
Is there an easy decision algorithm for the inhabitation problem for simple types?
Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the Subject Reduction Property and the fact that any typable term is strongly $\beta$-...
CommunityBot
- 1
6
votes
1
answer
359
views
On an automatic translation of typed lambda calculus in untyped lambda calculus
I have a question regarding the "compilation" of typed lambda calculus in untyped lambda calculus.
Take for example the inductive definition of lists, with introduction rules:
and:
We can ...
- 1,452
6
votes
1
answer
737
views
Explanation of the definition of Saturated Sets in Lambda Calculus
I have a question on the definition of Saturated Sets, as particular subset of the set of strongly normalizing terms in lambda calculus.
Here is the definition: a set $S$ of strongly normalizing $\...
- 1,452
16
votes
7
answers
3k
views
What is lambda calculus related to?
So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based.
I was wondering if anyone had a suggestion ...
CommunityBot
- 1
17
votes
3
answers
3k
views
What is the history of the Y-combinator?
Inspired by the comments to this question, I wonder if someone can explain the history of the fixed point combinator (often called the Y combinator) in lambda calculus.
Where did it first appear? ...
CommunityBot
- 1
8
votes
0
answers
248
views
Is there a notion analogous to separability but requiring definable rather than countable sets?
Among models of $\lambda$-calculus, some like the Bohm tree model have the property that every element is a directed sup of definable elements, whereas others like the $D_\infty$ and $P(\omega)$ ...
- 211
1
vote
1
answer
169
views
Interaction-based approximation for HP-complete λ-theory?
We are looking for a proof or counter-examples for the following hypothesis.
Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either
$$
\exists ...
1
vote
1
answer
223
views
Hypothesis: interaction-based model for λKβη
We are looking for a proof or counter-examples to the following
Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ ...
3
votes
0
answers
266
views
Is it possible to implement η-reduction in interaction nets?
There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the ...
3
votes
5
answers
2k
views
Theory mainly concerned with $\lambda$-calculus?
Automata theory is mainly concerned with Turing machines and all its relatives-in-spirit. $\lambda$-calculus is rather rarely mentioned in textbooks on automata theory.
What's the common name of the ...
- 105
7
votes
4
answers
1k
views
What is the intuitive meaning of star and box in a pure type system?
The systems of the λ-cube have the axiom $\star:\square$.
I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\...
- 316
7
votes
1
answer
531
views
Are innermost reductions perpetual in untyped $\lambda$-calculus?
Background
In the untyped lambda calculus, a term may contain many redexes, and
different choices about which one to reduce may produce wildly
different results (e.g. $(\lambda x.y)((\lambda x.xx)\...
CommunityBot
- 1
11
votes
4
answers
2k
views
Can dependent sums be encoded as dependent products?
Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...
- 2,283
12
votes
3
answers
7k
views
Is functional programming a branch of mathematics?
In Theory mainly concerned with lambda-calculus?, F. G. Dorais wrote, of the idea that the lambda-calulus defines a domain of mathematics:
That would never stick unless there's another good reason. ...
CommunityBot
- 1