1177 calculated below for each argument. |
1177 calculated below for each argument. |
1178 First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, |
1178 First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, |
1179 we can determine whether the argument is a shallow or deep |
1179 we can determine whether the argument is a shallow or deep |
1180 binder, and in the latter case also whether it is a recursive or |
1180 binder, and in the latter case also whether it is a recursive or |
1181 non-recursive binder. |
1181 non-recursive binder. |
1182 |
1182 % |
1183 \begin{center} |
1183 \begin{equation}\label{deepbinder} |
|
1184 \mbox{% |
1184 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1185 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1185 $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\ |
1186 $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\ |
1186 $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep |
1187 $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep |
1187 non-recursive binder with the auxiliary binding function @{text "bn"}\\ |
1188 non-recursive binder with the auxiliary binding function @{text "bn"}\\ |
1188 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is |
1189 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is |
1189 a deep recursive binder with the auxiliary binding function @{text "bn"} |
1190 a deep recursive binder with the auxiliary binding function @{text "bn"} |
1190 \end{tabular} |
1191 \end{tabular}} |
1191 \end{center} |
1192 \end{equation} |
1192 |
1193 |
1193 \noindent |
1194 \noindent |
1194 The first clause states that shallow binders do not contribute to the |
1195 The first clause states that shallow binders do not contribute to the |
1195 free variables; in the second clause, we have to collect all |
1196 free variables; in the second clause, we have to collect all |
1196 variables that are left unbound by the binding function @{text "bn"}---this |
1197 variables that are left unbound by the binding function @{text "bn"}---this |
1228 |
1229 |
1229 The last case we need to consider is when @{text "x\<^isub>i"} is neither |
1230 The last case we need to consider is when @{text "x\<^isub>i"} is neither |
1230 a binder nor a body of an abstraction. In this case it is defined |
1231 a binder nor a body of an abstraction. In this case it is defined |
1231 as in \eqref{deepbody}, except that we do not need to subtract the |
1232 as in \eqref{deepbody}, except that we do not need to subtract the |
1232 set @{text bnds}. |
1233 set @{text bnds}. |
1233 |
1234 |
1234 Next, we need to define a free-variable function @{text "fv_bn\<^isub>j"} for |
1235 The definitions of the free-variable functions for binding |
1235 each binding function @{text "bn\<^isub>j"}. The idea behind these |
1236 functions are similar. For each binding function |
1236 functions is to compute the set of free atoms that are not bound by |
1237 @{text "bn\<^isub>j"} we need to define a free-variable function |
1237 @{text "bn\<^isub>j"}. Because of the restrictions we imposed on the |
1238 @{text "fv_bn\<^isub>j"}. Given a term-constructor @{term "C"}, the |
1238 form of binding functions, this can be done automatically by recursively |
1239 function @{text "fv_bn\<^isub>j(C x\<^isub>1 \<dots> x\<^isub>n)"} is the union of the |
1239 building up the the set of free variables from the arguments that are |
1240 values calculated for the arguments. For each argument @{term "x\<^isub>i"} |
1240 not bound. Let us assume one clause of a binding function is |
1241 we know whether it appears in the @{term "rhs"} of the binding |
1241 @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n)"} is the |
1242 function equation @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. If it does not |
1242 union of the values calculated for @{text "x\<^isub>i"} as follows: |
1243 appear in @{text "rhs"} we generate the premise according to the |
|
1244 rules for @{text "fv_ty"} described above in (\ref{deepbinder}--\ref{deepbody}). Otherwise: |
1243 |
1245 |
1244 \begin{center} |
1246 \begin{center} |
1245 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1247 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1246 \multicolumn{2}{l}{@{text "x\<^isub>i"} occurs in @{text "rhs"}:}\\ |
1248 $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "rhs"} contains the |
1247 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom, |
1249 recursive call @{text "bn x\<^isub>i"}\medskip\\ |
1248 atom list or atom set\\ |
1250 $\bullet$ & @{term "{}"} provided @{text "rhs"} contains |
1249 $\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the |
1251 @{term "x\<^isub>i"} without a recursive call. |
1250 recursive call @{text "bn x\<^isub>i"}\medskip\\ |
|
1251 \end{tabular} |
|
1252 \end{center} |
|
1253 |
|
1254 \begin{center} |
|
1255 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
|
1256 \multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\ |
|
1257 $\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\ |
|
1258 $\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
|
1259 $\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
|
1260 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is the type of @{text "x\<^isub>i"} and one of the raw |
|
1261 types corresponding to the types specified by the user\\ |
|
1262 % $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>i - bnds"} provided @{term "x\<^isub>i"} is not in @{text "rhs"} |
|
1263 % and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\ |
|
1264 $\bullet$ & @{term "{}"} otherwise |
|
1265 \end{tabular} |
1252 \end{tabular} |
1266 \end{center} |
1253 \end{center} |
1267 |
1254 |
1268 \noindent |
1255 \noindent |
1269 To see how these definitions work in practise, let us reconsider the term-constructors |
1256 To see how these definitions work in practise, let us reconsider the term-constructors |