From 743e32daa929d04a94a78ce63446ef23a65d3531 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Thu, 1 Feb 2024 18:17:46 +0100 Subject: [PATCH] Use Unify recursive in method call soundness proof --- soundness.tex | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/soundness.tex b/soundness.tex index 4d1c5e8..c1608ee 100644 --- a/soundness.tex +++ b/soundness.tex @@ -106,6 +106,13 @@ $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ %TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N) % and which is a supertype of T_r (so no free variables in T_r) + +We could use unify to generate S by +$\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$ +%TODO: Proof that this always works. +% Only the variables in \Delta' ol\Delta are used. Maybe change the lemma 10 to that. +% That part of the unify algorithm is not influenced by other free variables + This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$, $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,