2
$\begingroup$

Curry-Howard style correspondences establish a tight conection between various logics on the one hand and explicitly computational calculi on the other. The canonical example is the correspondence between simple type theory (with arrow types) and natural deduction in the implicational fragment of propositional intuitionistic/minimal logic.

I understand that adding dependent types to the underlying type theory corresponds to the addition of quantifiers in the paired logic. Likewise, one can think of the passage from simple type theory to system F as corresponding to the addition of universal quantification over propositional variables. But I'm a bit unclear on what the addition of proper type operators corresponds to.

I'm sure this question has a relatively simple answer.

$\endgroup$
2
  • $\begingroup$ Do you have a link for "proper type operators"? $\endgroup$
    – Malice Vidrine
    Mar 25, 2017 at 3:17
  • 1
    $\begingroup$ Yes, sorry. I just meant the $\lambda\underline{\omega}$ axis of the $\lambda$ cube. My references for this stuff is Geuvers and Nederpelt's book $\textit{Type Theory and Formal Proof}$ (no link), and Sørensen and Urzyczyn's book $\textit{Lectures on the Curry-Howard Isomorphism}$(disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf). $\endgroup$
    – user279406
    Mar 25, 2017 at 20:04

2 Answers 2

Reset to default
1
$\begingroup$

As a relation between logic and type theory, there's not much to say. A logic is a kind of degenerate type theory. Namely, it's one where all (proof) terms are treated as equivalent. $\lambda\underline\omega$ is basically a simply typed lambda calculus (STLC) whose type level itself forms a STLC. The logic corresponding to this is what you get by degenerating the term level STLC to intuitionistic propositional logic. The type level STLC remains the same; we can't degenerate the type level STLC because that would lead to all formulas being considered equivalent. So the logical analog of type operators is type operators.

$\endgroup$
0
$\begingroup$

I'll share the motivation I have in mind.

First let's agree that the $ \lambda 2 $ axis (AKA system $ F $) is well-motivated, as it allows for the identity function; i.e. a term which, when given a type, reduces to the identity function of that type.

Problem is that in the $ \lambda 2 $ axis is its dependencies on external checks of validity. Each time you introduce a variable via $ (var) $ or a type via $ (form) $, you must validate the context. If you want a type over which to apply a term, you have to construct it externally and perform a relatively complicated check before introducing it using the $ (form) $ rule.

In the $ \lambda \underline{\omega} $ axis, the formation of types and contexts are internalized.

$\endgroup$
1

You must log in to answer this question.