Changeset 2526
 Timestamp:
 Dec 3, 2012, 5:48:57 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2525 r2526 674 674 satisfying requirement 1. 675 675 676 \begin{definition}[Pattern matching encoding] 677 A pattern match $match~t~with \{K_{n_j} \Rightarrow M_{n_j}\}^r_1$ that only considers a superset of the constructors listed in the polymorphic variant type 678 $i$ is encoded as 679 $match~t~with \{K_i \Rightarrow k_i \in i \to M'_i\}$ 680 where $M'_{n_j} = M_{n_j}$ for all $j \in [1,\ldots,r]$ and 681 $M'_{n_j}$ is obtained by elimination of $False$ in all other cases. 682 The proofs of $False$ required to perform the elimination are obtained from 683 the hypotheses $k_i \in i$ which contradicts the fact that $k_i$ was not 684 listed in a superset of $i$. 685 \end{definition} 686 Again, for closed types $i$, the test $k_i \in i$ can be implemented in such 687 a way that it reduces to $False$ in all cases where a proof of $False$ is 688 required. In the remaining case proof automation can be used to automatically 689 find the proofs of absurdity. 690 676 691 \subsection{Simulation (reduction + type checking)} 677 692 \subsection{Examples}
Note: See TracChangeset
for help on using the changeset viewer.