Cody Roux (May 27 2022 at 22:03): Cody Roux (May 27 2022 at 22:03):I had a question for the great people of https://constructive-maths.zulipchat.com, but I think I'll ask here just in case...
I'm struggling with formalizing the normalization for STLC (really system T) in HA2, even on paper! The stumbling block is the definition of the interpretation of types .
In Coq I'd do this:
Fixpoint interp (t : type) : term -> Prop :=
match t with
| Nat => (* the set of terms that reduce to a numeral *)
| Arrow t1 t2 => (* the realizability arrow over the interpretation of t1 and t2 *)
end.
How do I code this with HA2? I'm suspecting "something something Tarski fixed-point theorem", but some clarification would be much appreciated.
Note that my "real" definition is mutually inductive, so any reference that handles that is appreciated (but not required).
Pierre-Marie Pédrot (May 27 2022 at 22:10):AFAIK you can't really define internally a type by large dependent elimination in HA2 (this would require a form of choice) but if you present this intepretation inductively you can define it by the usual impredicative encoding.
Pierre-Marie Pédrot (May 27 2022 at 22:12):That is, you encode instead
Inductive interp : type -> (term -> Prop) -> Prop :=
| nat_interp : interp nat (the set of terms that realize numerals)
| arr_interp : forall σ σi τ τi, interp σ σi -> interp τ τi -> interp (arr σ τ) (Fun σi τi)
Such inductive declarations can be systematically translated into HA2.
Cody Roux (May 27 2022 at 22:21):That mostly makes sense, thanks!
I'm a bit worried about that second argument of interp, though, can you remind me what the encoding is (roughly)?
Last updated: Sep 26 2023 at 13:01 UTC