1052 since there is no overlap of binders. |
1052 since there is no overlap of binders. |
1053 |
1053 |
1054 Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}. |
1054 Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}. |
1055 Whenever such a binding clause is present, we will call the binder \emph{recursive}. |
1055 Whenever such a binding clause is present, we will call the binder \emph{recursive}. |
1056 To see the purpose for this, compare ``plain'' Lets and Let\_recs: |
1056 To see the purpose for this, compare ``plain'' Lets and Let\_recs: |
1057 |
1057 % |
1058 \begin{center} |
1058 \begin{equation}\label{letrecs} |
|
1059 \mbox{% |
1059 \begin{tabular}{@ {}l@ {}} |
1060 \begin{tabular}{@ {}l@ {}} |
1060 \isacommand{nominal\_datatype} {\it trm} =\\ |
1061 \isacommand{nominal\_datatype}~@{text "trm ="}\\ |
1061 \hspace{5mm}\phantom{$\mid$}\ldots\\ |
1062 \hspace{5mm}\phantom{$\mid$}\ldots\\ |
1062 \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm} |
1063 \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} |
1063 \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\ |
1064 \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\ |
1064 \hspace{5mm}$\mid$ Let\_rec\;{\it a::assn}\; {\it t::trm} |
1065 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} |
1065 \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}, |
1066 \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}, |
1066 \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\ |
1067 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\ |
1067 \isacommand{and} {\it assn} =\\ |
1068 \isacommand{and} {\it assn} =\\ |
1068 \hspace{5mm}\phantom{$\mid$} ANil\\ |
1069 \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ |
1069 \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\ |
1070 \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\ |
1070 \isacommand{with} {\it bn::assn $\Rightarrow$ atom list}\\ |
1071 \isacommand{with} @{text "bn::assn \<Rightarrow> atom list"}\\ |
1071 \isacommand{where} $bn(\textrm{ANil}) = []$\\ |
1072 \isacommand{where}~@{text "bn(ANil) = []"}\\ |
1072 \hspace{5mm}$\mid$ $bn(\textrm{ACons}\;x\;t\;a) = [atom\; x]\; @\; bn(a)$\\ |
1073 \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\ |
1073 \end{tabular} |
1074 \end{tabular}} |
1074 \end{center} |
1075 \end{equation} |
1075 |
1076 |
1076 \noindent |
1077 \noindent |
1077 The difference is that with Let we only want to bind the atoms @{text |
1078 The difference is that with Let we only want to bind the atoms @{text |
1078 "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms |
1079 "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms |
1079 inside the assignment. This requires recursive binders and also has |
1080 inside the assignment. This requires recursive binders and also has |
1234 % $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} |
1235 % $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} |
1235 % and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\ |
1236 % and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\ |
1236 $\bullet$ & @{term "{}"} otherwise |
1237 $\bullet$ & @{term "{}"} otherwise |
1237 \end{tabular} |
1238 \end{tabular} |
1238 \end{center} |
1239 \end{center} |
|
1240 |
|
1241 \noindent |
|
1242 To see how these definitions work, let us consider the term-constructors |
|
1243 for @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. |
|
1244 For this specification we need to define three functions, namely |
|
1245 @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. |
|
1246 % |
|
1247 \begin{center} |
|
1248 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
|
1249 @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "fv\<^bsub>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\ |
|
1250 @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\ |
|
1251 \multicolumn{3}{r}{@{text "(fv\<^bsub>assn\<^esub> as - set (bn as)) \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}}\\[1mm] |
|
1252 |
|
1253 @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\ |
|
1254 @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm] |
|
1255 |
|
1256 @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\ |
|
1257 @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"} |
|
1258 \end{tabular} |
|
1259 \end{center} |
|
1260 |
|
1261 \noindent |
|
1262 Since there are no binding clauses for the term-constructors @{text ANil} |
|
1263 and @{text "ACons"}, the corresponding free-variable function @{text |
|
1264 "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The |
|
1265 binding happens in @{text Let} and @{text "Let_rec"}. In the first clause we |
|
1266 want to bind all atoms given by @{text "set (bn as)"} in @{text |
|
1267 t}. Therefore we have to subtract @{text "set (bn as)"} from @{text |
|
1268 "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are |
|
1269 free in @{text "as"}. This is what the purpose of the function @{text |
|
1270 "fv\<^bsub>bn\<^esub>"} is. In contrast, in @{text "Let_rec"} we have a |
|
1271 recursive binder where we want to also bind all occurences of atoms inside |
|
1272 @{text "as"}. Therefore we have to subtract @{text "set (bn as)"} from |
|
1273 @{text "fv\<^bsub>assn\<^esub> as"}. Similarly for @{text |
|
1274 "fv\<^bsub>trm\<^esub> t - bn as"}. An interesting point in this example is |
|
1275 that an assignment ``alone'' does not have any bound variables. Only in the |
|
1276 context of a @{text Let} pr @{text "Let_rec"} will some atoms occuring in an |
|
1277 assignment become bound. This is a phenomenon that has also been pointed out |
|
1278 in \cite{ott-jfp}. |
1239 |
1279 |
1240 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1280 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1241 we need to define |
1281 we need to define |
1242 |
1282 |
1243 \begin{center} |
1283 \begin{center} |