equal
deleted
inserted
replaced
129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
130 \mode<presentation>{ |
130 \mode<presentation>{ |
131 \begin{frame}<1>[c] |
131 \begin{frame}<1>[c] |
132 \frametitle{Higher-Order Unification} |
132 \frametitle{Higher-Order Unification} |
133 |
133 |
134 State of the art: |
134 State of the art at the time: |
135 |
135 |
136 \begin{itemize} |
136 \begin{itemize} |
137 \item Lambda Prolog with full Higher-Order Unification\\ |
137 \item Lambda Prolog with full Higher-Order Unification\\ |
138 \textcolor{darkgray}{(no mgus, undecidable, modulo $\alpha\beta$)}\bigskip |
138 \textcolor{darkgray}{(no mgus, undecidable, modulo $\alpha\beta$)}\bigskip |
139 \item Higher-Order Pattern Unification\\ |
139 \item Higher-Order Pattern Unification\\ |
959 \end{center}\bigskip\bigskip |
959 \end{center}\bigskip\bigskip |
960 \pause |
960 \pause |
961 |
961 |
962 \item The alternative rule |
962 \item The alternative rule |
963 |
963 |
964 %\begin{center}\small |
964 \begin{center}\small |
965 %\colorbox{cream}{ |
965 \colorbox{cream}{ |
966 %\smath{\{a.t \eqprob b.t'\}\cup P \redu{\id} \{\swap{a}{c}\act t \eqprob \swap{b}{c}\act t', a \freshprob t'\} \cup P}} |
966 \begin{tabular}{@ {}l@ {}} |
967 %\end{center} |
967 \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id}}\\ |
|
968 \mbox{}\hspace{2cm}\smath{\{\swap{a}{c}\act t \eqprob |
|
969 \swap{b}{c}\act t', c \freshprob t, c \freshprob t'\} \cup P} |
|
970 \end{tabular}} |
|
971 \end{center} |
968 |
972 |
969 |
973 leads to a more complicated notion of mgu.\medskip\pause |
970 leads to a more complicated notion of mgu. |
974 |
|
975 \footnotesize |
|
976 \smath{\{a.X \eqprob b.Y\} \redu{} (\{a\fresh Y, c\fresh Y\}, [X:=\swap{a}{c}\swap{b}{c}\act Y])} |
971 \end{itemize} |
977 \end{itemize} |
972 |
978 |
973 \end{frame}} |
979 \end{frame}} |
974 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
980 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
975 *} |
981 *} |
1001 \begin{textblock}{6}(1.5,0.5) |
1007 \begin{textblock}{6}(1.5,0.5) |
1002 \begin{tikzpicture} |
1008 \begin{tikzpicture} |
1003 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
1009 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
1004 {\color{darkgray} |
1010 {\color{darkgray} |
1005 \begin{minipage}{9cm}\raggedright |
1011 \begin{minipage}{9cm}\raggedright |
1006 {\bf Problem:} If we ask whether |
1012 {\bf One problem:} If we ask whether |
1007 |
1013 |
1008 \begin{center} |
1014 \begin{center} |
1009 ?- type ([(x, T')], lam(x.Var(x)), T) |
1015 ?- type ([(x, T')], lam(x.Var(x)), T) |
1010 \end{center} |
1016 \end{center} |
1011 |
1017 |
1025 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1031 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1026 \mode<presentation>{ |
1032 \mode<presentation>{ |
1027 \begin{frame}<1-> |
1033 \begin{frame}<1-> |
1028 \frametitle{Equivariant Unification} |
1034 \frametitle{Equivariant Unification} |
1029 |
1035 |
1030 James Cheney |
1036 James Cheney proposed |
1031 |
1037 |
1032 \begin{center} |
1038 \begin{center} |
1033 \colorbox{cream}{ |
1039 \colorbox{cream}{ |
1034 \smath{t \eqprob t' \redu{\nabla, \sigma, \pi} |
1040 \smath{t \eqprob t' \redu{\nabla, \sigma, \pi} |
1035 \nabla \vdash \sigma(t) \approx \pi \act \sigma(t')}} |
1041 \nabla \vdash \sigma(t) \approx \pi \act \sigma(t')}} |
1036 \end{center}\bigskip\bigskip |
1042 \end{center}\bigskip\bigskip |
1037 \pause |
1043 \pause |
1038 |
1044 |
1039 He also showed that this is undecidable in general. :( |
1045 But he also showed this problem is undecidable\\ in general. :( |
1040 |
1046 |
1041 \end{frame}} |
1047 \end{frame}} |
1042 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1048 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1043 *} |
1049 *} |
1044 |
1050 |
1052 \pause |
1058 \pause |
1053 |
1059 |
1054 Unfortunately this breaks the mgu-property: |
1060 Unfortunately this breaks the mgu-property: |
1055 |
1061 |
1056 \begin{center} |
1062 \begin{center} |
1057 |
1063 \smath{a.Z \eqprob X.Y.v(a)} |
1058 \end{center} |
1064 \end{center} |
1059 |
1065 |
1060 \end{frame}} |
1066 can be solved by |
1061 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1067 |
1062 *} |
1068 \begin{center} |
1063 |
1069 \smath{[X:=a, Z:=Y.v(a)]} and |
1064 text_raw {* |
1070 \smath{[Y:=a, Z:=Y.v(Y)]} |
1065 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1071 \end{center} |
1066 \mode<presentation>{ |
1072 |
1067 \begin{frame}<1> |
1073 \end{frame}} |
|
1074 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1075 *} |
|
1076 |
|
1077 text_raw {* |
|
1078 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1079 \mode<presentation>{ |
|
1080 \begin{frame}<1>[c] |
1068 \frametitle{HOPU vs. NOMU} |
1081 \frametitle{HOPU vs. NOMU} |
1069 |
1082 |
1070 \begin{itemize} |
1083 \begin{itemize} |
1071 \item James Cheney showed\bigskip |
1084 \item James Cheney showed\bigskip |
1072 \begin{center} |
1085 \begin{center} |
1073 \colorbox{cream}{\smath{HOPU \Rightarrow NOMU}} |
1086 \colorbox{cream}{\smath{HOPU \Rightarrow NOMU}} |
1074 \end{center}\bigskip |
1087 \end{center}\bigskip |
1075 |
1088 |
1076 \item Levi\bigskip |
1089 \item Jordi Levy and Mateu Villaret established\bigskip |
1077 \begin{center} |
1090 \begin{center} |
1078 \colorbox{cream}{\smath{HOPU \Leftarrow NOMU}} |
1091 \colorbox{cream}{\smath{HOPU \Leftarrow NOMU}} |
1079 \end{center}\bigskip |
1092 \end{center}\bigskip |
1080 \end{itemize} |
1093 \end{itemize} |
1081 |
1094 |
1121 \mode<presentation>{ |
1134 \mode<presentation>{ |
1122 \begin{frame}<1> |
1135 \begin{frame}<1> |
1123 \frametitle{Complexity} |
1136 \frametitle{Complexity} |
1124 |
1137 |
1125 \begin{itemize} |
1138 \begin{itemize} |
1126 \item Maribel Fernandez |
1139 \item Christiopher Calves and Maribel Fernandez showed first that |
1127 |
1140 it is polynomial and then also quadratic |
1128 \item Levi |
1141 |
1129 |
1142 \item Jordi Levy and Mateu Villaret showed that it is quadratic |
|
1143 by a translation into a subset of NOMU and using ideas from |
|
1144 Martelli/Montenari. |
1130 |
1145 |
1131 \end{itemize} |
1146 \end{itemize} |
1132 |
1147 |
1133 \end{frame}} |
1148 \end{frame}} |
1134 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1149 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1141 \begin{frame}<1->[c] |
1156 \begin{frame}<1->[c] |
1142 \frametitle{Conclusion} |
1157 \frametitle{Conclusion} |
1143 |
1158 |
1144 \begin{itemize} |
1159 \begin{itemize} |
1145 \item Nominal Unification is a completely first-order |
1160 \item Nominal Unification is a completely first-order |
1146 language, but implements unification modulo $\alpha$.\medskip\pause |
1161 language, but implements unification modulo $\alpha$. |
|
1162 \textcolor{gray}{(verification\ldots Ramana Kumar and Michael Norrish)} |
|
1163 \medskip\pause |
1147 |
1164 |
1148 \item NOMU has been applied in term-rewriting and |
1165 \item NOMU has been applied in term-rewriting and |
1149 logic programming. I hope it will also be used in typing |
1166 logic programming. \textcolor{gray}{(Maribel Fernandez et |
|
1167 al has a KB-completion procedure.)} |
|
1168 I hope it will also be used in typing |
1150 systems.\medskip\pause |
1169 systems.\medskip\pause |
1151 |
1170 |
1152 \item NOMU and HOPU are `equivalent' (it took a long time |
1171 \item NOMU and HOPU are `equivalent' (it took a long time |
1153 and considerable time to find this out).\medskip\pause |
1172 and considerable research to find this out).\medskip\pause |
1154 |
1173 |
1155 \item The question about complexity is still an ongoing |
1174 \item The question about complexity is still an ongoing |
1156 story.\medskip |
1175 story.\medskip |
1157 \end{itemize} |
1176 \end{itemize} |
1158 |
1177 |
1166 \mode<presentation>{ |
1185 \mode<presentation>{ |
1167 \begin{frame}<1>[c] |
1186 \begin{frame}<1>[c] |
1168 \frametitle{ |
1187 \frametitle{ |
1169 \begin{tabular}{c} |
1188 \begin{tabular}{c} |
1170 \mbox{}\\[23mm] |
1189 \mbox{}\\[23mm] |
1171 \alert{\LARGE Thank you very much}\\ |
1190 \alert{\LARGE Thank you very much!}\\ |
1172 \alert{\Large Questions?} |
1191 \alert{\Large Questions?} |
1173 \end{tabular}} |
1192 \end{tabular}} |
1174 |
1193 |
1175 \end{frame}} |
1194 \end{frame}} |
1176 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |