nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:06a8f782b2c1
+:c86b98642013
 %
 \noindent
 and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
 type-variables.  While it is possible to implement this kind of more general
 binders by iterating single binders, this leads to a rather clumsy
-formalisation of W. The need of iterating single binders is also one reason
+formalisation of W.
-why Nominal Isabelle
+%The need of iterating single binders is also one reason
+%why Nominal Isabelle
 % and similar theorem provers that only provide
 %mechanisms for binding single variables
-has not fared extremely well with the
+%has not fared extremely well with the
-more advanced tasks in the POPLmark challenge \cite{challenge05}, because
+%more advanced tasks in the POPLmark challenge \cite{challenge05}, because
-also there one would like to bind multiple variables at once.
+%also there one would like to bind multiple variables at once.
 Binding multiple variables has interesting properties that cannot be captured
 easily by iterating single binders. For example in the case of type-schemes we do not
 want to make a distinction about the order of the bound variables. Therefore
 we would like to regard the following two type-schemes as $\alpha$-equivalent
 %requires a lot of extra reasoning work.
 Although in informal settings a reasoning infrastructure for $\alpha$-equated
 terms is nearly always taken for granted, establishing it automatically in
 the Isabelle/HOL is a rather non-trivial task. For every
-specification we will need to construct a type containing as elements the
+specification we will need to construct type(s) containing as elements the
 $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
 a new type by identifying a non-empty subset of an existing type.  The
 construction we perform in Isabelle/HOL can be illustrated by the following picture:
 %
 \begin{center}
 We take as the starting point a definition of raw terms (defined as a
 datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in
 the type of sets of raw terms according to our $\alpha$-equivalence relation,
 and finally define the new type as these $\alpha$-equivalence classes
 (non-emptiness is satisfied whenever the raw terms are definable as datatype
-in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is
+in Isabelle/HOL and our relation for $\alpha$-equivalence is
-indeed an equivalence relation).
+an equivalence relation).
 %The fact that we obtain an isomorphism between the new type and the
 %non-empty subset shows that the new type is a faithful representation of
 %$\alpha$-equated terms. That is not the case for example for terms using the
 %locally nameless representation of binders \cite{McKinnaPollack99}: in this
 induction principles that have the variable convention already built in.
 The method behind our specification of general binders is taken
 from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
 that our specifications make sense for reasoning about $\alpha$-equated terms.
 The main improvement over Ott is that we introduce three binding modes
-(only one is present in Ott), provide definitions for $\alpha$-equivalence and
+(only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and
 for free variables of our terms, and also derive a reasoning infrastructure
-for our specifications inside Isabelle/HOL.
+for our specifications inside Isabelle/HOL from ``first principles''.
 %\begin{figure}
 %\begin{boxedminipage}{\linewidth}
 %%\begin{center}
 and the inverse permutation of @{term p} as @{text "- p"}. The permutation
 operation is defined over the type-hierarchy \cite{HuffmanUrban10};
 for example permutations acting on products, lists, sets, functions and booleans is
 given by:
 %
-\begin{equation}\label{permute}
+%\begin{equation}\label{permute}
-\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+%\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+%\begin{tabular}{@ {}l@ {}}
+%@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+%@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
+%@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+%\end{tabular} &
+%\begin{tabular}{@ {}l@ {}}
+%@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
+%@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
+%@{thm permute_bool_def[no_vars, THEN eq_reflection]}
+%\end{tabular}
+%\end{tabular}}
+%\end{equation}
+%
+\begin{center}
+\mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}
 \begin{tabular}{@ {}l@ {}}
-@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\
+@{thm permute_bool_def[no_vars, THEN eq_reflection]}
+\end{tabular} &
+\begin{tabular}{@ {}l@ {}}
 @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
 @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
 @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
 @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-@{thm permute_bool_def[no_vars, THEN eq_reflection]}
 \end{tabular}
 \end{tabular}}
-\end{equation}
+\end{center}
 \noindent
 Concrete permutations in Nominal Isabelle are built up from swappings,
 written as \mbox{@{text "(a b)"}}, which are permutations that behave
 as follows:
 @{thm (lhs) fresh_star_def[no_vars]}, defined as
 @{thm (rhs) fresh_star_def[no_vars]}.
 A striking consequence of these definitions is that we can prove
 without knowing anything about the structure of @{term x} that
 swapping two fresh atoms, say @{text a} and @{text b}, leaves
-@{text x} unchanged:
+@{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
+then @{term "(a \<rightleftharpoons> b) \<bullet> x"}.
-\begin{myproperty}\label{swapfreshfresh}
-@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+%\begin{myproperty}\label{swapfreshfresh}
-\end{myproperty}
+%@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+%\end{myproperty}
 %While often the support of an object can be relatively easily
 %described, for example for atoms, products, lists, function applications,
 %booleans and permutations as follows
 %%
 from this specification (remember that Nominal Isabelle is a definitional
 extension of Isabelle/HOL, which does not introduce any new axioms).
 In order to keep our work with deriving the reasoning infrastructure
 manageable, we will wherever possible state definitions and perform proofs
-on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
+on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code. % that
-generates them anew for each specification. To that end, we will consider
+%generates them anew for each specification.
+To that end, we will consider
 first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
 are intended to represent the abstraction, or binding, of the set of atoms @{text
 "as"} in the body @{text "x"}.
 The first question we have to answer is when two pairs @{text "(as, x)"} and
 \mbox{\it (iii)} &  @{text "(p \<bullet> x) R y"} \\
 \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"} &
 \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"} \\
 \end{array}
 \end{equation}
+%
 \noindent
 Note that this relation depends on the permutation @{text
 "p"}; $\alpha$-equivalence between two pairs is then the relation where we
 existentially quantify over this @{text "p"}. Also note that the relation is
 dependent on a free-atom function @{text "fa"} and a relation @{text
 \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
 \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* p"} &
 \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"}\\
 \end{array}
 \end{equation}
+%
 \noindent
 where @{term set} is the function that coerces a list of atoms into a set of atoms.
 Now the last clause ensures that the order of the binders matters (since @{text as}
 and @{text bs} are lists of atoms).
 \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
 \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\
 \end{array}
 \end{equation}
-It might be useful to consider first some examples about how these definitions
+It might be useful to consider first some examples how these definitions
 of $\alpha$-equivalence pan out in practice.  For this consider the case of
 abstracting a set of atoms over types (as in type-schemes). We set
 @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
 define
+%
 \begin{center}
 @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
 \end{center}
 \noindent
 \isacommand{where}~@{text "bn(PNil) = []"}\\
 \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
 \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\
 \end{tabular}}
 \end{equation}
+%
 \noindent
 In this specification the function @{text "bn"} determines which atoms of
 the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
 second-last @{text bn}-clause the function @{text "atom"} coerces a name
 into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
 allows us to treat binders of different atom type uniformly.
 As said above, for deep binders we allow binding clauses such as
 %
-\begin{center}
+%\begin{center}
-\begin{tabular}{ll}
+%\begin{tabular}{ll}
-@{text "Bar p::pat t::trm"} &
+@{text "Bar p::pat t::trm"} %%%&
-\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
+\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} %%\\
-\end{tabular}
+%\end{tabular}
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 where the argument of the deep binder also occurs in the body. We call such
 binders \emph{recursive}.  To see the purpose of such recursive binders,
 compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
 specification:
 %
 \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
 \isacommand{where}~@{text "bn(ANil) = []"}\\
 \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
 \end{tabular}}
 \end{equation}
+%
 \noindent
 The difference is that with @{text Let} we only want to bind the atoms @{text
 "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
 inside the assignment. This difference has consequences for the associated
 notions of free-atoms and $\alpha$-equivalence.
 To make sure that atoms bound by deep binders cannot be free at the
 same time, we cannot have more than one binding function for a deep binder.
 Consequently we exclude specifications such as
+%
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
 \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
 @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
 either refer to labels of atom types (in case of shallow binders) or to binding
 functions taking a single label as argument (in case of deep binders). Assuming
 @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the
 set of binding atoms in the binders and @{text "B'"} for the set of free atoms in
 non-recursive deep binders,
-then the free atoms of the binding clause @{text bc\<^isub>i} are
+then the free atoms of the binding clause @{text bc\<^isub>i} are\\[-2mm]
 %
 \begin{equation}\label{fadef}
 \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
 \end{equation}
+%
 \noindent
 The set @{text D} is formally defined as
 %
-\begin{center}
+%\begin{center}
 @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
 where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
 specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
 we are defining by recursion;
 %(see \eqref{fvars});
 otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
 In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
-for atom types to which shallow binders may refer
+for atom types to which shallow binders may refer\\[-4mm]
 %
 %\begin{center}
 %\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 %@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
 %@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
 %@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
 %\end{tabular}
 %\end{center}
 %
 \begin{center}
-@{text "bn_atom a \<equiv> {atom a}"}\hspace{17mm}
+@{text "bn\<^bsub>atom\<^esub> a \<equiv> {atom a}"}\hfill
-@{text "bn_atom_set as \<equiv> atoms as"}\\
+@{text "bn\<^bsub>atom_set\<^esub> as \<equiv> atoms as"}\hfill
-@{text "bn_atom_list as \<equiv> atoms (set as)"}
+@{text "bn\<^bsub>atom_list\<^esub> as \<equiv> atoms (set as)"}
 \end{center}
+%
 \noindent
 Like the function @{text atom}, the function @{text "atoms"} coerces
 a set of atoms to a set of the generic atom type.
 %It is defined as  @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
-The set @{text B} is then formally defined as
+The set @{text B} is then formally defined as\\[-4mm]
 %
 \begin{center}
 @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
 \end{center}
+%
 \noindent
 where we use the auxiliary binding functions for shallow binders.
 The set @{text "B'"} collects all free atoms in non-recursive deep
 binders. Let us assume these binders in @{text "bc\<^isub>i"} are
 %
 %\end{center}
 %
 %\noindent
 with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the
 @{text "l"}$_{1..r}$ being among the bodies @{text
-"d"}$_{1..q}$. The set @{text "B'"} is defined as
+"d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm]
 %
 \begin{center}
-@{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
+@{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}\\[-9mm]
 \end{center}
+%
 \noindent
 This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
 Note that for non-recursive deep binders, we have to add in \eqref{fadef}
 the set of atoms that are left unbound by the binding functions @{text
 \noindent
 Recall that @{text ANil} and @{text "ACons"} have no
 binding clause in the specification. The corresponding free-atom
 function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
-occurring in an assignment (in case of @{text "ACons"}, they are given in
+of an assignment (in case of @{text "ACons"}, they are given in
 terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}).
 The binding only takes place in @{text Let} and
 @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
 that all atoms given by @{text "set (bn as)"} have to be bound in @{text
 t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
 permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
 by lifting. Assuming a
 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define
 %
 \begin{center}
-@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}
+@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} \;\; with
-\end{center}
+$\begin{cases}
-%
+\text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\
-\noindent
+\text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\
-with @{text "y\<^isub>i"} determined as follows:
+\text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}
-%
+\end{cases}$
-\begin{center}
+\end{center}
-\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
+%
-$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+%\noindent
-$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+%with @{text "y\<^isub>i"} determined as follows:
-$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+%
-\end{tabular}
+%\begin{center}
-\end{center}
+%\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
-%
+%$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+%$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+%$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+%\end{tabular}
+%\end{center}
+%
+\noindent
 Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
 @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
 is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But
 these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
 completes the interesting cases in \eqref{letpat} for strengthening the induction
 order of binders should matter, or vacuous binders should be taken into
 account). %To do so, one would require additional predicates that filter out
 %unwanted terms. Our guess is that such predicates result in rather
 %intricate formal reasoning.
-Another representation technique for binding is higher-order abstract syntax
+Another technique for representing binding is higher-order abstract syntax
-(HOAS), which for example is implemented in the Twelf system. This representation
+(HOAS). %, which for example is implemented in the Twelf system.
+This %%representation
 technique supports very elegantly many aspects of \emph{single} binding, and
 impressive work has been done that uses HOAS for mechanising the metatheory
 of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
 binders of SML are represented in this work. Judging from the submitted
 Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
-binding constructs where the number of bound variables is not fixed. For
+binding constructs where the number of bound variables is not fixed. %For
-example in the second part of this challenge, @{text "Let"}s involve
+example
+In the second part of this challenge, @{text "Let"}s involve
 patterns that bind multiple variables at once. In such situations, HOAS
-representations have to resort to the iterated-single-binders-approach with
+seems to have to resort to the iterated-single-binders-approach with
 all the unwanted consequences when reasoning about the resulting terms.
 %Two formalisations involving general binders have been
 %performed in older
 %versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
 rather different from ours, not using any nominal techniques.  To our
 knowledge there is also no concrete mathematical result concerning this
 notion of $\alpha$-equivalence.  A definition for the notion of free variables
 is work in progress in Ott.
-Although we were heavily inspired by the syntax in Ott,
+Although we were heavily inspired by the syntax of Ott,
 its definition of $\alpha$-equivalence is unsuitable for our extension of
 Nominal Isabelle. First, it is far too complicated to be a basis for
 automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
 covers cases of binders depending on other binders, which just do not make
 sense for our $\alpha$-equated terms. Third, it allows empty types that have no
 $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.
 The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
 has a more operational flavour and calculates a partial (renaming) map.
 In this way, the definition can deal with vacuous binders. However, to our
 best knowledge, no concrete mathematical result concerning this
-definition of $\alpha$-equivalence has been proved.
+definition of $\alpha$-equivalence has been proved.\\[-7mm]
 *}
 section {* Conclusion *}
 text {*
 We have left out a discussion about how functions can be defined over
 $\alpha$-equated terms involving general binders. In earlier versions of Nominal
 Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We
 hope to do better this time by using the function package that has recently
 been implemented in Isabelle/HOL and also by restricting function
-definitions to equivariant functions (for such functions it is possible to
+definitions to equivariant functions (for such functions we can
 provide more automation).
 %There are some restrictions we imposed in this paper that we would like to lift in
 %future work. One is the exclusion of nested datatype definitions. Nested
 %datatype definitions allow one to specify, for instance, the function kinds
 %We have also not yet played with other binding modes. For example we can
 %imagine that there is need for a binding mode
 %where instead of lists, we abstract lists of distinct elements.
 %Once we feel confident about such binding modes, our implementation
 %can be easily extended to accommodate them.
+%
-\medskip
+\smallskip
 \noindent
 {\bf Acknowledgements:} %We are very grateful to Andrew Pitts for
 %many discussions about Nominal Isabelle.
 We thank Peter Sewell for
 making the informal notes \cite{SewellBestiary} available to us and
 also for patiently explaining some of the finer points of the work on the Ott-tool.
 %Stephanie Weirich suggested to separate the subgrammars
-%of kinds and types in our Core-Haskell example.
+%of kinds and types in our Core-Haskell example. \\[-6mm]
 *}
 (*<*)
 end

changeset 2516	c86b98642013
parent 2515	06a8f782b2c1
child 2517	e1093e680bcf