equal
deleted
inserted
replaced
726 abstracting a set of atoms over types (as in type-schemes). We set |
726 abstracting a set of atoms over types (as in type-schemes). We set |
727 @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we |
727 @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we |
728 define |
728 define |
729 |
729 |
730 \[ |
730 \[ |
731 @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"} |
731 @{text "fa(x) \<equiv> {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"} |
732 \]\smallskip |
732 \]\smallskip |
733 |
733 |
734 \noindent |
734 \noindent |
735 Now recall the examples shown in \eqref{ex1} and |
735 Now recall the examples shown in \eqref{ex1} and |
736 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and |
736 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and |
750 abstract a single atom. |
750 abstract a single atom. |
751 |
751 |
752 In the rest of this section we are going to show that the alpha-equivalences really |
752 In the rest of this section we are going to show that the alpha-equivalences really |
753 lead to abstractions where some atoms are bound (more precisely removed from the |
753 lead to abstractions where some atoms are bound (more precisely removed from the |
754 support). For this we are going to introduce |
754 support). For this we are going to introduce |
755 three abstraction types that are quotients with respect to the relations |
755 three abstraction types that are quotients of the relations |
756 |
756 |
757 \begin{equation} |
757 \begin{equation} |
758 \begin{array}{r} |
758 \begin{array}{r} |
759 @{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\ |
759 @{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\ |
760 @{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\ |
760 @{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\ |
1049 |
1049 |
1050 \noindent |
1050 \noindent |
1051 In these specifications @{text "name"} refers to an atom type, and @{text |
1051 In these specifications @{text "name"} refers to an atom type, and @{text |
1052 "fset"} to the type of finite sets. Note that for @{text Lam} it does not |
1052 "fset"} to the type of finite sets. Note that for @{text Lam} it does not |
1053 matter which binding mode we use. The reason is that we bind only a single |
1053 matter which binding mode we use. The reason is that we bind only a single |
1054 @{text name}. However, having \isacommand{binds (set)} or just \isacommand{binds} |
1054 @{text name}, in which case all three binding modes coincide. However, having |
|
1055 \isacommand{binds (set)} or just \isacommand{binds} |
1055 in the second case makes a difference to the semantics of the specification |
1056 in the second case makes a difference to the semantics of the specification |
1056 (which we will define in the next section). |
1057 (which we will define in the next section). |
1057 |
1058 |
1058 A \emph{deep} binder uses an auxiliary binding function that ``picks'' out |
1059 A \emph{deep} binder uses an auxiliary binding function that ``picks'' out |
1059 the atoms in one argument of the term-constructor, which can be bound in |
1060 the atoms in one argument of the term-constructor, which can be bound in |
1412 "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text |
1413 "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text |
1413 "fa\<^bsub>bn\<^esub>"} as follows: |
1414 "fa\<^bsub>bn\<^esub>"} as follows: |
1414 |
1415 |
1415 \[\mbox{ |
1416 \[\mbox{ |
1416 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1417 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1417 @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\ |
1418 @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\ |
1418 @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\ |
1419 @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\ |
1419 |
1420 |
1420 @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ |
1421 @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "\<equiv>"} & @{term "{}"}\\ |
1421 @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\ |
1422 @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "\<equiv>"} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\ |
1422 |
1423 |
1423 @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ |
1424 @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "\<equiv>"} & @{term "{}"}\\ |
1424 @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"} |
1425 @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"} |
1425 \end{tabular}} |
1426 \end{tabular}} |
1426 \]\smallskip |
1427 \]\smallskip |
1427 |
1428 |
1428 |
1429 |
1429 \noindent |
1430 \noindent |