1256 $\bullet$ & @{term "{}"} otherwise |
1256 $\bullet$ & @{term "{}"} otherwise |
1257 \end{tabular} |
1257 \end{tabular} |
1258 \end{center} |
1258 \end{center} |
1259 |
1259 |
1260 \noindent |
1260 \noindent |
1261 To see how these definitions work, let us consider again the term-constructors |
1261 To see how these definitions work in practise, let us reconsider the term-constructors |
1262 @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. |
1262 @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. |
1263 For this specification we need to define three functions, namely |
1263 For this specification we need to define three functions, namely |
1264 @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows: |
1264 @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows: |
1265 % |
1265 % |
1266 \begin{center} |
1266 \begin{center} |
1291 @{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text |
1291 @{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text |
1292 "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from |
1292 "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from |
1293 @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is |
1293 @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is |
1294 that an assignment ``alone'' does not have any bound variables. Only in the |
1294 that an assignment ``alone'' does not have any bound variables. Only in the |
1295 context of a @{text Let} or @{text "Let_rec"} will some atoms become bound |
1295 context of a @{text Let} or @{text "Let_rec"} will some atoms become bound |
1296 (teh term-constructors that have binding clauses). This is a phenomenon |
1296 (the term-constructors that have binding clauses). This is a phenomenon |
1297 that has also been pointed out in \cite{ott-jfp}. |
1297 that has also been pointed out in \cite{ott-jfp}. We can also see that |
1298 |
1298 given a @{text "bn"}-function for a type @{text "ty"}, then we have |
1299 Next we define alpha-equivalence realtions for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them |
1299 % |
1300 @{text "\<approx>ty\<^isub>1 \<dots> \<approx>ty\<^isub>n"}. Like with the free-variable functions, |
1300 \begin{equation}\label{bnprop} |
|
1301 @{text "fv_ty x = bn x \<union> fv_bn x"}. |
|
1302 \end{equation} |
|
1303 |
|
1304 Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them |
|
1305 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, |
1301 we also need to define auxiliary alpha-equivalence relations for the binding functions. |
1306 we also need to define auxiliary alpha-equivalence relations for the binding functions. |
1302 Say we have @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"}, we also define @{text "\<approx>bn_ty\<^isub>1 \<dots> \<approx>bn_ty\<^isub>n"}. |
1307 Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}. |
|
1308 To simplify our definitions we will use the following abbreviations for |
|
1309 relations and free-variable acting on products. |
|
1310 % |
|
1311 \begin{center} |
|
1312 \begin{tabular}{rcl} |
|
1313 @{text "(x\<^isub>1, y\<^isub>1) R\<^isub>1 \<otimes> R\<^isub>2 (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\ |
|
1314 @{text "fv\<^isub>1 \<oplus> fv\<^isub>2 (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\ |
|
1315 \end{tabular} |
|
1316 \end{center} |
|
1317 |
1303 |
1318 |
1304 The relations are inductively defined predicates, whose clauses have |
1319 The relations are inductively defined predicates, whose clauses have |
1305 conclusions of the form @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume |
1320 conclusions of the form @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume |
1306 @{text C} is of type @{text ty} and its arguments are specified as @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}). |
1321 @{text C} is of type @{text ty} and its arguments are specified as @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}). |
1307 The task is to specify what the premises of these clauses are. For this we |
1322 The task is to specify what the premises of these clauses are. For this we |
1309 @{text "ty\<^isub>i"}. For each of these pairs we calculate a premise as follows. |
1324 @{text "ty\<^isub>i"}. For each of these pairs we calculate a premise as follows. |
1310 |
1325 |
1311 \begin{center} |
1326 \begin{center} |
1312 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1327 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1313 \multicolumn{2}{l}{@{text "x\<^isub>i"} is a binder:}\\ |
1328 \multicolumn{2}{l}{@{text "x\<^isub>i"} is a binder:}\\ |
1314 $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a shallow binder\\ |
1329 $\bullet$ & none provided @{text "x\<^isub>i"} is a shallow binder\\ |
1315 $\bullet$ & @{text "x\<^isub>i \<approx>bn_ty\<^isub>i y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep |
1330 $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep |
1316 non-recursive binder\\ |
1331 non-recursive binder with the auxiliary binding function @{text bn}\\ |
1317 $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a deep |
1332 $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a deep |
1318 recursive binder\\ |
1333 recursive binder\\ |
1319 \end{tabular} |
1334 \end{tabular} |
1320 \end{center} |
1335 \end{center} |
1321 |
1336 |