# HG changeset patch # User Christian Urban # Date 1269976513 -7200 # Node ID 8c788ad717524eed9d7c6eb43752134cde140f84 # Parent 1cd509cba23fa181e5f20a59162d26bd28e53362 cleaned up the section about fv's diff -r 1cd509cba23f -r 8c788ad71752 Paper/Paper.thy --- a/Paper/Paper.thy Tue Mar 30 17:55:46 2010 +0200 +++ b/Paper/Paper.thy Tue Mar 30 21:15:13 2010 +0200 @@ -1091,29 +1091,32 @@ independently an alpha-equivalence relation over them. - The datatype definition can be obtained by just stripping off the + The datatype definition can be obtained by stripping off the binding clauses and the labels on the types. We also have to invent new names for the types @{text "ty\<^sup>\"} and term-constructors @{text "C\<^sup>\"} given by user. In our implementation we just use an affix @{text "_raw"}. - For the purpose of the paper we just use superscripts to indicate a - notion defined over alpha-equivalence classes and leave out the superscript - for the corresponding notion on the ``raw'' level. So for example we have - + For the purpose of the paper we just use the superscript @{text "_\<^sup>\"} to indicate + that a notion is defined over alpha-equivalence classes and leave it out + for the corresponding notion defined on the ``raw'' level. So for example + we have + \begin{center} @{text "ty\<^sup>\ \ ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\ \ C"} \end{center} \noindent + The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are non-empty and the types in the constructors only occur in positive - position (see \cite{Berghofer99} for an indepth explanation of the datatype package + position (see \cite{Berghofer99} for an indepth description of the datatype package in Isabelle/HOL). We then define the user-specified binding - functions by primitive recursion over the raw datatypes. We can also - easily define a permutation operation by primitive recursion so that for each - term constructor @{text "C ty\<^isub>1 \ ty\<^isub>n"} we have that + functions, called @{term "bn_ty"}, by primitive recursion over the corresponding + raw datatype @{text ty}. We can also easily define permutation operations by + primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \ ty\<^isub>n"} + we have that \begin{center} - @{text "p \ (C x\<^isub>1 \ x\<^isub>n) \ C (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} + @{text "p \ (C x\<^isub>1 \ x\<^isub>n) = C (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} \end{center} % TODO: we did not define permutation types @@ -1131,30 +1134,33 @@ \end{center} \noindent - We define them together with the auxiliary free variable functions for - binding functions. Given binding functions for raw types + We define them together with auxiliary free variable functions for + the binding functions. Given binding functions @{text "bn_ty\<^isub>1 \ bn_ty\<^isub>m"} we need to define - + % \begin{center} - @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \ atom set \ fv_bn_ty\<^isub>m :: ty\<^isub>m \ atom set"} + @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \ atom set \ fv_bn_ty\<^isub>m :: ty\<^isub>m \ atom set"} \end{center} \noindent - The basic idea behind these free-variable functions is to collect all atoms - that are not bound in a term constructor, but because of the rather - complicated binding mechanisms the details are somewhat involved. + The reason for this setup is that in a deep binder not all atoms have to be + bound. While the idea behind these free variable functions is just to + collect all atoms that are not bound, because of the rather complicated + binding mechanisms their definitions are somewhat involved. Given a term-constructor @{text "C"} of type @{text ty} with argument types - @{text "ty\<^isub>1 \ ty\<^isub>n"} and some binding clauses, the function + \mbox{@{text "ty\<^isub>1 \ ty\<^isub>n"}} and given some binding clauses associated with + this constructor, the function @{text "fv_ty (C x\<^isub>1 \ x\<^isub>n)"} will be the union of the values - defined below for each argument. From the binding clause of this term - constructor, we can determine whether the argument is a shallow or deep + calculated below for each argument. + + First we deal with the case @{text "x\<^isub>i"} is a binder. From the binding clauses, + we can determine whether the argument is a shallow or deep binder, and in the latter case also whether it is a recursive or - non-recursive binder. In case the argument, say @{text "x\<^isub>i"} with - type @{text "ty\<^isub>i"}, is a binder, the value is: + non-recursive binder. \begin{center} - \begin{tabular}{cp{7cm}} + \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\ $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}\\ @@ -1164,23 +1170,29 @@ \end{center} \noindent - In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of - one or more abstractions. Let @{text "bnds"} be the set of bound atoms calculated - as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}. - Otherwise there are two cases: either the - corresponding binders are all shallow or there is a single deep binder. - In the former case we build the union of all shallow binders; in the - later case we just take the set of atoms specified binding - function returns. With @{text "bnds"} computed as above the value of - for @{text "x\<^isub>i"} is given by: + The first clause states that shallow binders do not contribute to the + free variables; in the second clause, we have to look up all + the free variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this + is done with function @{text "fv_bn_ty\<^isub>i"}; in the third clause, since the + binder is recursive, we need to bind all variables specified by + @{text "bn_ty\<^isub>i"}---therefore we subtract @{text "bn_ty\<^isub>i x\<^isub>i"} from the free + variables of @{text "x\<^isub>i"}. + + In case the argument is \emph{not} a binder, we need to consider + whether the @{text "x\<^isub>i"} is the body of one or more binding clauses. + In this case we first calculate the set @{text "bnds"} as follows: + either the binders are all shallow or there is a single deep binder. + In the former case we take @{text bnds} to be the union of all shallow + binders; in the latter case, we just take the set of atoms specified by the + binding function. The value for @{text "x\<^isub>i"} is then given by: \begin{center} - \begin{tabular}{cp{7cm}} + \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ - $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes - we are defining with the free variable function @{text "fv_ty\<^isub>i"}\\ + $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes + corresponding to the types specified by the user\\ % $\bullet$ & @{text "(fv\<^isup>\ x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype % with a free variable function @{text "fv\<^isup>\"}\\ $\bullet$ & @{term "{}"} otherwise @@ -1188,28 +1200,37 @@ \end{center} \noindent - Next, for each binding function @{text "bn_ty"} we define a - free variable function @{text "fv_bn_ty"}. The basic idea behind this - function is to compute all the free atoms that are not bound by the binding - function. So given that @{text "bn"} is a binding function for type - @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the - omission of the arguments present in @{text "bn"}. + Like the function @{text atom}, @{text "atoms"} coerces a set of atoms to the generic atom type. + It is defined as @{text "atom as \ {atom a | a \ as}"}. - For a binding function clause @{text "bn (C x\<^isub>1 \ x\<^isub>n) = rhs"}, - we define @{text "fv_bn"} to be the union of the values calculated - for @{text "x\<^isub>j"} as follows: + The last case we need to consider is when @{text "x\<^isub>i"} is neither + a binder nor a body of an abstraction. In this case it is defined + as above, except that we do not subtract the set @{text bnds}. + + Next, we need to define a free variable function @{text "fv_bn_ty\<^isub>i"} for + each binding function @{text "bn_ty\<^isub>i"}. The idea behind this + function is to compute the set of free atoms that are not bound by + the binding function. Because of the restrictions we imposed on the + form of binding functions, this can be done automatically by recursively + building up the the set of free variables from the arguments that are + not bound. Let us assume one clause of the binding function is + @{text "bn_ty\<^isub>i (C x\<^isub>1 \ x\<^isub>n) = rhs"}, then @{text "fv_bn_ty\<^isub>i"} is the + union of the values calculated for @{text "x\<^isub>j"} of type @{text "ty\<^isub>j"} + as follows: \begin{center} - \begin{tabular}{cp{7cm}} - $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom, + \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} + \multicolumn{2}{l}{@{text "x\<^isub>j"} occurs in @{text "rhs"}:}\\ + $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is an atom, atom list or atom set\\ - $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} - with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ - $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\ - $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\ - $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is - one of the datatypes - we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ + $\bullet$ & @{text "fv_bn_ty\<^isub>j x\<^isub>j"} in case @{text "rhs"} contains the + recursive call @{text "bn_ty\<^isub>j x\<^isub>j"}\\[1mm] + % + \multicolumn{2}{l}{@{text "x\<^isub>j"} does not occur in @{text "rhs"}:}\\ + $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms\\ + $\bullet$ & @{term "atoms (set x\<^isub>j)"} provided @{term "x\<^isub>j"} is a list of atoms\\ + $\bullet$ & @{text "fv_ty\<^isub>j x\<^isub>j"} provided @{term "ty\<^isub>j"} is one of the raw + types corresponding to the types specified by the user\\ % $\bullet$ & @{text "fv_ty\<^isup>\ x\<^isub>j - bnds"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} % and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\"}\\ $\bullet$ & @{term "{}"} otherwise diff -r 1cd509cba23f -r 8c788ad71752 Paper/document/root.bib --- a/Paper/document/root.bib Tue Mar 30 17:55:46 2010 +0200 +++ b/Paper/document/root.bib Tue Mar 30 21:15:13 2010 +0200 @@ -2,19 +2,18 @@ author = {S.~Berghofer and M.~Wenzel}, title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in {F}ormal-{L}ogic {E}ngineering}, - booktitle = {Proc.~of the 12th International Conference Theorem Proving in - Higher Order Logics (TPHOLs)}, + booktitle = {Proc.~of the 12th TPHOLs conference}, pages = {19--36}, year = 1999, - number = 1690, + volume = 1690, series = {LNCS} } @InProceedings{CoreHaskell, author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly}, title = {{S}ystem {F} with {T}ype {E}quality {C}oercions}, - booktitle = {Proc of TLDI}, - pages = {??}, + booktitle = {Proc of the TLDI Workshop}, + pages = {53-66}, year = {2007} } @@ -83,8 +82,8 @@ @Unpublished{HuffmanUrban10, author = {B.~Huffman and C.~Urban}, title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, - note = {To appear at {\it ITP'10 Conference}}, - annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, + note = {To appear at {\it ITP'10 Conference}, + http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, year = {2010} }