471 |
471 |
472 section {* Equivariance *} |
472 section {* Equivariance *} |
473 |
473 |
474 text {* |
474 text {* |
475 An important notion in the nominal logic work is |
475 An important notion in the nominal logic work is |
476 \emph{equivariance}. To give a definition for this notion, let us |
476 \emph{equivariance}. In order to prove properties about this notion, |
477 define \emph{HOL-terms}. They are given by the grammar |
477 let us first define \emph{HOL-terms}. They are given |
|
478 by the grammar |
478 |
479 |
479 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
480 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
480 @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"} |
481 @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"} |
481 \hfill\numbered{holterms} |
482 \hfill\numbered{holterms} |
482 \end{isabelle} |
483 \end{isabelle} |
483 |
484 |
484 \noindent |
485 \noindent |
485 whereby @{text c} stands for constants and @{text x} for |
486 whereby @{text c} stands for constant symbols, or short constants, and |
486 variables. We assume HOL-terms are fully typed, but for the sake of |
487 @{text x} for variables. We assume HOL-terms are fully typed, but for the |
487 greater legibility we leave the typing information implicit. We |
488 sake of greater legibility we leave the typing information implicit. We |
488 also assume the usual notions for free and bound variables of a |
489 also assume the usual notions for free and bound variables of a HOL-term. |
489 HOL-term. |
|
490 |
490 |
491 An equivariant HOL-term is one that is invariant under the |
491 An equivariant HOL-term is one that is invariant under the |
492 permutation operation. This notion can be defined as follows: |
492 permutation operation. This notion can be defined in Isabelle/HOL |
|
493 as follows: |
493 |
494 |
494 \begin{definition}[Equivariance]\label{equivariance} |
495 \begin{definition}[Equivariance]\label{equivariance} |
495 A HOL-term @{text t} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> t = t"}. |
496 A HOL-term @{text t} with permutation type is \emph{equivariant} provided |
|
497 @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}. |
496 \end{definition} |
498 \end{definition} |
497 |
499 |
498 \noindent |
500 \noindent |
499 There are a number of equivalent formulations for the equivariance |
501 There are a number of equivalent formulations for the equivariance |
500 property. For example, assuming @{text t} is of type @{text "\<alpha> \<Rightarrow> |
502 property. For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow> |
501 \<beta>"}, then equivariance can also be stated as |
503 \<beta>"}, then equivariance can also be stated as |
502 |
504 |
503 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
505 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
504 \begin{tabular}{@ {}l} |
506 \begin{tabular}{@ {}l} |
505 @{text "\<forall>\<pi> x. \<pi> \<bullet> (t x) = t (\<pi> \<bullet> x)"} |
507 @{text "\<forall>\<pi> x. \<pi> \<bullet> (t x) = t (\<pi> \<bullet> x)"} |
526 \end{tabular} |
528 \end{tabular} |
527 \end{isabelle} |
529 \end{isabelle} |
528 |
530 |
529 \noindent |
531 \noindent |
530 using the permutation operation on booleans and property |
532 using the permutation operation on booleans and property |
531 \eqref{permuteequ}. Lemma~\ref{permutecompose} establishes that the |
533 \eqref{permuteequ}. |
|
534 Lemma~\ref{permutecompose} establishes that the |
532 permutation operation is equivariant. The permutation operation for |
535 permutation operation is equivariant. The permutation operation for |
533 lists and products, shown in \eqref{permdefs}, state that the |
536 lists and products, shown in \eqref{permdefs}, state that the |
534 constructors for products, @{text "Nil"} and @{text Cons} are |
537 constructors for products, @{text "Nil"} and @{text Cons} are |
535 equivariant. Furthermore a simple calculation will show that our |
538 equivariant. Furthermore a simple calculation will show that our |
536 swapping functions are equivariant, that is |
539 swapping functions are equivariant, that is |
544 \noindent |
547 \noindent |
545 for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans |
548 for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans |
546 @{const True} and @{const False} are equivariant by the definition |
549 @{const True} and @{const False} are equivariant by the definition |
547 of the permutation operation for booleans. It is also easy to see |
550 of the permutation operation for booleans. It is also easy to see |
548 that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text |
551 that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text |
549 "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. |
552 "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro) |
550 |
553 |
551 In contrast, the advantage of Definition \ref{equivariance} is that |
554 In contrast, the advantage of Definition \ref{equivariance} is that |
552 it leads to a simple rewrite system. Consider the following oriented |
555 it leads to a simple rewrite system. Consider the following oriented |
553 versions |
556 versions |
554 |
557 |