stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Compare commits

base: stan:bf401f1f08666cfeb96c374002109b3ea9620476
Branches Tags
stan:master
stan:cctv
stan:lncs
stan:completeness
stan:cleanup
stan:MultiLet
...
compare: stan:b546da831dfc8e7206714e0a325f16c5616c8111
Branches Tags
stan:master
stan:cctv
stan:lncs
stan:completeness
stan:cleanup
stan:MultiLet

2 Commits
bf401f1f08 ... b546da831d

Author SHA1 Message Date
Andreas Stadelmeier
b546da831d Start soundness for prepare rule 2024-01-15 20:43:19 +01:00
Andreas Stadelmeier
b9e0b1fa6d Fix error in Prepare rule 2024-01-15 20:43:06 +01:00
2 changed files with 16 additions and 6 deletions
Show Stats Expand all files Collapse all files

16
soundness.tex
View File

@ -271,15 +271,25 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
\item[Prepare]
To show
$\Delta \vdash \wctype{\overline{\wildcard{B}{U}{L}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof:
$\Delta \vdash \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof:
We know
\begin{gather}
\ol{S} = \ol{T}\\
\text{fv}(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) = \emptyset\\
\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
%TODO
\end{gather}
\begin{gather}
\Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\
\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta) \\
\label{rp:3}
\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \overline{\wildcard{B}{U}{L}}) \\
\label{rp:4}
\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset
\end{gather}
\ref{rp:4} is always true.
Due to $\text{fv}(\sigma(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}})) = \emptyset$ implies \ref{rp:3}.
\item[Capture]
If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.

6
unify.tex
View File

@ -380,10 +380,10 @@ Their upper and lower bounds are fresh type variables.
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \overline{\wildcard{B}{\type{U}}{\type{L}}}
\wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}}
\vdash C \cup \, \set{
\ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
\ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
@ -391,7 +391,7 @@ Their upper and lower bounds are fresh type variables.
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\ol{\rwildcard{C}} \ \text{fresh}\\
\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset\\
\text{fv}(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}}) = \emptyset\\
\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
\end{array}
\end{array}