5
$\begingroup$

We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). Now according to Martin-Löf's meaning explanations [1], a hypothetical judgment of the form $$ x_1 : A_1, ..., x_n : A_n \vdash a : A \qquad\qquad\qquad\qquad\qquad\qquad (1)$$ means that $$ \vdash a[x_1,...,x_n/a_1,...,a_n] : [x_1,...,x_n/a_1,...,a_n]A \qquad (2)$$ for all closed terms $a_1 : A_1, ..., a_n : A_n$ (and also that this judgment should be functional in respect to judgmental equality, but I don't need to tackle this issue here).

This means, among other things, that the judgment $$ x : \mathsf{empty} \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat} \qquad\qquad\qquad\qquad\qquad\qquad\quad (3)$$ is derivable in the theory, since there are no closed terms of the empty type (for the condition given is vacuously true). But also that less obvious judgments are also vacuously evident: $$ x : \mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty}) \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat} \qquad\qquad\qquad\qquad (4)$$ since any closed term of $\mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty})$ gives us a closed term of $\mathsf{empty}$, which should have none.

My question is:

What is a nice way to implement a type checker for such a hypothetical judgments?

(I'm aware that the problem is undecidable in general, but in theory this should affect us only in the sense that we are unable to rule out all invalid judgments).

For simplicity, we can suppose that we already have a type checking algorithm for categorical judgments.

IMHO$-$and in the spirit of the universal introduction rule of predicate logic$-$the obvious type checking algorithm for (1) to say that it is valid whenever $$\vdash a[x_1,...,x_n/t_1,...,t_n] : [x_1,...,x_n/t_1,...,t_n]A$$ for a list of arbitraries closed terms $t_1 : A_1 ,..., t_n : A_n $ (since we can't possibly consider each closed term of such types). However, this algorithm is clearly unable to validate sequents such as (3), let alone (4).

There is a quick highly-inelegant fix, which is to add the condition that if you find $x : \mathsf{empty}$ in the context list, halt and automatically recognize the whole sequent as true. But what about not-so-evident vacuously evident judgments such as (4)?

Anyway, how would a correct, elegant and general approach look like?

PS: I'm sorry if the question is not precise enough, but I can't think of a better way to state it.

[1] Martin-Löf, Constructive Mathematics and Computer Programming, 1982.

$\endgroup$
  • $\begingroup$ I don't get your motivating example: are you saying that there are no inhabitants of $A\times (A \rightarrow \mathrm{empty})$? That really depends on $A$. $\endgroup$ – cody Oct 9 '16 at 19:23
  • $\begingroup$ @cody I made an edit with a concrete instance of $A$ to make my point clearer. $\endgroup$ – StudentType Oct 10 '16 at 2:49
  • $\begingroup$ Are you looking for Andromeda? It can derive these crazy things. Of course, not completely by itself, but with a bit of hints. $\endgroup$ – Andrej Bauer Oct 10 '16 at 7:17
  • $\begingroup$ I think you're looking for the equality reflection rule -- prove it sound with respect to your realizability semantics, and then prove (4) by proving that 𝗇𝖺𝗍→𝗇𝖺𝗍 is propositionally equal to 𝗇𝖺𝗍 in the inconsistent context, and so they are definitionally equal, and so you get (4) from the obvious 1 : nat. $\endgroup$ – Neel Krishnaswami Oct 13 '16 at 11:36
5
$\begingroup$

Part of the problem is we cannot say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ reduces to a hypothetico-general judgment.

In practice, the way that you implement this kind of type theory is by formalizing rules for hypothetico-general equality & membership as a kind of sequent calculus, and then you can write tactics that automate as much of the work as possible. This is the technique used in Nuprl, JonPRL and RedPRL, which all implement type theories of the kind that you describe in your post.

$\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.