21
votes
Is there a typed lambda calculus which is consistent and Turing complete?
Alright I'll give a crack at it: In general for a given type system $T$, the following is true:
If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a ...
- 13.2k
11
votes
Accepted
Simply typed lambda calculus and higher order logic
The distinction is this: if STLC is taken as a primitive language at the type-level adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL.
Taking ...
- 13.2k
11
votes
Is there a typed lambda calculus which is consistent and Turing complete?
Here is an answer to a variant of @cody's precisification of my question. There is a consistent LPTS which is Turing complete in roughly @cody's sense, if we allow the introduction of additional ...
- 461
11
votes
Why is the Curry-Howard isomorphism?
I suspect someone is going to come along with a deep category-theoretic reason for the connection, but in the meantime, here is my insight.
Both logic and programming with functions are built around ...
- 2,724
10
votes
Type-theoretic interpretation of Skolemization
Skolemization corresponds to the so-called type theoretic axiom of choice, which is briefly discussed in section 1.6 of the HoTT book.
This provides an equivalence along which we can swap $\Sigma$ ...
- 1,349
8
votes
Accepted
How do continuations represent negations (under the Curry–Howard correspondence)?
When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type ...
- 611
8
votes
Accepted
Motivation for Dependent Type
Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in ...
- 13.2k
6
votes
Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program?
I'll answer the opposite question which is:
can Curry-Howard prove a theorem for your program, which has nothing to do with the type?
The answer is yes, depending on the meaning of "nothing to ...
- 13.2k
6
votes
Why is the Curry-Howard isomorphism?
Someone wanted a deep category-theoretic insight?
A Heyting algebra is a cartesian-closed category.
- 26.6k
4
votes
Accepted
What's the logical counterpart to jumps with arguments on CPS terms?
Such a logic of continuations (or a syntax of continuation that arose from logical considerations) would be Laurent's “polarised linear logic” (LLP): Olivier Laurent, Étude de la polarisation en ...
- 112
4
votes
Accepted
Languages that lack contraction, weakening or exchange
As other commenters have mentioned what you are actually asking for is a language for planar string diagrams, aka monoidal categories.
But let me address your question purely from the point of view ...
- 331
3
votes
Languages that lack contraction, weakening or exchange
If you remove all those rules and add something like
If $A \vdash B$ and $A' \vdash B'$ then $A, A' \vdash B, B'$
you get a logic essentially for monoidal categories (it's basically string diagrams ...
- 431
3
votes
What's the logical counterpart to jumps with arguments on CPS terms?
For me, what is going on is reasonably standard:
You have $c$ with free variables $(x_i : \tau_i)_i$, and you replace it with $c[t_i/x_i]$ with the $(t_i)_i$ at types $(\tau_i)_i$; this is a standard ...
- 1,882
1
vote
What's the logical counterpart to jumps with arguments on CPS terms?
You may be interested in the Kappa calculus which has no higher order maps and broadly corresponds to Cartesian categories. You might also want to look into co-intuitionistic logic which has "...
- 111
Only top scored, non community-wiki answers of a minimum length are eligible