equal
deleted
inserted
replaced
357 properties (see \cite{Homeier05}). In the paper we show that we are able to |
357 properties (see \cite{Homeier05}). In the paper we show that we are able to |
358 automate these proofs and as a result can automatically establish a reasoning |
358 automate these proofs and as a result can automatically establish a reasoning |
359 infrastructure for alpha-equated terms.\smallskip |
359 infrastructure for alpha-equated terms.\smallskip |
360 |
360 |
361 The examples we have in mind where our reasoning infrastructure will be |
361 The examples we have in mind where our reasoning infrastructure will be |
362 helpful includes the term language of Core-Haskell (see |
362 helpful include the term language of Core-Haskell (see |
363 Figure~\ref{corehas}). This term language involves patterns that have lists |
363 Figure~\ref{corehas}). This term language involves patterns that have lists |
364 of type-, coercion- and term-variables, all of which are bound in @{text |
364 of type-, coercion- and term-variables, all of which are bound in @{text |
365 "\<CASE>"}-expressions. In these patterns we do not know in advance how many |
365 "\<CASE>"}-expressions. In these patterns we do not know in advance how many |
366 variables need to be bound. Another example is the algorithm W, |
366 variables need to be bound. Another example is the algorithm W, |
367 which includes multiple binders in type-schemes.\medskip |
367 which includes multiple binders in type-schemes.\medskip |
569 @{text "f x"} can be moved to the argument @{text x}. That means for equivariant |
569 @{text "f x"} can be moved to the argument @{text x}. That means for equivariant |
570 functions @{text f}, we have for all permutations @{text "\<pi>"}: |
570 functions @{text f}, we have for all permutations @{text "\<pi>"}: |
571 |
571 |
572 \begin{equation}\label{equivariance} |
572 \begin{equation}\label{equivariance} |
573 @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\; |
573 @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\; |
574 @{text "\<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"} |
574 @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"} |
575 \end{equation}\smallskip |
575 \end{equation}\smallskip |
576 |
576 |
577 \noindent |
577 \noindent |
578 From property \eqref{equivariancedef} and the definition of @{text supp}, we |
578 From property \eqref{equivariancedef} and the definition of @{text supp}, we |
579 can easily deduce that equivariant functions have empty support. There is |
579 can easily deduce that equivariant functions have empty support. There is |