0
$\begingroup$

Girard's System F have the following definition for natural numbers : $$ \mathbb N := \forall\alpha, (\alpha\rightarrow\alpha) \rightarrow (\alpha\rightarrow\alpha) $$

A dependent type system can have a similar definition based on dependent product (where $\mathbb T$ is the type of all types) : $$ \mathbb N := \prod_{\alpha:\mathbb T} (\alpha\rightarrow\alpha) \rightarrow (\alpha\rightarrow\alpha) $$

Let's define the $\lambda$-term successor in this dependent type system : $$ S := \lambda n^{\mathbb N}. \lambda\alpha^{\mathbb T}. \lambda s^{\alpha\rightarrow\alpha}. \lambda z^\alpha. s \bigl( n \alpha s z \bigr) $$

We know that relation $\leq$ on natural numbers satisfies the following first order logic propositions : $$ \forall m, \forall n, m \leq n \Rightarrow m \leq S n $$ $$ \forall n, n \leq n $$

Can we define $\leq$ in our dependent type system like we defined $\mathbb N$ ? : $$ \leq := \prod_{p:\mathbb N} \prod_{q:\mathbb N} \prod_{\alpha:\mathbb N\rightarrow(\mathbb N\rightarrow\mathbb T)} \bigl( \prod_{m:\mathbb N} \prod_{n:\mathbb N} (\alpha m n) \rightarrow (\alpha m (S n)) \bigr) \rightarrow \bigl( \prod_{x:\mathbb N} \alpha x x \bigr) \rightarrow (\alpha p q) $$

Or : $$ \leq := \sum_{p:\mathbb N} \prod_{q:\mathbb N} \prod_{\alpha:\mathbb N\rightarrow(\mathbb N\rightarrow\mathbb T)} \bigl( \prod_{m:\mathbb N} \prod_{n:\mathbb N} (\alpha m n) \rightarrow (\alpha m (S n)) \bigr) \rightarrow \bigl( \prod_{x:\mathbb N} \alpha x x \bigr) \rightarrow (\alpha p q) $$

$\endgroup$
0
$\begingroup$

Night was helpful, I think I found the right definition : $$ \leq := \lambda p^{\mathbb N}. \lambda q^{\mathbb N}. \Biggl( \prod_{\alpha:\mathbb N\rightarrow(\mathbb N\rightarrow\mathbb T)} \bigl( \prod_{m:\mathbb N} \prod_{n:\mathbb N} (\alpha m n) \rightarrow (\alpha m (S n)) \bigr) \rightarrow \bigl( \prod_{x:\mathbb N} \alpha x x \bigr) \rightarrow (\alpha p q) \Biggr) $$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.