336 |
336 |
337 \noindent |
337 \noindent |
338 (Note that this means also the term-constructors for variables, applications |
338 (Note that this means also the term-constructors for variables, applications |
339 and lambda are lifted to the quotient level.) This construction, of course, |
339 and lambda are lifted to the quotient level.) This construction, of course, |
340 only works if alpha-equivalence is indeed an equivalence relation, and the |
340 only works if alpha-equivalence is indeed an equivalence relation, and the |
341 lifted definitions and theorems are respectful w.r.t.~alpha-equivalence. |
341 ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence. |
342 For example, we will not be able to lift a bound-variable function. Although |
342 For example, we will not be able to lift a bound-variable function. Although |
343 this function can be defined for raw terms, it does not respect |
343 this function can be defined for raw terms, it does not respect |
344 alpha-equivalence and therefore cannot be lifted. To sum up, every lifting |
344 alpha-equivalence and therefore cannot be lifted. To sum up, every lifting |
345 of theorems to the quotient level needs proofs of some respectfulness |
345 of theorems to the quotient level needs proofs of some respectfulness |
346 properties (see \cite{Homeier05}). In the paper we show that we are able to |
346 properties (see \cite{Homeier05}). In the paper we show that we are able to |
350 The examples we have in mind where our reasoning infrastructure will be |
350 The examples we have in mind where our reasoning infrastructure will be |
351 helpful includes the term language of System @{text "F\<^isub>C"}, also |
351 helpful includes the term language of System @{text "F\<^isub>C"}, also |
352 known as Core-Haskell (see Figure~\ref{corehas}). This term language |
352 known as Core-Haskell (see Figure~\ref{corehas}). This term language |
353 involves patterns that have lists of type-, coercion- and term-variables, |
353 involves patterns that have lists of type-, coercion- and term-variables, |
354 all of which are bound in @{text "\<CASE>"}-expressions. One |
354 all of which are bound in @{text "\<CASE>"}-expressions. One |
355 difficulty is that we do not know in advance how many variables need to |
355 feature is that we do not know in advance how many variables need to |
356 be bound. Another is that each bound variable comes with a kind or type |
356 be bound. Another is that each bound variable comes with a kind or type |
357 annotation. Representing such binders with single binders and reasoning |
357 annotation. Representing such binders with single binders and reasoning |
358 about them in a theorem prover would be a major pain. \medskip |
358 about them in a theorem prover would be a major pain. \medskip |
359 |
359 |
360 \noindent |
360 \noindent |
930 (possibly empty) list of \emph{binding clauses}, which indicate the binders |
930 (possibly empty) list of \emph{binding clauses}, which indicate the binders |
931 and their scope in a term-constructor. They come in three \emph{modes}: |
931 and their scope in a term-constructor. They come in three \emph{modes}: |
932 |
932 |
933 \begin{center} |
933 \begin{center} |
934 \begin{tabular}{l} |
934 \begin{tabular}{l} |
935 \isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\ |
935 \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ |
936 \isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\ |
936 \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ |
937 \isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\ |
937 \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ |
938 \end{tabular} |
938 \end{tabular} |
939 \end{center} |
939 \end{center} |
940 |
940 |
941 \noindent |
941 \noindent |
942 The first mode is for binding lists of atoms (the order of binders matters); |
942 The first mode is for binding lists of atoms (the order of binders matters); |
943 the second is for sets of binders (the order does not matter, but the |
943 the second is for sets of binders (the order does not matter, but the |
944 cardinality does) and the last is for sets of binders (with vacuous binders |
944 cardinality does) and the last is for sets of binders (with vacuous binders |
945 preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding |
945 preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding |
946 clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will |
946 clause will be called \emph{body}; the ``\isacommand{bind}-part'' will |
947 be called the \emph{binder}. |
947 be called \emph{binder}. |
948 |
948 |
949 In addition we distinguish between \emph{shallow} and \emph{deep} |
949 In addition we distinguish between \emph{shallow} and \emph{deep} |
950 binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\; |
950 binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\; |
951 \isacommand{in}\; {\it label'} (similar for the other two modes). The |
951 \isacommand{in}\; {\it labels'} (similar for the other two modes). The |
952 restriction we impose on shallow binders is that the {\it label} must either |
952 restriction we impose on shallow binders is that the {\it labels} must either |
953 refer to a type that is an atom type or to a type that is a finite set or |
953 refer to atom types or to finite sets or |
954 list of an atom type. Two examples for the use of shallow binders are the |
954 lists of atom types. Two examples for the use of shallow binders are the |
955 specification of lambda-terms, where a single name is bound, and |
955 specification of lambda-terms, where a single name is bound, and |
956 type-schemes, where a finite set of names is bound: |
956 type-schemes, where a finite set of names is bound: |
957 |
957 |
958 \begin{center} |
958 \begin{center} |
959 \begin{tabular}{@ {}cc@ {}} |
959 \begin{tabular}{@ {}cc@ {}} |
1109 function and alpha-equivalence relation, which we are going to describe in the |
1109 function and alpha-equivalence relation, which we are going to describe in the |
1110 rest of this section. |
1110 rest of this section. |
1111 |
1111 |
1112 Having dealt with all syntax matters, the problem now is how we can turn |
1112 Having dealt with all syntax matters, the problem now is how we can turn |
1113 specifications into actual type definitions in Isabelle/HOL and then |
1113 specifications into actual type definitions in Isabelle/HOL and then |
1114 establish a reasoning infrastructure for them. Because of the problem |
1114 establish a reasoning infrastructure for them. As |
1115 Pottier and Cheney pointed out, we cannot in general re-arrange arguments of |
1115 Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general |
|
1116 re-arrange arguments of |
1116 term-constructors so that binders and their bodies are next to each other, and |
1117 term-constructors so that binders and their bodies are next to each other, and |
1117 then use the type constructors @{text "abs_set"}, @{text "abs_res"} and |
1118 then use the type constructors @{text "abs_set"}, @{text "abs_res"} and |
1118 @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first |
1119 @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first |
1119 extract datatype definitions from the specification and then define |
1120 extract datatype definitions from the specification and then define |
1120 expicitly an alpha-equivalence relation over them. |
1121 expicitly an alpha-equivalence relation over them. |