1120 \end{center} |
1120 \end{center} |
1121 |
1121 |
1122 \noindent |
1122 \noindent |
1123 In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of |
1123 In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of |
1124 one or more abstractions. Let @{text "bnds"} be the bound atoms computed |
1124 one or more abstractions. Let @{text "bnds"} be the bound atoms computed |
1125 as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{text "{}"}. |
1125 as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}. |
1126 Otherwise there are two cases: either the |
1126 Otherwise there are two cases: either the |
1127 corresponding binders are all shallow or there is a single deep binder. |
1127 corresponding binders are all shallow or there is a single deep binder. |
1128 In the former case we build the union of all shallow binders; in the |
1128 In the former case we build the union of all shallow binders; in the |
1129 later case we just take set or list of atoms the specified binding |
1129 later case we just take set or list of atoms the specified binding |
1130 function returns. With @{text "bnds"} computed as above the value of |
1130 function returns. With @{text "bnds"} computed as above the value of |
1131 for @{text "x\<^isub>i"} is given by: |
1131 for @{text "x\<^isub>i"} is given by: |
1132 |
1132 |
1133 \begin{center} |
1133 \begin{center} |
1134 \begin{tabular}{cp{7cm}} |
1134 \begin{tabular}{cp{7cm}} |
1135 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1135 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1136 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1136 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1137 $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
1137 $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
1138 $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ |
1138 $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes |
1139 $\bullet$ & @{term "{}"} otherwise |
1139 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
1140 \end{tabular} |
1140 $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype |
1141 \end{center} |
1141 with a free variable function @{text "fv\<^isup>\<alpha>"}\\\\ |
1142 |
1142 $\bullet$ & @{term "{}"} otherwise |
1143 \marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?} |
1143 \end{tabular} |
|
1144 \end{center} |
1144 |
1145 |
1145 \noindent Next, for each binding function @{text "bn"} we define a |
1146 \noindent Next, for each binding function @{text "bn"} we define a |
1146 free variable function @{text "fv_bn"}. The basic idea behind this |
1147 free variable function @{text "fv_bn"}. The basic idea behind this |
1147 function is to compute all the free atoms under this binding |
1148 function is to compute all the free atoms under this binding |
1148 function. So given that @{text "bn"} is a binding function for type |
1149 function. So given that @{text "bn"} is a binding function for type |
1151 |
1152 |
1152 For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, |
1153 For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, |
1153 we define @{text "fv_bn"} to be the union of the values calculated |
1154 we define @{text "fv_bn"} to be the union of the values calculated |
1154 for @{text "x\<^isub>j"} as follows: |
1155 for @{text "x\<^isub>j"} as follows: |
1155 |
1156 |
1156 \marginpar{raw for being defined} |
|
1157 |
|
1158 \begin{center} |
1157 \begin{center} |
1159 \begin{tabular}{cp{7cm}} |
1158 \begin{tabular}{cp{7cm}} |
1160 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\ |
1159 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom, |
|
1160 atom list or atom set\\ |
1161 $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1161 $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1162 with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ |
1162 with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ |
1163 $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\ |
1163 $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\ |
1164 $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\ |
1164 $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\ |
1165 $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype |
1165 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is |
1166 with a free variable function @{text "fv_ty"}. This includes the types being |
1166 one of the datatypes |
1167 defined, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\ |
1167 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
|
1168 $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} |
|
1169 and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\ |
1168 $\bullet$ & @{term "{}"} otherwise |
1170 $\bullet$ & @{term "{}"} otherwise |
1169 \end{tabular} |
1171 \end{tabular} |
1170 \end{center} |
1172 \end{center} |
1171 |
1173 |
1172 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1174 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |