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

Remove Settle and Raise rules

Browse Source
This commit is contained in:
JanUlrich 2024-02-05 01:33:39 +01:00
parent 3d10421439
commit 5c73e0b0f8
1 changed files with 43 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
unify.tex
View File

@ -128,27 +128,27 @@ $
\rulename{Upper}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{T} } \\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{G} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{T} }
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{G} }
\end{array}
\quad \quad
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{T} } \\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{T} }
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G} }
\end{array}
$
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{T} \lessdot \type{A} } \\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{T} \lessdot \type{L} }
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{L} }
\end{array}
$
\\\\
@ -607,6 +607,21 @@ This builds a search tree over multiple possible solutions.
\begin{center}
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{Same}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \type{G} \lessdot \tv{a}\\
\hline
\wildcardEnv \vdash
C \cup \set{
\tv{a} \doteq \type{G}
}
\end{array} \quad \begin{array}[c]{l}
\text{fv}(\type{G}) \in \Delta_{in}
\end{array}
$
\\\\
\rulename{\generalizeRule}
& $
\begin{array}[c]{l}
@ -665,28 +680,28 @@ This builds a search tree over multiple possible solutions.
\end{array}
$
\\\\
\rulename{Settle}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\tv{a} \lessdot^* \tv{b}}
\\
\hline
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} }
\end{array}
$
\\\\
\rulename{Raise}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
\tv{a} \lessdot \tv{b}}
\\
\hline
\wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
\end{array}
$
\\\\
% \rulename{Settle}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
% \tv{a} \lessdot^* \tv{b}}
% \\
% \hline
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} }
% \end{array}
% $
% \\\\
% \rulename{Raise}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
% \tv{a} \lessdot \tv{b}}
% \\
% \hline
% \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
% \end{array}
% $
% \\\\
\end{tabular}}
\end{center}
\caption{Step 2 branching: Multiple rules can be applied to the same constraint}