1087 \begin{center} |
1087 \begin{center} |
1088 @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"} |
1088 @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"} |
1089 \end{center} |
1089 \end{center} |
1090 |
1090 |
1091 \noindent |
1091 \noindent |
1092 and given binding functions @{text "bn_ty\<^isub>1, \<dots>, bn_ty\<^isub>m"} we also need to define |
1092 We define them together with the auxiliary free variable functions for |
1093 the free-variable functions |
1093 binding functions |
1094 |
1094 |
1095 \begin{center} |
1095 \begin{center} |
1096 @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"} |
1096 @{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"} |
1097 \end{center} |
1097 \end{center} |
1098 |
1098 |
1099 \noindent |
1099 \noindent |
1100 The basic idea behind these free-variable functions is to collect all atoms |
1100 The basic idea behind these free-variable functions is to collect all atoms |
1101 that are not bound in a term constructor, but because of the rather |
1101 that are not bound in a term constructor, but because of the rather |
1109 whether it is a recursive or non-recursive of a binder. In these cases the value is: |
1109 whether it is a recursive or non-recursive of a binder. In these cases the value is: |
1110 |
1110 |
1111 \begin{center} |
1111 \begin{center} |
1112 \begin{tabular}{cp{7cm}} |
1112 \begin{tabular}{cp{7cm}} |
1113 $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\ |
1113 $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\ |
1114 $\bullet$ & @{text "ft_bn_by\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\ |
1114 $\bullet$ & @{text "fv_bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep |
1115 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep recursive binder\\ |
1115 non-recursive binder with the auxiliary function @{text "bn\<^isub>j"}\\ |
|
1116 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is |
|
1117 a deep recursive binder with the auxiliary function @{text "bn\<^isub>j"} |
1116 \end{tabular} |
1118 \end{tabular} |
1117 \end{center} |
1119 \end{center} |
1118 |
1120 |
1119 \noindent |
1121 \noindent |
1120 In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of |
1122 In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of |
1121 one or more abstractions. There are two cases: either the |
1123 one or more abstractions. Let @{text "bnds"} be the bound atoms computed |
1122 corresponding binders are all shallow or there is a single deep binder. |
1124 as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{text "{}"}. |
1123 In the former case we build the union of all shallow binders; in the |
1125 Otherwise there are two cases: either the |
|
1126 corresponding binders are all shallow or there is a single deep binder. |
|
1127 In the former case we build the union of all shallow binders; in the |
1124 later case we just take set or list of atoms the specified binding |
1128 later case we just take set or list of atoms the specified binding |
1125 function returns. Let @{text "bnds"} be an abbreviation of the bound |
1129 function returns. With @{text "bnds"} computed as above the value of |
1126 atoms. Then the value is given by: |
1130 for @{text "x\<^isub>i"} is given by: |
1127 |
1131 |
1128 \begin{center} |
1132 \begin{center} |
1129 \begin{tabular}{cp{7cm}} |
1133 \begin{tabular}{cp{7cm}} |
1130 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1134 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1131 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1135 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1133 $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ |
1137 $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ |
1134 $\bullet$ & @{term "{}"} otherwise |
1138 $\bullet$ & @{term "{}"} otherwise |
1135 \end{tabular} |
1139 \end{tabular} |
1136 \end{center} |
1140 \end{center} |
1137 |
1141 |
1138 \noindent |
1142 \marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?} |
1139 If the argument is neither a binder, nor a body of an abstraction, then the |
1143 |
1140 value is defined as above, except that @{text "bnds"} is empty. i.e.~no atoms |
1144 |
1141 are abstracted. |
1145 \noindent Next, for each binding function @{text "bn"} we define a |
1142 |
1146 free variable function @{text "fv_bn"}. The basic idea behind this |
1143 TODO |
1147 function is to compute all the free atoms under this binding |
1144 |
1148 function. So given that @{text "bn"} is a binding function for type |
1145 Given a clause of a binding function of the form |
1149 @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the |
1146 |
1150 omission of the arguments present in @{text "bn"}. |
1147 \begin{center} |
1151 |
1148 @{text "bn_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"} |
1152 For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, |
1149 \end{center} |
1153 we define @{text "fv_bn"} to be the union of the values calculated |
1150 |
1154 for @{text "x\<^isub>j"} as follows: |
1151 \noindent |
|
1152 then the corresponding free-variable function @{text "fv_bn_ty\<^isub>i"} is the |
|
1153 union of the values calculated for the @{text "x\<^isub>j"} as follows: |
|
1154 |
1155 |
1155 \begin{center} |
1156 \begin{center} |
1156 \begin{tabular}{cp{7cm}} |
1157 \begin{tabular}{cp{7cm}} |
1157 $\bullet$ & @{text "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\ |
1158 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\ |
1158 $\bullet$ & @{text "fv_bn_ty x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1159 $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1159 with the recursive call @{text "bn_ty x\<^isub>j"}\\ |
1160 with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ |
1160 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1161 $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\ |
1161 $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
1162 $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\ |
1162 $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ |
1163 $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype |
|
1164 with a free variable function @{text "fv_ty"}. This includes the currently defined |
|
1165 types, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\ |
1163 $\bullet$ & @{term "{}"} otherwise |
1166 $\bullet$ & @{term "{}"} otherwise |
1164 \end{tabular} |
1167 \end{tabular} |
1165 \end{center} |
1168 \end{center} |
1166 |
1169 |
1167 *} |
1170 *} |