1156 \end{center} |
1156 \end{center} |
1157 |
1157 |
1158 \noindent |
1158 \noindent |
1159 In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of |
1159 In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of |
1160 one or more abstractions. Let @{text "bnds"} be the bound atoms computed |
1160 one or more abstractions. Let @{text "bnds"} be the bound atoms computed |
1161 as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{text "{}"}. |
1161 as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}. |
1162 Otherwise there are two cases: either the |
1162 Otherwise there are two cases: either the |
1163 corresponding binders are all shallow or there is a single deep binder. |
1163 corresponding binders are all shallow or there is a single deep binder. |
1164 In the former case we build the union of all shallow binders; in the |
1164 In the former case we build the union of all shallow binders; in the |
1165 later case we just take set or list of atoms the specified binding |
1165 later case we just take set or list of atoms the specified binding |
1166 function returns. With @{text "bnds"} computed as above the value of |
1166 function returns. With @{text "bnds"} computed as above the value of |
1167 for @{text "x\<^isub>i"} is given by: |
1167 for @{text "x\<^isub>i"} is given by: |
1168 |
1168 |
1169 \begin{center} |
1169 \begin{center} |
1170 \begin{tabular}{cp{7cm}} |
1170 \begin{tabular}{cp{7cm}} |
1171 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1171 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1172 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1172 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1173 $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
1173 $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
1174 $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ |
1174 $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes |
1175 $\bullet$ & @{term "{}"} otherwise |
1175 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
1176 \end{tabular} |
1176 $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype |
1177 \end{center} |
1177 with a free variable function @{text "fv\<^isup>\<alpha>"}\\\\ |
1178 |
1178 $\bullet$ & @{term "{}"} otherwise |
1179 \marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?} |
1179 \end{tabular} |
|
1180 \end{center} |
1180 |
1181 |
1181 \noindent Next, for each binding function @{text "bn"} we define a |
1182 \noindent Next, for each binding function @{text "bn"} we define a |
1182 free variable function @{text "fv_bn"}. The basic idea behind this |
1183 free variable function @{text "fv_bn"}. The basic idea behind this |
1183 function is to compute all the free atoms under this binding |
1184 function is to compute all the free atoms under this binding |
1184 function. So given that @{text "bn"} is a binding function for type |
1185 function. So given that @{text "bn"} is a binding function for type |
1187 |
1188 |
1188 For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, |
1189 For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, |
1189 we define @{text "fv_bn"} to be the union of the values calculated |
1190 we define @{text "fv_bn"} to be the union of the values calculated |
1190 for @{text "x\<^isub>j"} as follows: |
1191 for @{text "x\<^isub>j"} as follows: |
1191 |
1192 |
1192 \marginpar{raw for being defined} |
|
1193 |
|
1194 \begin{center} |
1193 \begin{center} |
1195 \begin{tabular}{cp{7cm}} |
1194 \begin{tabular}{cp{7cm}} |
1196 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\ |
1195 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom, |
|
1196 atom list or atom set\\ |
1197 $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1197 $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1198 with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ |
1198 with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ |
1199 $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\ |
1199 $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\ |
1200 $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\ |
1200 $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\ |
1201 $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype |
1201 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is |
1202 with a free variable function @{text "fv_ty"}. This includes the types being |
1202 one of the datatypes |
1203 defined, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\ |
1203 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
|
1204 $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} |
|
1205 and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\ |
1204 $\bullet$ & @{term "{}"} otherwise |
1206 $\bullet$ & @{term "{}"} otherwise |
1205 \end{tabular} |
1207 \end{tabular} |
1206 \end{center} |
1208 \end{center} |
1207 |
1209 |
1208 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1210 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1217 functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define |
1219 functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define |
1218 \begin{center} |
1220 \begin{center} |
1219 @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"} |
1221 @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"} |
1220 \end{center} |
1222 \end{center} |
1221 |
1223 |
1222 Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances |
1224 Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances |
1223 of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there |
1225 of this constructor are alpha-equivalent @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if there |
1224 exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that |
1226 exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that |
1225 the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds. |
1227 the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds. |
1226 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if: |
1228 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if: |
1227 |
1229 |
1228 \begin{center} |
1230 \begin{center} |
1229 \begin{tabular}{cp{7cm}} |
1231 \begin{tabular}{cp{7cm}} |
1230 $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\ |
1232 $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\ |
1232 with the auxiliary binding function @{text "bn\<^isub>m"}\\ |
1234 with the auxiliary binding function @{text "bn\<^isub>m"}\\ |
1233 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x\<^isub>n)) \<approx>gen R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"} |
1235 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x\<^isub>n)) \<approx>gen R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"} |
1234 provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1236 provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1235 function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound |
1237 function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound |
1236 free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and |
1238 free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and |
1237 @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>n"}\\ |
1239 @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\ |
1238 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
1240 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
1239 $\bullet$ & @{term "(x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"} |
1241 $\bullet$ & @{term "({x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} has |
1240 is bound in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1242 a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1241 alpha-equivalence for @{term "x\<^isub>j"} |
1243 alpha-equivalence for @{term "x\<^isub>j"} |
1242 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1244 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1243 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "bn\<^isub>m x\<^isub>n"} |
1245 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} |
1244 is bound non-recursively in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1246 has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1245 alpha-equivalence for @{term "x\<^isub>j"} |
1247 alpha-equivalence for @{term "x\<^isub>j"} |
1246 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1248 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1247 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes |
1249 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes |
1248 the types being defined, raw)\\ |
1250 the types being defined, raw)\\ |
1249 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1251 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1252 |
1254 |
1253 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences |
1255 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences |
1254 for their respective types, the difference is that they ommit checking the arguments that |
1256 for their respective types, the difference is that they ommit checking the arguments that |
1255 are bound. We assumed that there are no bindings in the type on which the binding function |
1257 are bound. We assumed that there are no bindings in the type on which the binding function |
1256 is defined so, there are no permutations involved. For a binding function clause |
1258 is defined so, there are no permutations involved. For a binding function clause |
1257 @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent |
1259 @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent |
1258 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if: |
1260 @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if: |
1259 \begin{center} |
1261 \begin{center} |
1260 \begin{tabular}{cp{7cm}} |
1262 \begin{tabular}{cp{7cm}} |
1261 $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\ |
1263 $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\ |
1262 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not a nominal datatype and does not occur in @{text "rhs"}\\ |
1264 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not a nominal datatype and does not occur in @{text "rhs"}\\ |
1263 $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a nominal datatype occuring in @{text "rhs"} |
1265 $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a nominal datatype occuring in @{text "rhs"} |