415 @{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define aggregate |
415 @{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define aggregate |
416 abstraction and representation functions using the functions @{text "ABS (\<sigma>, |
416 abstraction and representation functions using the functions @{text "ABS (\<sigma>, |
417 \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind |
417 \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind |
418 them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate |
418 them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate |
419 @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore |
419 @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore |
420 we returning just the identity whenever the types are equal. All clauses |
420 we return just the identity whenever the types are equal. All clauses |
421 are as follows: |
421 are as follows: |
422 |
422 |
423 \begin{center} |
423 \begin{center} |
424 \begin{tabular}{rcl} |
424 \begin{tabular}{rcl} |
425 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ |
425 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ |
704 behind this function is that it replaces quantifiers and |
704 behind this function is that it replaces quantifiers and |
705 abstractions involving raw types by bounded ones, and equalities |
705 abstractions involving raw types by bounded ones, and equalities |
706 involving raw types are replaced by appropriate aggregate |
706 involving raw types are replaced by appropriate aggregate |
707 relations. It is defined as follows: |
707 relations. It is defined as follows: |
708 |
708 |
709 \begin{itemize} |
709 \begin{center} |
710 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"} |
710 \begin{tabular}{rcl} |
711 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
711 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
712 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"} |
712 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |
713 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
713 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
714 \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"} |
714 \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\ |
715 \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"} |
715 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\ |
716 \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"} |
716 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
717 \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"} |
717 \multicolumn{3}{@ {\hspace{-4mm}}l}{equality (with same types and different types):}\\ |
718 \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"} |
718 @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\ |
719 \end{itemize} |
719 @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\ |
|
720 \multicolumn{3}{@ {\hspace{-4mm}}l}{application, variable, constant:}\\ |
|
721 @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\ |
|
722 @{text "REG (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\ |
|
723 @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\ |
|
724 \end{tabular} |
|
725 \end{center} |
720 |
726 |
721 In the above definition we omitted the cases for existential quantifiers |
727 In the above definition we omitted the cases for existential quantifiers |
722 and unique existential quantifiers, as they are very similar to the cases |
728 and unique existential quantifiers, as they are very similar to the cases |
723 for the universal quantifier. |
729 for the universal quantifier. |
724 |
730 |