25   been implemented as part of the Heterogeneous Tool Set. The the target logic
26   is Isabelle/HOLCF, and the translation is based on a shallow embedding
37 Automating translation from programming languages to the language of a generic
38 prover may provide useful support for the formal development and the
40 make the task of proving assertions about programs written in them easier,
41 owing to the relative simplicity of their semantics
43 to us, more specifically, from an interest in the use of functional languages
44 for the specification of reactive systems. Haskell is a strongly typed, purely
51 supporting several logics --- in particular, Isabelle/HOL is the
56 \cite{Paulson94isa,holcf} is Isabelle/HOL conservatively extended with the
64 application designed to support heterogeneous specification and the
69 modelling of the type system \cite{Huff}.
72 the semantic background of the translation, while the subsequent sections
73 are devoted to the translation of types, datatypes, classes and function
75 and Sect.~\ref{sec:conclusion} concludes the paper.
77 %Section 2 gives some background, section 3 introduces the system, section 4
78 %gives the sublanguages of Haskell that can be translated, in section 5 we
79 %define the two translations.
81 %associated with the translation to Isabelle/HOLCF, in section 7 we show how translation
84 \section{Semantic Background of the Translation}
87 We firstly describe the subset of Haskell that we cover.
96 following, for the main lines, the denotational semantics of lazy evaluation
102 Of all these limitations, the only logically deep ones are those related to
103 classes --- all the other ones are just a matter of implementation.
105 For the translation, we have followed the informal description of the
106 operational semantics given in the Haskell report \cite{HaskellRep},
107 and also consulted the complete static semantics for Haskell 98
108 \cite{journals/jfp/Faxen02}, as well as the (fragmentary) dynamic
111 become clear after a query that one of the authors has sent to the
113 Isabelle/HOLCF can be seen as the first denotational semantics given
116 \emph{defines} the denotational semantics.  Of course, an interesting
117 question is the coincidence of denotational and operational semantics.
118 However, this is beyond the scope of the paper.
122 %partiality could be obtained by lifting the type of function values with
124 %been used to translate \emph{maybe}. On the other hand, laziness appears very
125 %hard to be captured with Isabelle-HOL. It also seems hard to overcome the
127 %mentioned for the translation to Isabelle/HOLCF --- with the notable exception of
137 %gets analysed and translated, the result of a successful run being an Isabelle
138 %theory file in the target logic.
141 %Programatica, whereas the internal representation of Isabelle is based on the
142 %ML definition of the Isabelle base logic, extended in order to allow for a
145 %formed by a signature and a set of sentences, according to the theoretical
148 %essentially a morphism from theories in the internal representation of the
149 %source language to theories in the representation of the target language.
160 at the stage of definition --- in fact, a specific relation has to be
172 spared the need to discharge proof obligations at the definition
174 throughout the proofs. A standard strategy is then to define as much
179 Isabelle/HOLCF eases the translation of Haskell types and functions a
180 lot.  However, special care is needed when trying to understand the
181 Haskell semantics. If one reads the section of the Haskell report
182 dealing with types and classes, one could come to the conclusion that
183 a function space in Haskell can be mapped to the space of the
187 evaluation. This function is introduced in part 6 of the Haskell
191   However, the provision of $seq$ has important semantic consequences,
193   not the same as $\lambda x \rightarrow \bot$, since $seq$ can be
198 specific Isabelle/HOLCF theory \emph{HsHOLCF} (included in the Hets
224 the recursive translation of item $\alpha$ and the renaming according
225 to the name translation.  The translation of types is given by the
245 Built-in types are translated to the lifting of the corresponding HOL type.
247 domains. The type constructor $llist$ is discussed in the next section.
252 As explained in the Haskell report \cite{HaskellRep}, section 4.2.3,
253 the following four Haskell declarations
262 have four different semantics. Indeed, the correct translation to
272 \noindent In Isabelle/HOLCF, the keyword \emph{domain} defines a
273 (possibly recursive) domain as solution of the corresponding domain
274 equation.  The keyword \emph{lazy} ensures that the constructor $D1$
278 pcpo --- this is the semantics of Haskell \emph{newtype} definitions.
280 also introduces an isomorphic copy, the difference is that the
282 introduced implicitly by the above \emph{pcpodef} declaration is
285 values of type $N$ must be variable (which always matches), and the
287 applied to this variable whereever the corresponding value of type
289 exactly the behaviour specified for newtypes in the Haskell report.
291 Lists are translated to the domain \emph{llist}, defined as follows 
299 For each datatype, we have to lift the constructors from the
336   However, this will be fixed in Isabelle 2007; the fix currently is
337   available in the development snapshot.} Order of declarations is
339 Haskell), the keyword \emph{lazy} is omitted.
350 type class identifier (these functions are also called the
351 \emph{methods} of the class). In Isabelle, type classes are typically
352 further specified using a set of axioms; for example, the class
353 $\mathit{linorder}$ of total orders is specified using the usual total
355 Haskell. Indeed, in Haskell, there is no check that the class $Ord$
370 obligations, namely that the methods for the type at hand indeed
371 satisfy the axioms of the class. Since our translation only generates
377 to belong to class $C$ may define the behaviour of $C$'s
379 normal Isabelle constant definitions, if the type of the
380 constant (function) is specialised to $T$ in the definition.
382 described in the static semantics of Haskell \cite{journals/jfp/Faxen02}.
385 %Not all the problems have been solved with
390 classes. Therefore, the same restrictions apply to our
409 Haskell, the same concept is called ``kind''), defined by the set of
410 the classes of which it is member.  
448 \mathit{lift})$ are used to lift operators, as well as the following, defined in
458 Boolean connectives to the corresponding Isabelle/HOLCF operators.
461 restrictions, however, on case expressions, due to limitations in the
463 nested ones). On the other hand, Isabelle sensitiveness to the order of
468 $\bot$ being used as default value in the latter. Only let expressions
469 without patterns on the left are dealt with; guarded expressions are
510 application (the \emph{\$\$} operator), see Sect.~\ref{sec:types}
516 We illustrate our translation with a sample proof about the
551 However, the latter makes the Isabelle simplifier loop, and hence needs
564 Due to the recursion, this theorem cannot be fed into the simplifier either.
565 However, using substitution, it helps in proving the following
566 expected lemmas about the behaviour of $map1$:
605 also is the first denotational semantics that has been given to
609 possible out of the automation currently available in Isabelle,
612 well as with a smart syntax --- also thanks to the \emph{fixrec}
614 types have to be lifted due to the mixture of eager and lazy evaluation
615 that Haskell exhibits due to the presence of the $seq$ function.
619 The main disadvantage of our approach is the lack of type
620 constructor classes. Anyway, it is possible to get around the
623 minimises the need for interactive proofs.
640 to terms, relying on a domain-theoretic modelling of the type system
641 at the object level, allowing explicitly for a clear semantics, and
643 including type constructor classes.  In contrast, we provide in the
644 case of Isabelle/HOLCF with a translation that follows the lines of a
645 denotational semantics under the assumption that type constructors and
648 the point of view of behavioural equivalence between programs --- in
650 solution gives in general less expressiveness than the deeper approach
654 %On the other hand, the main novelty in our work is
655 %to rely on theory morphisms and on their implementation for Isabelle in the
658 % Currently Hets provides with an extension of the
661 %solution is available only for Isabelle/HOL at the moment, although in
666 Haskell programs.  Also, the lacking support of constructor classes should
669 notation, using theory morphisms as provided by the package AWE
672 Isabelle/HOLCF. These problems should be solved in the near future.
674 For monadic programs, we are also planning to use the monad-based
677 Isabelle is part of the Heterogeneous Tool Set Hets and can be
679 about the translations can be found in \cite{Tlmm}.
682 %This translation, due to the character of the P-logic
688 This work has been supported by the {\em Deutsche
690   1191/7-2 }. We thank Brian Huffmann for help with the Isabelle/HOLCF
700 to theories in Isabelle/HOL extended with AWE can be defined with the
734 Here we highlight the main differences the translation to Isabelle/HOLCF and this,
736 HOL).  Function type, product and list are used to translate the corresponding
743 analogous way as in the translation to Isabelle/HOLCF. However, partial functions and
746 In HOL one has to pay attention to the distinction between \emph{primitive
747   recursive} functions (introduced by the keyword \emph{primrec}) and
749 recursive function by the fact that recursion is based on the datatype
750 structure of one of the parameters. In contrast, termination is no trivial
752 association with the parameters. This cannot be dealt with automatically in
757 more precisely, given a set $F$ of functions: 1) all the functions in $F$ are
758 recursive in the first argument; 2) all recursive arguments in $F$ are of the
759 same type modulo variable renaming; 3) each type variable occurring in the
760 type of a function in $F$ already occurs in the type of the first argument.
762 variables which occurs on the right hand-side but not on the left hand-side of
767 $A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
768 expression $nth_n \ t$ used in the translation rule is simply an informal
769 abbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
770 extracts the $n$-th projection from a tuple no shorter than $n$.\\
922 Given the restriction to total functions, equality on built-in types can be
927 Denotational semantics con be given as basis for the translation to Isabelle/HOLCF.
928 Essentially, the claim here is that the expressions on the left hand-side of
929 the following tables represent the denotational meaning of the Haskell
930 expressions on the right hand-side, as well as of the Isabelle/HOLCF expressions to
931 which they are translated. The language on the left hand-side is still based
933 point ($\mu$) in order to represent the denotational meaning of domain
967 The representation of term denotation is similar to what we get from the
968 translation, except that for functions we give the representation of the
969 meaning of \emph{fixrec} definitions ($FIX$ is the Isabelle/HOLCF fixed point
1000 that satisfy the monadic axioms. This solution can be expressed in terms of
1003 arities, entailing the definition of maps between theorems. Theory morphisms
1005 terms, making it possible to implement parametrisation at the theory level
1007 a sub-theory $\mathit{Th}_P$ which is the parameter --- this may contain
1009 $\mathit{Th}_P$ to a theory $I$ provides the instantiation of the parameter
1010 with $I$, and makes it possible to translate the proofs made in the abstract
1011 setting of $\mathit{Th}$ to the concrete setting of $I$ --- the result being
1012 an extension of $I$.  AWE is an extension of Isabelle that can assist in the
1016 level, a hierarchy of theories culminating in \emph{Monad}, based on the
1017 declaration of a unary type constructor $M$ (in \emph{MonadType}) with the two
1019 respectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
1021 morphism from \emph{MonadAxms} to the specific theory; this involves giving
1022 specific definitions of the operators, as well as discharging proof
1024 the axioms. The following gives an example.  \\
1074 \noindent In order to build up the instantiation of \textit{LS} as a monad,
1075 here it is defined the morphism $m\_LS$ from \emph{MonadType} to the
1087 monads --- here again, note the difference with overloading. Morphism
1088 \emph{m\_LS} is then used to instantiate the parameterised theory
1093 \noindent This instantiation gives the declaration of the
1103 \emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this
1115 \noindent Now, the morphism from \emph{MonadAxms} to
1117 automatically access to the theorems proven in \emph{Monad} and, modulo
1118 renaming, the monadic syntax which is defined there. \\
1129 \noindent The \emph{Monad} theory allows for the characterisation of
1132 An approach altogether similar to the one shown for HOL could be used, in
1193 In the following, we give a definition of the sub-language of Haskell
1194 $H_c$ that is covered by the translation to Isabelle/HOLCF.\\
1282 In contrast, the following gives a definition of the Haskell sub-language
1283 $H_s$ that is covered by the translation to HOL.\\
1328   & \qquad \mbox{primitive \ recursive \ in \ the \ first \ argument, \ and \ 
1333   & \qquad \mbox{that} \ \tau_1 = \sigma_i(\tau_i) \ \mbox{and \ all \ the \ 

Indexes created Tue Jul 24 14:28:13 CEST 2018