Ignore:
Timestamp:
Dec 3, 2012, 5:48:57 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2525 r2526  
    674674satisfying requirement 1.
    675675
     676\begin{definition}[Pattern matching encoding]
     677A 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\}$
     680where $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.
     682The proofs of $False$ required to perform the elimination are obtained from
     683the hypotheses $k_i \in i$ which contradicts the fact that $k_i$ was not
     684listed in a superset of $i$.
     685\end{definition}
     686Again, for closed types $i$, the test $k_i \in i$ can be implemented in such
     687a way that it reduces to $False$ in all cases where a proof of $False$ is
     688required. In the remaining case proof automation can be used to automatically
     689find the proofs of absurdity.
     690
    676691\subsection{Simulation (reduction + type checking)}
    677692\subsection{Examples}
Note: See TracChangeset for help on using the changeset viewer.