walker (Jan 29 2023 at 21:47): walker (Jan 29 2023 at 21:47):I was reading a paper where they showed a technique of showing a technique which I thought I might borrow for different purpose:
So The goal is to show a language with set of operational semantics, and typing rules have the same properties of another language
Ideally, I wanted show that progress and preservation can be carried from one language to another.
My goal was to have a an richer MLTT implementation and try to cheat the system and get proofs of progress and preservation by showing that anything done in this language can be done in a simpler MLTT language.
So I started by Term and CTerm which is core language term.
Then I created a simple function to translate terms to core terms:
Fixpoint translate (t: Term) : CTerm :=
match t with
| var idx => Cvar idx
| univ lvl => Cuniv lvl
| pi A B => Cpi (translate A) (translate B)
.....
end.
They are identical as you can see, bec. my current goal is to identify the fundamental problems.
I was able to prove that this translation preserves structure by making sure that it preserves typing, substitution, and reduction:
Lemma translate_preserve_subst_term (t n: Term): translate t.[n/] = (translate t).[translate n/].
Lemma translate_preserve_typing Γ t T:
Γ t ⊢ T -> map translate Γ ⊢ (translate t) : (translate T).
Lemma translate_preserve_mred t1 t2:
t1 ⟶* t2 -> (translate t1) ⟶* (translate t2).
Note I am abusion the notation abit but my problem is not a problem of coq anyway it is problem with the technique.
So now that I have proofs of preserving structure, I want to prove, confluence.
I know that:
Lemma core_mred_confluence (t1 t2 t: CTerm)
t ⟶* t1 ->
t ⟶* t2 ->
exists t',
t1 ⟶* t' /\ t2 ⟶* t'.
and I wanted to prove that:
Lemma mred_confluence (t1 t2 t: Term)
t ⟶* t1 ->
t ⟶* t2 ->
exists t',
t1 ⟶* t' /\ t2 ⟶* t'.
using translate_preserve_mred and the core_mred_confluence lemma I was stuck at proving:
t3: CTerm
=================
CMulti CReduction (translate t1) t3 ->
CMulti CReduction (translate t2) t3 -> exists t' : Term, t1 ⟶* t' /\ t2 ⟶* t'
and it feels like I need to get the inverse translation, that would work for this particular case, because both languages are identical, but I would intend to add multi-argument functions/pairs/ and moules, then translation would lose information since the core language has only the basic tuples, and single argument functions. Also I indented to remove annotations required for bidirectional type checking like:
lam A t => core_lam t but then inverting this operations using only the expression is impossible.
So my question is: is this technique known ?(the goal is to avoid having to deal with the full proofs of progress and preservation everytime I make a modification to the language I am building)
B- if yes, I don't even know what is it called and I cannot search for it in literature, and I don't know where did I go wrong with my proof strategy.
C- If now, what would be the right way to go with my goal of diving the language design into core theory and elaboration and prove that the elaboration maintains all the (arbitrary) properties of the core.
Gaëtan Gilbert (Jan 29 2023 at 22:10):sounds like https://hal.inria.fr/hal-01445835/
Gaëtan Gilbert (Jan 29 2023 at 22:13):btw for reduction you might not have the other direction ie forall t1 t2, (translate t1) ⟶* (translate t2) -> t1 ⟶* t2 but still have something close like forall t1 ct2, (translate t1) ⟶* ct2 -> exists t2, ct2 ⟶* (translate t2) /\ t1 ⟶* t2
walker (Jan 29 2023 at 22:17):I thought this paper was just a survery, but I see lots of interesting ideas! thanks alot for reminding me of it!
walker (Jan 29 2023 at 22:18):wow first time I checked it, it didn't make sense, and now everything sounds familiar!
walker (Jan 29 2023 at 22:18):Gaëtan Gilbert said:
btw for reduction you might not have the other direction ie
forall t1 t2, (translate t1) ⟶* (translate t2) -> t1 ⟶* t2but still have something close likeforall t1 ct2, (translate t1) ⟶* ct2 -> exists t2, ct2 ⟶* (translate t2) /\ t1 ⟶* t2
right that should work and I hope it does, I was so fixated on the idea that inverse translation is to be avoided thanks for the hint
walker (Jan 30 2023 at 21:45):@Gaëtan Gilbert I tried following that lead you gave me,
The problem is is using the lemma "forall t1 ct2, (translate t1) ⟶* ct2 -> exists t2, ct2 ⟶* (translate t2) /\ t1 ⟶* t2` is that it doesn't tell much about ct2, I couldn't use it to lift confluence from core language to elaborate language:
We start from here:
t ⟶* t1 ->
t ⟶* t2 ->
exists t', t1 ⟶* t' /\ t2 ⟶* t'.
then we translate to core terms:
(translate t) ⟶* (translate t1) ->
(translate t) ⟶* (translate t2) ->
exists t', t1 ⟶* t' /\ t2 ⟶* t'.
Then we use confluence the core language:
(translate t1) ⟶* ct' ->
(translate t2) ⟶* ct' ->
exists t' : Term, t1 ⟶* t/\ t2 ⟶* t
using the inverse lemma: one gets something like:
(exists A' : Term, translate A' :=ct' /\ t2 ⟶* A') ->
(exists A' : Term, translate A' := ct' /\ t1 ⟶* A') ->
exists t'0 : Term, t1 ⟶* t'0 /\ t2 ⟶* t'0
Which doesn't look far of the starting point.
The confluence property is lost once you go back, and I feel stuck.
This partial inverse of translation is too weak, the proper inverse is too strong, and I feel totally stuck.
walker (Jan 30 2023 at 21:47):I also created a translation judgement in the hope it might be make things easier to work with:
Reserved Notation "'⟦' x '⟧' ':=' y" (at level 20, y at next level).
Inductive Translate: Term -> CTerm -> Prop :=
| Translate_var idx : ⟦ var idx ⟧ := Cvar idx
| Translate_univ lvl : ⟦univ lvl⟧ := Cuniv lvl
| Translate_pi A B A' B':
⟦A⟧ := A' ->
⟦B⟧ := B' ->
⟦pi A B⟧ := Cpi A' B'
| Translate_lam A t A' t' :
⟦A⟧ := A' ->
⟦t⟧ := t' ->
⟦lam A t⟧ := Clam A' t'
| Translate_appl m n m' n':
⟦m⟧ := m' ->
⟦n⟧ := n' ->
⟦appl m n⟧ := Cappl m' n'
| Translate_sigma A B A' B':
⟦A⟧ := A' ->
⟦B⟧ := B' ->
⟦sigma A B⟧ := Csigma A' B'
| Translate_pair A B m n A' B' m' n':
⟦A⟧ := A' ->
⟦B⟧ := B' ->
⟦m⟧ := m' ->
⟦n⟧ := n' ->
⟦pair A B m n⟧ := Cpair A' B' m' n'
| Translate_proj1 m m':
⟦m⟧ := m' ->
⟦proj1 m⟧ := Cproj1 m'
| Translate_proj2 m m':
⟦m⟧ := m' ->
⟦proj2 m⟧ := Cproj2 m'
where "'⟦' x '⟧' ':=' y" := (Translate x y) (format "⟦ x ⟧ := y").
what I want to avoid doing is assuming that translation has inverse, because I plan to lose some information in future iterations from the core language ( like A B parts in sigma which is used for type annotations)
That makes it feel like the type system is not actually confluent, because then in this particular case (which I still doesn't have)
⟦pair (univ 1) (univ 2) m n⟧ := Cpair m' n' and ⟦pair (var 1) (var 2) m n⟧ := := Cpair m' n, but then the two translations reduce to one another by reflexivity, but the two original terms does not for obvious reasons.
which makes me wonder if the general assumption "if lang X can be embedeed in lang Y, and lang Y has properties A, B, C, then lang X also has the properties A, B, C" is actually wrong ?
walker (Jan 30 2023 at 23:20):I think I found name of the property I need, "Conservativity"
Gaëtan Gilbert (Jan 31 2023 at 06:31):which makes me wonder if the general assumption "if lang X can be embedeed in lang Y, and lang Y has properties A, B, C, then lang X also has the properties A, B, C" is actually wrong ?
If you lose information, can it be called an embedding?
walker (Jan 31 2023 at 07:13):But my assumption is if a language is
Type safe, then that language with extra annotations should also be type safe
walker (Jan 31 2023 at 07:15):Especially if this annotations does not restrict the language usage, and does not allow extra theorems to be proven.
Notification Bot (Jan 31 2023 at 07:15):A message was moved here from #Miscellaneous > Content about System F (Polymorphic Lambda Calculus)) by walker.
Paolo Giarrusso (Jan 31 2023 at 08:11):It might be easier to construct counter-examples: take erasure from simply-typed lambda calculus to un(i)typed lambda calculus, and patch STLC to fail preservation
Paolo Giarrusso (Jan 31 2023 at 08:13):In general, weakening typing doesn't necessarily weaken preservation: Typing appears both co- and contravariantly in the statement, after all
walker (Jan 31 2023 at 08:28):but then why would everyone say that if there is structure preserving transformation from A to B, then proving that B is safe is sufficient to prove that A is safe (or a variant of that) ?
walker (Jan 31 2023 at 08:28):let me check the paper
walker (Jan 31 2023 at 08:29):"To justify a complex type theory, it suffices to compile it into a simpler—already justified—type theory.”
in the The next 700 syntactical models of type theory paper.
walker (Jan 31 2023 at 08:30):but they never proved this statement which is confusing.
Gaëtan Gilbert (Jan 31 2023 at 08:44):because "justify" is a variety of properties
same way you didn't define what "safe" means
walker (Jan 31 2023 at 08:46):I see, that is unfortunate, I though it would be possible to move proofs of progress& preservation to richer type theory.
Paolo Giarrusso (Jan 31 2023 at 09:28):However, do you really need to consider reduction on the source language, instead of only the target language?
Paolo Giarrusso (Jan 31 2023 at 09:30):There isn't a notion of reduction on Coq source terms, only on the Coq terms produced by elaboration
walker (Jan 31 2023 at 10:12):What I am currenty doing is trying to use the source language as the main language,I wanted to enahnce it with enough structure that will be important when doing code generation to assembly/SSA-like IR,
so what is really needed here is to have evidence that this source language has 2 properties, type safety, desirable type checking (assuming normalization)
To prove the bidirectional type checker, I often used the confluence property in the proofs, so I need that. As for the type safety, i need to show the source language has progress&subject reduction.
In principle I can do that from scratch, but I wanted to offload that task to the core language and infer those properties in the source language.
For instance, when adding module system to the source language.
walker (Jan 31 2023 at 13:43):apparently this property I need is to some extent studied under the names conservative extension,definitional extension, conservative transformations and they have not been formalized in any proof system before.
walker (Jan 31 2023 at 13:44):the question is : is proving one of those three properties easier than proving type safety by other means ? and I could't find definite answer for that.
Last updated: Apr 19 2024 at 00:02 UTC