[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 13 October 2017 at 10:23, Bruno Bentzen <[email protected]> wrote: > but I would like to understand why, from the perspective of the meaning > explanations alone (where terms are open-ended programs in a computation > system resulted from an untyped notion of computation), the inference from 1 > to 2 fails? > > Perhaps because programs are open-ended (as it was pointed out to me by Bob > Harper), so that we have no means of recursively enumerate them all (because > one can always extend the computational system with new programs)? But if > this is the case, I fail to see why it is acceptable to rule out Kleene's T > as a program (since programs are open-ended). Dear Bruno, I understand the meaning explanation can be seen as basically a realizability interpretation of type theory based on untyped realizers [1]? Then let me provide my 2 cents, based on my (partial) understanding of realizability and PER models. I welcome any corrections. Since we talk about truth in a model and not usual provability, I'll write Γ ⊧ t : T, instead of Γ ⊢ t : T true. I'm not 100% what you mean by open-ended — with an open-ended set of terms, where you allow adding "postulates", you can't even validate (E) [1]. But once you fix your set of terms, you can do structural induction on them *in the metatheory*, but even untyped lambda terms cannot inspect the structure of their arguments (as Andrej explained), unlike Turing machines. So, let's write U for your type Π(e : nat) (Σ (i, x : nat) T(e,i,x)) + ¬(Σ (i, x : nat) T(e,i,x)). Then, it should be provable metatheoretically that there is no closed value of of type U (as you say). This reasoning cannot be internalized into a lambda term, essentially by Andrej's argument; yet, I expect the metatheoretic argument is sufficient to prove that H: U ⊧ ⊥ (or, in your notation, that H : U ⊢ empty true). Specifically, just like (E) p : Id(nat,0,1) ⊧ 1 : nat -> nat holds because Id(nat,0,1) is empty, and vacuously for all members p of Id(nat,0,1) we have that 1 realizes nat -> nat, I think that judgement (B) p : U ⊧ 1 : empty holds by a similar argument. In either case, if we add postulates to sets of realizers so that Id(nat,0,1) or U is non-empty [1], we get a different model where (E) and (B) fail—however, such postulates could not be reduced, destroying canonicity. Which is good: canonicity enables computation, so a realizer for excluded middle can't actually be computable in all cases. (Formally, IIUC, instead of considering closed values as realizers, we'd allow a few free variables, and make assumptions on what types those variables realize). On a related note, IIUC your judgement holds in NuPRL (by a different proof?), which appears to be also based on the meaning explanation [2]. That's how I interpret http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/quot_1/no-excluded-middle-quot-true2.html (where ⇃ is defined in http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/per!type!1/quotient.html and quotients realizers together). [1] https://ncatlab.org/nlab/show/meaning+explanation [2] http://www.jonmsterling.com/pdfs/meaning-explanations.pdf Cheers, -- Paolo G. Giarrusso - Ph.D. Student, Tübingen University http://ps.informatik.uni-tuebingen.de/team/giarrusso/
