hs2isa.tex revision 56f499bbc75665b431ab11e7f9f3fb05f2607c52
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski% Author: Paolo Torrini <paolot@helios.dai.ed.ac.uk>
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski% Created: Mon Feb 15 1999
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{llncs}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\documentclass{/home/polh/Documents/Hs2Isa/llcns}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%%\documentstyle{/home/polh/Documents/Hs2Isa/llcns}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%%\documentclass[a4paper,12pt]{article}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage[dvips]{graphics}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{amsfonts}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{amssymb}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%\usepackage{psfig}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{fancybox}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{epsfig}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{graphicx}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{color}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\usepackage{semrot}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\input{newmacros}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% Use \includegraphics{*.eps} for pictures
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{document}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\title{Translating Haskell into Isabelle}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\author{Paolo Torrini, Till Mossakowski, Christian Maeder}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\institute {Informatik, Universitaet Bremen}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\abstract{\scriptsize \bf We have defined and implemented as functions
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski of Hets two partial translations of Haskell into Isabelle
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski higher-order logics. Hets is a Haskell-based proof-management and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski program development system that allows for integration with other
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski verification tools. Our application can translate simple Haskell
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski programs to HOLCF and, under stronger restrictions, to HOL. Both
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski translations use the static analysis of Programatica, are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski based on shallow embedding and rely on denotational semantics.}\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% The translation of monads uses the AWE extension of Isabelle.}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTranslations between programming and specification languages, as well
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias the corresponding integration of compilers, analyzers and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheorem-provers, can provide useful support to the formal development
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand verification of programs. Verifying a program involves a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiformulation of the requirements in a logic, a translattion of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprogram to the logic, and a proof of the correctness statement. The
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslation must rest on a formal semantics of the programming
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilanguage given in the logic. It should allow for representations of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprograms that make proofs as easy as possible. And, not the least on
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiaccount of safety, it should be carried out automatically. It has long
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibeen argued that functional languages, based on notions closer to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigeneral, mathematical ones, can make the task of proving assertions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiabout them easier, owing to the clarity and relative simplicity of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheir semantics \cite{Thompson92}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn the following we present automated translations of Haskell programs
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinto Isabelle higher-order logic based on a denotational semantics.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell is a strongly typed, purely functional language with lazy
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskievaluation, polymorphic types extended with type constructor classes,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand a syntax for side effects and pseudo-imperative code based on
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimonadic operators \cite{HaskellRep}. The translations are implemented
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias functions of Hets \cite{Hets}, an Haskell-based application
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidesigned to support heterogeneous specification and formal development
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof programs. Hets supplies with parsing, static analysis, proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimanagement and interface to various language-specific tools. Hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelies for interactive proofs on an interface with Isabelle, a generic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheorem-prover written in SML that includes the formalization of many
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogics \cite{Paulson94isa}. Hets uses Programatica \cite{Prog04} for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe parsing and the static analysis of Haskell programs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiProgramatica, a Haskell-specific formal development system built at
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOGI, has a proof management on its own that includes a specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic and translations to different proof tools, notably to Isabelle
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Huff}, albeit following a different approach from ours (see
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisection~\ref{sec:Translations}).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Isabelle}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIsabelle-HOL (hereafter simply HOL) is the implementation in Isabelle
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof classical higher-order logic based on simply typed lambda calculus
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand extended with axiomatic type classes. It provides considerable
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisupport for reasoning about programming functions, both in terms of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirich libraries and efficient automation. Since the late nineties, it
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskihas essentially superseded FOL (classical first-order logic) as an
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIsabelle standard. HOL has an implementation of recursive functions
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckebased on Knaster-Tarski fixed-point theorem. All functions are total;
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckepartiality may be dealt with by lifting types through the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\emph{option} type constructor.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHOLCF \cite{holcf} is HOL conservatively extended with the logic of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicomputable functions --- a formalization of domain theory. In HOL,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitypes --- elements of class \emph{type} --- are just sets; functions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimay not be computable, and a recursive function may require
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidischarging proof obligations already at the definition stage --- in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifact, a specific measure has to be given for the function to be proved
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimonotonic. In contrast, domain theory has each type interpreted as an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskielement of class \emph{pcpo} (pointed complete partially ordered sets)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskii.e. as a set with a partial order which is closed w.r.t.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$\omega$-chains and has a bottom. All functions defined over domains,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiincluding partial ones, are continuous, therefore computable.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiRecursion can be expressed in terms of least fixed-point operator, and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiso, in contrast with HOL, function definition never depends on proofs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe Isabelle formalization of HOLCF is based on axiomatic type classes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Wenzel} so to deal with complete partial orders in a totally
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiabstract way. Domain theory offers a good basis for the semantical
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis of programming languages; nevertheless, it may make proofs
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskicomparatively hard. After being spared the need to discharge proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiobligations at the defining stage, one has to bear with assumptions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiover the continuity of functions while proving theorems. A standard
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistrategy to get the best out of the two systems is to define as much
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias possible in HOL, using HOLCF type constructors to lift types only
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhen this is needed.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Translations}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:Translations}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTranslations depend first of all on the expressiveness of the target
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowskilogic. Those into FOL based on large-step operational semantics of
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMiranda \cite{Thompson95,Thompson89,Thompson95b} and Haskell
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Thompson92} struggle with higher-order features such as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicurrying. The Haskell translation to the Agda implementation of
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMartin-Loef type theory in \cite{Abel} struggles with Haskell
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederpolymorphism. Higher-order logic helps overcome such obstacles. It
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maederalso allows for higher-level approaches based on denotational
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedersemantics, such as proposed in \cite{Huff} to translate Haskell to
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederHOLCF and in \cite{Pollack} to translate ML to HOL. Denotational
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskisemantics makes it possible to give representations of programs that
464c78620a182d2e8fbd125098045eae8788e2bdTill Mossakowskiare closer to their specification as well as to give proofs that are
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowskirelatively more abstract and general.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA shallow embedding into a logical language is one that relies quite
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiradically on its extra-logical features, possibly taking advantage of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibuilt-in packages provided with the implementation of that language,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiparticularly with respect to features such as types, classes, and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirecursion. On the contrary, a deep embedding relies on the logical
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidefinition of all the relevant notions. This may give a plus in
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskisemantic clarity and, if the logic is expressive enough, in generality
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskias well. Taking advantage of built-in features, on the other hand, may
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskihelp rely on standard proof methods to make theorem proving less
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe translation of ML in \cite{Pollack} based on the definition of a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiclass of types with bottom elements in HOL gives an example of the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskideep sort. The translation of Haskell to HOLCF proposed in \cite{Huff}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskirelies on a generic formalization of domain theory and particularly on
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithe \emph{fixrec} package for recursive functions, created to provide
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskia friendly syntax covering mutually recursive definitions as well. In
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiorder to capture type constructor classes --- an important feature of
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithe Haskell type system --- a deep embedding approach is used there as
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiwell. Haskell types are translated to terms, relying on a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskidomain-theoretic modelling of the type system at the object level. The
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskipractical drawback of this approach is that plenty of the automation
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckebuilt into Isabelle type checking either needs to be reimplemented or
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe translations of Haskell to HOLCF and HOL that we are presenting
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskihere are based on denotational semantics and on a shallow embedding
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiapproach. The translation to HOLCF relies on the \emph{fixrec}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskipackage. In contrast with \cite{Huff}, we rely on the similarity
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskibetween type systems, translating Haskell types to HOLCF types, in a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicomparatively direct way, and Haskell classes to Isabelle axiomatic
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiclasses. The modelling we are relying on is a simplified one, and we
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiexpect operational equivalence between Haskell programs and their
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskitranslation to HOLCF up to the level of typeable output. The
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskitranslation covers a significant part of the Prelude syntax, although
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiit is still incomplete in one important respect --- it does not
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiinclude type constructor classes; we have plans for an extention that
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskishould address this aspect.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiConceptually, type classes in Isabelle are quite different from those
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiin Haskell. Where the former ones are associated with sets of axioms,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithe latter ones come with sets of function declarations. Moreover,
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiIsabelle classes may have at most a single type parameter. Most
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiimportantly, Isabelle does not allow for type constructor classes. The
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilast limitation is serious, since it makes hard to cope with essential
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHaskell features such as monads and the \emph{do} notation. In
30256573a343132354b122097b0ee1215dda1364Till Mossakowskialternative to the method proposed in \cite{Huff}, we would like to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiget around the obstacle by relying on an extension of Isabelle based
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederon theory morphism (see section~ \ref{sec:Monads}). The AWE system
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\cite{AWE} is in fact an implementation of such an extension.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe translation to HOL, similar in respect of shallow approach,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinevertheless is much more limited. An important restriction has to do
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwith recursion --- only primitive recursive functions are covered.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis limitation appears relatively hard to overcome, given the way
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisyntax for full recursion is defined for HOL. Moreover, we have to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskirestrict to total functions. Operational equivalence for a larger
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifragment could be obtained using option types, but it is not pursued
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Haskell2Isabelle}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe Hets function \emph{Haskell2Isabelle} supports the translation of
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisimple Haskell programs to HOLCF and, with more restriction, to HOL.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiNot all the syntactical features used in the Prelude and main
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilibraries are covered. Some of the most noticeable limitations are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithose related to built-in types, pattern-matching, local definitions,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimport and export. There are additional and more substantial
30256573a343132354b122097b0ee1215dda1364Till Mossakowskirestrictions in the case of HOL, related to termination and recursion.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiEach of the translations relies on a \emph{base theory}. These are
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle theory files, respectively \emph{HsHOLCF}, extending HOLCF,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand \emph{HsHOL}, extending HOL, which are included in the Hets
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskidistribution. Each of them provides definitions and axiomatizations of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskinotions that are used in the corresponding translation --- notably
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiInformation for the use of Hets may be found in \cite{HetsUG} and a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigeneral outlook in \cite{HetsUG}. The Haskell-to-Isabelle translation
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirequires essentially GHC, Isabelle 2006 and Programatica --- with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirespect to the latter, both analysis and translation functions in Hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimake use of its modules. The command to run the application is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{hets -v[1--5] -t Haskell2Isabelle[HOLCF | HOL] -o thy filename}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent where options set verbosity, target logic and name of the
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskioutput file. The input file (last argument) must be a GHC source
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(\emph{hs} extension). The Haskell program gets analyzed and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitranslated. The result of a successful execution is an Isabelle theory
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifile (\emph{thy} extension) depending on the corresponding base
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%The application requires essentially Haskell GHC and Programatica. It
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%is run by the command \emph{hets -t ... [h|hc] file.hs} where the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%options stand for HOL and HOLCF, respectively.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe internal representation of Haskell in Hets (module
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\emph{Logic\_Haskell} and particularly \emph{HatAna}) is essentially
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe same as in Programatica, whereas the internal representation of
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIsabelle (module \emph{Logic\_Isabelle} and particularly
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\emph{IsaSign}) is a Haskell reworking of the ML definition of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIsabelle own base logic, extended in order to allow for a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistraightforward representation of HOL and HOLCF.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHaskell programs as well as Isabelle theories are internally
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirepresented as Hets theories --- each of them a data-structures formed
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiby a signature and a set of sentences, fitting a theoretical framework
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidescribed in \cite{MossaTh}. Each translation, defined as composition
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof the signature translation with the translation of all sentences,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskihas the structure of a morphism from theories in the internal
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirepresentation of the source language to those in the representation
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowskiof the target language. The distribution module
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder\emph{Haskell2IsabelleHOLCF} contains the main function, dependent on
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederthe target logic. The module \emph{IsaPrint} provides the essential
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederfunctions for the pretty-printing of Isabelle theories.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederThe following gives a list of reserved names, i.e. the names that are
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiused in order to either rename or name automatically variables and
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederconstants in the translations. 1) Type variables, in the translation
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederto HOL: \emph{'vX}; any name terminating with \emph{'XXn} where $n$ is
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederan integer. 2) Term variables, in both translations: \emph{pXn},
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\emph{qXn}, with $n$ integer. 3) Constants, in the translation to HOL:
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederstrings obtained by joining together names of defined functions, using
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\emph{\_X} as end sequence and separator.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Correspondingly, the translation function is defined as the
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%composition of signature translation with the translation of all
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%structure of a morphism from Hets theories written in the language of
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%the source internal representation to those in the language
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%representation of the target language. Internally, the information
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%about types is collected into a signature, whereas datatype
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%declarations and definitions are associated with sentences.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% module that contains the main translation function, carried out as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% composition of a signature morphism and a theory morphism.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \emph{IsaSign.hs} contains the Hets representation of the Isabelle
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% base logic and extensions.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% The general design of the translation functions, and particularly
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% the two-layered recursion adopted for them, is similar to that used
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% for the translation Haskell to Agda in Programatica.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection{HOLCF: Type signature}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe translation to HOLCF keeps into account partiality, i.e. the fact
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthat a function might be undefined for certain values, either because
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidefinition is missing, or because the program does not terminate. It
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskialso keeps into account laziness, i. e. the fact that by default
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskifunction values in Haskell are passed by name and evaluated only when
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskineeded. Essentially, we are following the main lines of the ``crude''
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidenotational semantics for lazy evaluation in \cite{winskel}, pp.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski216--217. Raising an exception is different from running forever, and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiboth are different from stopping short of evaluation. However, from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe point of view of the printable output, these behaviours are
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisimilar and can be treated semantically as such, i.e. using one and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe same bottom element.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% In order to ease the translation of some notions, the Isabelle
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% theory \emph{HsHOLCF.thy}, that extends HOLCF has been defined and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski% included in the Hets distribution.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski% It is often convenient to define in Isabelle notions that match the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder% translation of some itmes.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% Haskell datatype and function declarations are translated to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder% declarations in HOLCF. Names are translated by a function that
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% preserves them, up to avoidance of clashes with HOLCF keywords.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiEach type in Isabelle has a sort, defined by the set of the classes of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwhich it is member. Haskell type variables are translated to HOLCF
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederones, of class \emph{pcpo}. Each built-in type is translated to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilifting of its corresponding HOL type. Properly covered are Haskell
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskibooleans and unbounded integers, associated respectively to HOL
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskibooleans and integers.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Rationals need to be
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%imported in order to be used in Haskell, so they are not covered by
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%the translation at the present stage (import has not been dealt with
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%and rationals.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiBound integers and floating point numbers would need low-level
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermodelling, and have not been covered. Bounded integers in particular
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederare simply treated as unbounded in the translation. The HOLCF type
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiconstructor \emph{lift} is used to lift HOL types to flat domains. In
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe case of booleans, we can use type \emph{tr}, defined as equal to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski$bool \ lift$ in HOLCF. In the case of integers, we use \emph{dInt},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskidefined in \emph{HsHOLCF} to equal $int \ lift$. The types of Haskell
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifunctions and product are translated, respectively, to HOLCF function
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispaces and lazy product --- i.e. such that $\bot = (\bot * \bot) \neq
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(\bot*'a) \neq ('a * \bot)$, consistently with lazy evaluation. Type
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichconstructors are translated to corresponding HOLCF ones (noticeably,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiparameters precede type constructors in Isabelle syntax). In
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederparticular, lists are translated to the domain \emph{llist} defined in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\emph{HsHOLCF}. Function declarations are translated to HOLCF ones
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(keyword \emph{consts}). Names (for types as well as for terms) are
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitranslated by a function ($t$ here) that preserves them, up to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiavoidance of clashes with HOLCF keywords. Translation of types (minus
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermutual recursion) may be summed up as follows:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% Haskell datatype and function declarations are translated to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% declarations in HOLCF.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$$\begin{array}{lcl}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \lceil a \rceil & = & 'a_{t}::pcpo \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \lceil Bool \rceil & = & tr \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \lceil Integer \rceil & = & dInt \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \lceil a \to b \rceil & = & \lceil a \rceil \to \lceil b \rceil \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \lceil [a] \rceil & = & \lceil a \rceil \ llist \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\noindent In HOL, datatype declarations define types of class
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\emph{type} by keyword \emph{datatype}; in contrast, in HOLCF, they
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdefine types of class \emph{pcpo} (i.e. domains) by keyword
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\emph{domain} (so we also may call them \emph{domain declarations}).
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiEach recursive datatype declaration in Haskell is translated to the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcorresponding one in HOLCF. The translation of mutually recursive
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskidatatypes relies on specific Isabelle syntax (keyword
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich\emph{and}), as in the next example.\\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski$data \ AType \ a \ b \ = \ ABase \ a \ | \ AStep \ (AType \ a \ b) \ (BType \ a \ b) $
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$data \ BType \ a \ b \ = \ BBase \ b \ | \ BStep \ (BType \ a \ b) \ (AType \ a \ b) $\\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\noindent This translates to HOLCF as the following.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski$$\begin{array}{rr} domain & \ ('a::pcpo, 'b::pcpo) \ BType \ = \ BBase \ (BBase\_1::'b) \ | \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski & BStep \ (BStep\_1::('a, 'b) \ BType) \ (BStep\_2::('a, 'b) \ AType) \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski and & \ ('a::pcpo, 'b::pcpo) \ AType \ = \ ABase \ (ABase\_1::'a) \ | \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski & AStep \ (AStep\_1::('a, 'b) \ AType) \ (AStep\_2::('a, 'b) \ BType) \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\noindent Notably, domain declarations require an explicit
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiintroduction of destructors. Both translations (to HOL as well as to
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill MossakowskiHOLCF) take care automatically of the order of datatype declarations
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski--- this is needed, insofar as, differently from Haskell, Isabelle
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirequires them to be listed according to their order of dependency.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{HOLCF: Sentences}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederEach Haskell function definition is translated to a corresponding one.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNon-recursive definitions are translated to standard ones (keyword
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\emph{defs}), whereas the translation of recursive definitions relies
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskion the \emph{fixrec} package. Lambda abstraction is translated as
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicontinuous abstraction (\emph{LAM}), and function application as
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicontinuous application (the \emph{dot} operator) --- these notions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicoincide with the corresponding, HOL-defined ones, whenever their
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiarguments are continuous.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% As to the translation of terms containing either values or operators
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% of built-in type, it is often the case that we translate them to
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% lifted HOL operators. The lifting function is \emph{Def}; $\bot$ is
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% used for the undefined case.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiTerms of built-in type (boolean and integers) are translated to lifted
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHOL values, using the HOLCF-defined lifting function \emph{Def}. The
30256573a343132354b122097b0ee1215dda1364Till Mossakowskibottom element $\bot$ is used for all undefined terms. The following
30256573a343132354b122097b0ee1215dda1364Till Mossakowskioperator, defined in \emph{HsHOLCF}, is used to map binary arithmetic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifunctions to lifted functions over
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilifted integers.\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \Rightarrow ('a \ lift \to \ 'b \ lift \to \ 'c \ lift) $
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$fliftbin \ f \ == \ LAM \ y x. \ (flift1 \ (\%u. \ flift2 \ (\%v. \ f \ v \ u))) \cdot x \ \cdot y $\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\noindent Booleans are translated to values of \emph{tr} ---
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\emph{TT}, \emph{FF} and $\bot$, and boolean connectives are
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitranslated to the corresponding HOLCF-defined lifted operators.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHOLCF-defined \emph{If then else fi} and \emph{case} syntax are used
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederto translate, respectively, conditional and case expressions. There
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiare some restrictions, however, on the latters, due to limitations in
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe translation of patterns (see section~\ref{sec:Patterns}); in
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederparticular, the case term should always be a variable, and no nested
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederpatterns are allowed.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederThe translation of lists and list constructors relies on the
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederfollowing \emph{HsHOLCF}-defined datatype.\\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder$domain \ 'a\ llist \ = \ lNil \ | \ lCons \ (lazy \ lHd ::'a) \ (lazy \ lTl ::'a \ llist) $\\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\noindent Under the given interpretation, a stream as well as an
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederundefined list function take value $\bot$. This may be regarded as a
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedersemantical weakness.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHaskell allows for local definitions by means of \emph{let} and
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\emph{where} expressions. The \emph{let} expressions where the
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederleft-hand side is a variable are translated to similar Isabelle ones;
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederother \emph{let} expressions (i.e. those containing patterns on the
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederleft hand-side) and the \emph{where} expressions are not covered. The
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitranslation of terms (minus mutual recursion) may be summed up,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiessentially, as follows:
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder$$\begin{array}{lcl}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \lceil c \rceil & = & c_{t} \\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \lceil \backslash x \ \to \ f \rceil & = & LAM \ x_{t}. \ \lceil f \rceil \\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \lceil f \ a_{1} \ldots a_{n} \rceil & = & FIX \ f_{t}. \ f_{t} \ \cdot \
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \lceil a \rceil \ldots \cdot \ \lceil a_{n} \rceil \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder & let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% \ldots \lceil a_{n} \rceil \ TyCons_{t}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder%In HOLCF, where every type is a domain and every function is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent In HOLCF all recursive functions can be defined by fixpoint
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskioperator --- a function that, given as argument the defining term
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederabstracted of the recursive call name, returns the corresponding
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederrecursive function. Coding this directly turns out to be rather
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedercumbersome, particularly in the case of mutually recursive functions,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwhere tuples of defining terms and tupled abstraction would be needed.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiIn contrast, the \emph{fixrec} package allows us to handle fixpoint
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidefinitions in a way much more similar to ordinary Isabelle recursive
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdefinitions, providing with friendly syntax for mutual recursion,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias well. Continuing the example,\\
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\noindent $ fun1 \ :: \ (a \to c) \ \to \ (b \to d) \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\to \ AType \ a \ b \ \to \ AType \ c \ d $
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski$$\begin{array}{lll}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski fun1 & f \ g \ k & = \ case \ k \ of \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & ABase \ x & \to \ ABase \ (f \ x) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & AStep \ x \ y & \to \ AStep \ (fun1 \ f \ g \ x) \ (fun2 \ f \ g \
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\end{array} $$
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski$ fun2 \ :: \ (a \to c) \ \to \ (b \to d) \ \to \ BType \ a \ b \ \to \ BType \ c \ d $
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski$$\begin{array}{lll}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski fun2 & f \ g \ k & = \ case \ k \ of \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski & BBase \ x & \to \ BBase \ (g \ x) \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski & BStep \ x \ y & \to \ BStep \ (fun2 \ f \ g \ x) \ (fun1 \ f \ g \ y)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\end{array} $$
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\noindent this code translates to HOLCF as follows:\\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\noindent $consts $
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski$$ \begin{array}{ll} fun1 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to 'd::pcpo) \ \to \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski & ('a::pcpo, 'b::pcpo) \ AType \ \to \ ('c::pcpo, 'd::pcpo) \ AType \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski fun2 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski 'd::pcpo) \ \to \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski & ('a::pcpo, 'b::pcpo) \ BType \ \to \ ('c::pcpo,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski 'd::pcpo) \ BType
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder$$\begin{array}{rccl}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder fixrec & fun1 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
c5e63ec138b908ac9d15e6843120033bf36a1862Till Mossakowski & & & ABase \cdot pX1 \ => \ ABase \cdot (f \cdot pX1) \ | \\
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maeder & & & AStep \cdot pX1 \cdot pX2 \ => \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & & & \ AStep \cdot (fun1 \cdot f \cdot g \cdot pX1) \cdot (fun2 \cdot f \cdot g \cdot pX2)) \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder and & fun2 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski & & & BBase \cdot pX1 \ => \ BBase \cdot (g \cdot pX1) \ | \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski & & & BStep \cdot pX1 \cdot pX2 \ => \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski & & & \ BStep \cdot (fun2 \cdot f \cdot g \cdot pX1) \cdot (fun1 \cdot f \cdot g \cdot pX2)) \end{array}$$
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\noindent The translations take care automatically of the fact that,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiin contrast with Haskell, Isabelle requires patterns in case
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiexpressions to follow the order of datatype declarations.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiIn the Programatica representation of Haskell, class information about
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertype parameters is given by adding dictionary parameters to normal
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiones. These are eliminated by the translation, as class information in
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiIsabelle may be given by annotating arguments. In particular, each
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidefinition includes the type of the defined function complete with
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiclass annotation, in order to allow for overloading (a detail we
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederomitted to show for the sake of readability in some of the examples
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{HOL: Type signature}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiThe translation to HOL is semantically rather crude, it takes into
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiaccount neither partiality nor laziness, and so, for soundness, it
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederrequires all functions in the program to be total ones.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederAn account of partiality could be obtained using the \emph{option}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maedertype constructor to lift types, along lines similar to those followed
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederin HOLCF with \emph{lift}. Here instead we are just mapping Haskell
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maedertypes to corresponding, unlifted HOL ones --- so for booleans and
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederintegers. Type variables are of class \emph{type}. HOL function type,
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederproduct and list are used to translate the corresponding Haskell
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederconstructors. The translation of types (minus mutual recursion) may be
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maedersummed up as follows.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder% Haskell datatype and function declarations are translated to
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder% declarations in HOLCF.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder$$\begin{array}{lcl}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \lceil a \rceil & = & 'a_{t}::type \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \lceil Bool \rceil & = & bool \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \lceil Integer \rceil & = & int \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \lceil a \to b \rceil & = & \lceil a \rceil \Rightarrow \lceil b \rceil \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \lceil [a] \rceil & = & \lceil a \rceil \ list \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Recursive and mutually recursive data-types declarations are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitranslated to HOL as datatype declaration.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich$$\begin{array}{rll} datatype & \ ('a, 'b) \ BType & = \ BBase \ 'b \ | \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & & BStep \ (('a, 'b) \ BType) \ (('a, 'b) \ AType) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski and & \ ('a, 'b) \ AType & = \ ABase \ 'a \ | \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & & AStep \ (('a, 'b) \ AType) \ (('a, 'b) \ BType) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Metalevel features are essentially shared with the HOLCF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{HOL: Sentences}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNon-recursive definitions are treated in an analogous way to the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslation into HOLCF. Standard lambda-abstraction ($\%$) and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifunction application are used here instead of continuous ones. Partial
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifunctions, and particularly case expressions with incomplete patterns,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare not allowed. The translation of terms (minus recursion and case
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexpressions) may be summed up as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{lcl}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \lceil c \rceil & = & c_{t} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil \backslash x \ \to \ f \rceil & = & \% \ x_{t}. \ \lceil f \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil f \ a_{1} \ldots a_{n} \rceil & = & f_{t} \ \lceil a \rceil \ldots \ \lceil a_{n} \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder% \ldots \lceil a_{n} \rceil \ TyCons_{t}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Recursive definitions set HOL and HOLCF apart. In HOL a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidistinction is drawn, and syntactically highlighted, between primitive
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirecursive functions (introduced by keyword \emph{primrec}) and generic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirecursive ones (by keyword \emph{recdef}). Termination is guaranteed
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor each of the formers, by the fact that recursion is based on the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidatatype structure of one of the parameters. In contrast, termination
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis not a trivial matter for the latters. A strictly decreasing measure
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimust be provided, associated to the parameters of the defined
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifunction. This requires a degree of ingenuity that cannot be easily
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidealt with automatically. For this reason, the translation to HOL is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirestricted to primitive recursive functions.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederMutual recursion is allowed for under additional restrictions --- more
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederprecisely: 1) all the functions involved are recursive in the first
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiargument; 2) recursive arguments are of the same type in each
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifunction. The translation of mutually recursive functions $a
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\rightarrow b, \ldots a \rightarrow d$ introduces a new function $a
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\rightarrow (b * \ldots * d)$ recursively defined, for each case
30256573a343132354b122097b0ee1215dda1364Till Mossakowskipattern, as the product of the values
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicorrespondingly taken by the original, non-recursively defined ones. \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $ fun3 \ :: \ AType \ a \ b \to (a \to a) \to AType \ a \ b $
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder$$\begin{array}{ll}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifun3 \ k \ f & = \ case \ k \ of \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski & ABase \ a \to ABase \ (f \ a) \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski & AStep \ a \ b \to AStep \ (fun4 \ a) \ b \\
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\noindent $ fun4 \ :: \ AType \ a \ b \to AType \ a \ b $
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski$$\begin{array}{ll}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskifun4 \ k & = \ case \ k \ of \\
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski & AStep \ x \ y \to AStep \ (fun3 \ x \ (\backslash z \to z)) \ y \\
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski & ABase \ x \to ABase \ x \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent These functions, satisfying the restrictions, will translate
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskito the following.\\
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\noindent $consts$
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski$$\begin{array}{ll}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfun3 \ :: & ('a::type, 'b::type) AType \Rightarrow ('a::type \Rightarrow 'a::type) \Rightarrow \\ & ('a::type, 'b::type) AType \\
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskifun4 \ :: & ('a::type, 'b::type) AType \Rightarrow ('a::type \Rightarrow 'a::type) \Rightarrow\\ & ('a::type, 'b::type) AType \\
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskifun3\_Xfun4\_X :: & ('a::type, 'b::type) AType \Rightarrow \\ & (('aXX1::type \Rightarrow 'aXX1::type) \Rightarrow \\ & ('aXX1::type, 'bXX1::type) AType) * \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & (('aXX2::type \Rightarrow 'aXX2::type) \Rightarrow \\ & ('aXX2::type, 'bXX2::type) AType) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent $defs$
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$$\begin{array}{lll}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifun3\_def : & fun3 \ == \ \% k \ f. \ fst \ (( fun3\_Xfun4\_X :: \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \ ('a::type, 'b::type) AType \Rightarrow (('a::type \Rightarrow 'a::type) \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski& \Rightarrow ('a::type, 'b::type) AType) * ((unit \Rightarrow unit) \Rightarrow \\ & (unit, unit) AType) ) \ k) \ f \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederfun4\_def : & fun4 \ == \ \% k \ f. \ snd \ (( fun3\_Xfun4\_X :: \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & ('a::type, 'b::type) AType \Rightarrow ((unit \Rightarrow unit) \Rightarrow (unit, unit) AType) * \\ & (('a::type \Rightarrow 'a::type) \Rightarrow ('a::type, 'b::type) AType) ) \ k) \ f \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $primrec$
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$$\begin{array}{lll}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskifun3\_Xfun4\_X & (ABase \ pX1) \ = & (\% f. \ ABase \ (f \ pX1), \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder & & \% f. \ ABase \ pX1) \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederfun3\_Xfun4\_X & (AStep \ pX1 \ pX2) & = \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & (\% f. \ AStep \ (snd & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2, \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \% f. \ AStep \ (fst & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2) \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\noindent Calls of the recursive functions in the non-recursive
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederdefinitions are annotated with type where exceeding type variables are
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederinstantiated with the unit type, as required by Isabelle in order to
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederavoid definitions from which inconsistencies are derivable.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{Patterns}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\label{sec:Patterns}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSupport of patterns in definitions and case expressions is more
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirestricted in Isabelle than in Haskell. Nested patterns are overall
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidisallowed. In case expressions, the case term is required to be a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskivariable. Both of these restrictions apply to our translations. A
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifurther Isabelle limitation concerning case expressions ---
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisensitiveness to pattern order --- is dealt with automatically.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSimilarly, wildcards --- something unknown to Isabelle --- are dealt
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwith, as well as, in HOLCF, incomplete patterns. The exclusion of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskinested patterns complicate the translation of some specific ones ---
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin fact, guarded expressions and list comprehension are not covered;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertheir use should be avoided here, using conditional expressions and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\emph{map} instead.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% not allowed in Isabelle with ordinary definitions (keyword
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski% \emph{Defs}), but it is allowed with the syntax for recursive ones.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMultiple function definitions using top level pattern matching are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitranslated as definitions based on a single case expression; this is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidue to HOL more than to HOLCF. In fact, multiple definitions in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle are only allowed with the syntax of recursive ones. However,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin HOL primitive recursive definitions, patterns are allowed for only
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin one parameter. In order to translate definitions with more patterns
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias arguments, without resorting to tuples and to more complex syntax
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(\emph{recdef} instead of \emph{primrec}) we translate multiple
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidefinitions by top level pattern matching
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskias definitions by case construct.\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $ctl \ :: \ Bool \to Bool \to Bool \to Bool$ \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$ctl \ False \ a \ False \ = \ a $\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$ctl \ True \ a \ False \ = \ False $\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$ctl \ False \ a \ True = \ True $\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$ctl \ True \ a \ True \ = \ a $\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent This translates to HOL as the following.\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $consts \ ctl :: \ bool \Rightarrow bool \Rightarrow bool \Rightarrow bool$\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $defs$
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$$\begin{array}{llll}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederctl\_def : & ctl \ == & \% qX1. \% qX2. \% qX3. & case \ qX1 \ of \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & & False \Rightarrow case \ qX3 & of \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & & & False \Rightarrow qX2 \ | \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & & True \Rightarrow True \ | \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & True \Rightarrow case \ qX3 & of \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & & False \Rightarrow False \ | \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & & True \Rightarrow qX2 \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent This example does not go through with the translation to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHOLCF, as booleans there are translated to values of \emph{tr}, which
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederis not a recursive datatype. The following gives an alternative that
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskican be handled (a new datatype is used instead of booleans).\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $data \ Two \ = Fx \ | \ Tx $\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $ctlx :: \ Two \to Two \to Two \to Two $ \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$ctlx \ Fx \ a \ Fx \ = \ a $ \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$ctlx \ Tx \ a \ Fx \ = \ Fx $ \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$ctlx \ Fx \ a \ Tx \ = \ Tx $ \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$ctlx \ Tx \ a \ Tx \ = \ a $\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent This translates to HOLCF as follows.\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $domain \ Two \ = \ Fx \ | \ Tx $
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $consts \ ctlx :: \ Two \to Two \to Two \to Two$\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $defs$
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$$\begin{array}{llll}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskictlx\_def : & map5 \ == & LAM \ qX1 \ qX2 \ qX3. & case \ qX1 \ of \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & Fx \Rightarrow case \ qX3 & of \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & & Fx \Rightarrow qX2 \ | \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & & Tx \Rightarrow Tx \ | \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & Tx \Rightarrow case \ qX3 & of \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & & & Fx \Rightarrow Fx \ | \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & & & Tx \Rightarrow qX2 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent In case expressions as well as in top level pattern matching
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidefinitions, wildcards may be used --- though not in nested position.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIncomplete patterns are translated to HOLCF using $\bot$ as default
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\subsection{Classes}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiHaskell defined classes are translated to Isabelle as classes with
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiempty axiomatization. Isabelle allows classes with no more than one
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskitype parameter, therefore our translations can support only them ---
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiit might be possible to handle more than one parameter using tuples,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskibut this would surely involve considerable complications dealing with
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiconditional instances.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiInstance declarations are translated to corresponding ones in
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiIsabelle. Isabelle instances in general require proofs that class
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiaxioms are satisfied by the types, but as long as there are no axioms
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe proofs are trivial and can be handled automatically. Function
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskideclarations associated with Haskell classes are translated as
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiindependent function declarations with appropriate class annotation.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiFunction definitions associated with instance declarations are
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskitranslated as overloaded function definitions,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskirelying on class annotation of the typed variables.\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $class ClassA \ a \ where$
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$abase :: \ a \to Bool $
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$ astep :: \ a \to Bool $\\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent $instance \ (ClassA \ a, \ ClassA \ b) \Rightarrow ClassA \ (AType \ a \ b) \ where $
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$$\begin{array}{ll}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiabase \ x \ = & case \ x \ of \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski & ABase \ u \ \to \ True \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski & \_ \ \to \ False \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent This code translates to HOLCF as follows.\\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent $axclass \ ClassA < pcpo$
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent $instance \ AType::({pcpo, ClassA}, {pcpo, ClassA}) \ ClassA$
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$by \ intro\_classes$\\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent $consts$
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$\begin{array}{ll}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiabase :: & 'a::\{ClassA, pcpo\} \to tr \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiastep :: & 'a::\{ClassA, pcpo\} \to tr \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskidefault\_abase :: & 'a::\{ClassA, pcpo\} \to tr \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidefault\_astep :: & 'a::\{ClassA, pcpo\} \to tr \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\noindent $defs$
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski$$\begin{array}{rl}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAType\_abase\_def : & \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder abase :: & ('a::\{ClassA, pcpo\}, 'b::\{ClassA, pcpo\}) \ AType \to tr \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder == & LAM x. \ case \ x \ of \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder & ABase \cdot pX1 \Rightarrow TT \ | \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder & AStep \cdot pX2 \cdot pX1 \Rightarrow FF \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederAType\_astep\_def : & \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder astep :: & ('a::\{ClassA, pcpo\}, 'b::\{ClassA, pcpo\}) \ AType \to tr \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder & == default\_astep \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\noindent Similarly, it translates to HOL.\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent $axclass \ ClassA < type$\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent $instance \ AType::(\{type, ClassA\}, \{type, ClassA\}) \ ClassA$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$by \ intro\_classes$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $consts$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiabase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiastep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidefault\_abase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidefault\_astep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $defs$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{rl}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAType\_abase\_def : & \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski abase :: & ('a::\{ClassA, type\}, 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski == & \% x. \ case \ x \ of \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & ABase \ pX1 \Rightarrow True \ | \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & AStep \ pX2 \ pX1 \Rightarrow False \\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAType\_astep\_def : & \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski astep :: & ('a::\{ClassA, type\}, 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski == & default\_astep\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection{Equality}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAt the moment equality is the only covered built-in class. The
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiaxiomatizations provided, respectively, in \emph{HsHOLCF} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{HsHOL} are based on the abstract definition of the equality and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinequality functions \cite{HaskellRep}. In both theories, \emph{Eq} is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskideclared as a subclass of \emph{type} --- in \emph{HsHOLCF} this is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidone in order to instantiate it with lifted types.\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $consts$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$ \begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskihEq :: & ('a::Eq) lift \ \to \ 'a \ lift \ \to \ tr \\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskihNEq :: & ('a::Eq) lift \ \to \ 'a \ lift \ \to \ tr\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $axioms$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiaxEq: & ALL x. (hEq \cdot p \cdot q \ = \ Def x) \ = \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & (hNEq \cdot p \cdot q \ = \ Def (\sim x)) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent The instantiation of equality (consequently, of inequality) for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiboolean (and similarly for integer) is obtained by lifting HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiequality so that $\bot$ is returned whenever one of the argument is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $tr\_hEq\_def: \ hEq \ == \ fliftbin \ (\% (a::bool) \ b. \ a \ = \ b)$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%ax1: & hEq \cdot p \cdot p \ == \ Def \ true \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%ax2: & [| \ hEq \cdot q \cdot r \ = \ Def \ true; \ hEq \cdot p \cdot q \ = \ Def \ true \ |] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% & ==> \ hEq \cdot p \cdot r \ = \ Def \ true \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent In \emph{HsHOL} the axiomatization reflects the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirestriction to terminating programs.\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $consts$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskihEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskihNEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $axioms$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski axEq: & hEq \ p \ q \ == \ \sim hNEq \ p \ q \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent The instantiation of \emph{hEq} for boolean and integer is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisimply taken to be HOL equality.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% ax1: & hEq \ p \ p \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% ax2: & [| \ hEq \ q \ r; \ hEq \ p \ q \ |] ==> hEq \ p \ r \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Monads}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:Monads}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle does not allow for classes of type constructors, hence a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproblem in representing monads. We could deal with this problem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelying on an axiomatization of monads that allows for the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirepresentation of monadic types as an axiomatic class, as presented in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Lueth}. Monadic types should be translated to newly defined
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitypes that satisfy monadic axioms. This would involve defining a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheory morphism, as an instantiation of type variables in the theory
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof monads. We are planning to rely on AWE \cite{AWE}, an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimplementation of theory morphism on top of Isabelle base logic that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimay be used to extend HOL as well.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Conclusion}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following is a list of features that are covered by our
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{itemize}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item predefined types: boolean, integer.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item predefined type constructors: function, cartesian product, list.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item declaration of recursive datatype, including mutually recursive ones.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item predefined functions: equality, booelan constructors,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski connectives, list constructors, head and tail list functions,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski arithmetic operators.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item non-recursive functions, including conditional, \emph{case} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \emph{let} and expressions (with restriction related to use of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item use of incomplete patterns (in HOLCF) and of wildcards in case
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item total primitive recursive functions (in HOL)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand partial recursive ones (in HOLCF), including mutual ones (with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirestrictions in the HOL case).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item single-parameter class and instance declarations.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \item monad declarations and do notation.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe shallow embedding approach makes it possible to take the most out
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the automation currently available on Isabelle, especially in HOL.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFurther work should include extending the translation to cover the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhole of the Haskell Prelude. We would also be interested in carrying
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiout an extension to cover P-logic \cite{KiebPl}, a specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiformalism for Haskell programs included in the Programatica toolset.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%This translation, due to the character of the P-logic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%typing system, could be more easily carried out relying on some form
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%of universal quantification on type variables, or else further relying
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%on parametrisation.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\bibliographystyle{alpha}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\bibliography{case}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIn our example,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslation gives the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $consts$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$ \begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun1 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & ('a::type, 'b::type) \ Prelude\_AType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_AType \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun1\_Xfun2\_X & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & (('bXX1::type \Rightarrow 'dXX1::type) \ \Rightarrow \\ & ('aXX1::type, 'bXX1::type) \ Prelude\_AType \ \Rightarrow \\ & ('cXX1::type, 'dXX1::type) \ Prelude\_AType) * \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & (('bXX2::type \Rightarrow 'dXX2::type) \ \Rightarrow \\ & ('aXX2::type, 'bXX2::type) \ Prelude\_BType \ \Rightarrow \\ & ('cXX2::type, 'dXX2::type) \ Prelude\_BType) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun2 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & ('a::type, 'b::type) \ Prelude\_BType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_BType \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $defs$
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$$ \begin{array}{ll}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfun1\_def : & fun1 \ == \ \% f. \% g. \% k. \ fst (fun1\_Xfun2\_X \ f) \ g \ k \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun2\_def : & fun2 \ == \ \% f. \% g. \% k. \ snd (fun1\_Xfun2\_X \ f) \ g \ k
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent $primrec$
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$$ \begin{array}{ll}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder fun1\_Xfun2\_X \ (ABase \ pX1) & = \ (\% g. \% k. \ ABase \ (f \ pX1)) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun1\_Xfun2\_X \ (BBase \ pX1) & = \ (\% g. \% k. \ BBase \ (g \ pX1)) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun1\_Xfun2\_X \ (AStep \ pX1 \ pX2) & = \ (\% g. \% k. \ AStep \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder fun1\_Xfun2\_X \ (BStep \ pX1 \ pX2) & = \ (\% g. \% k. \ BStep \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\subsection{Equality: HOLCF}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\subsection{Equality: HOL}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederHaskell classes and instances are translated to Isabelle,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederrespectively, as classes with empty axiomatisation and as instances
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederwith trivial instantiation proof. The translation supports only
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisingle-parameter classes --- in principle, more than one parameter
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicould be handled using tuples.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiBuilt-in classes --- Eq and Ord in particular --- are translated to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskinewly defined classes in Isabelle; the corresponding axiomatisation
30256573a343132354b122097b0ee1215dda1364Till Mossakowskihowever here is not provided !!!
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiFunctions declarations associated to classes are translated to
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiIsabelle as independent function declarations with appropriate class
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederannotation. Function definitions associated to instances are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitranslated as overloaded function definitions, relying on class
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiannotation of typed variables.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu% ...xxx...!!! check out for stuff to include in Classes ---
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederNon-recursive definitions are translated to ordinary definitions (keyword
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\emph{defs}), whereas recursive ones require specific keywords. The
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescutype of the function, inclusive of class annotation, is included in
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuevery definitions in order to allow for overloading.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu%For values of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%built-in type, the lifting function is \emph{Def}; the undefined case
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%collapses on $\bot$.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuIn HOLCF, where every type is a domain and every function is
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescucontinuous, all recursive functions can be defined by fixpoint
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuoperator. This is essentially a function that, given as argument the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfunction definition body abstracted of the recursive call name,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescureturns the corresponding recursive function. Coding this directly
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuwould be rather cumbersome, particularly in the case of mutually
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescurecursive functions, where tuples of definition bodies and tupled
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuabstraction are needed. We can instead rely on the \emph{recdef}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescupackage, which allows to handle fixpoint definitions like ordinary
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederrecursive ones, offering nice syntax to deal with mutual recursion as
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\subsection{HOL: Type signature}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe present translation to HOL is very basic, and does take into
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuaccount neither partiality nor laziness. Essentially, it left to the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederHaskell programmer to check that all the functions are total ones.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederAn account of partiality -- although possibly not aof laziness ---
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercould be obtained using the option type constructor to lift types,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederalong a similar line to lift. Here however we are presenting just a
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuplain version, mapping Haskell types in the corresponding unlifted HOL
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescutypes. All variables belong to the class type. Recursive and mutually
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescurecursive data-types declarations are translated to HOL datatype
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{HOL: Function definitions}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiNon-recursive definitions and let expressions are treated similarly as
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin the translation to HOLCF. Recursive defitions is the topic that
30256573a343132354b122097b0ee1215dda1364Till Mossakowskireally sets HOL and HOLCF apart. In HOL a distinction has to be drawn
30256573a343132354b122097b0ee1215dda1364Till Mossakowskibetween primitive recursive functions and generic recursive ones. In
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe former, termination is guaranteed by the fact that recursive
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidefinitions are strictly associated with the datatype structure of a
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederparameter. In the latter, termination needs to be proved. This must be
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescudone, in a \emph{recdef} definition, by providing a measure for the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfunction parameter that can be proved to be strictly decreasing for
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescueach occurrence of a recursive call in the definition. This requires a
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescudegree of ingenuity that cannot be generally associated with an
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuautomated translation.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFor this reason, the translation of recursive functions to HOL is
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederrestricted to primitive recursive ones. Mutually recursive functions
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuare allowed under additional restrictions. These are: all the
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescufunctions should be recursive in the first argument; this should be of
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe same type for each of them; the constructors should be listed in
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthe same order in each of the case expressions; the variable names in
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe case patterns are expected to be maintained.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe translation of mutually recursive functions $a \rightarrow b, \ldots a
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescudefined, for each case pattern, as the product of the values
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescucorrespondingly taken by the original functions.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\subsection{Pattern matching}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSupport of pattern-matching in Isabelle is more restricted than in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHaskell. Nested patterns are disallowed; case expressions are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisensitive to the order of the constructors, which should be the same
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuas in the datatype declaration. In particular, the case variable si
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescurequired to be a variable. Translation of pattern-matching is
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederpotentially laborious. For this reason guarded expressions, list
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedercomprehension and nested pattern-matching have been left out; they
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedershould be replaced by the programmer, using conditional expressions
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuand map functions.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuFunction definition by top level pattern matching is not allowed in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIsabelle with ordinary definitions, but it is with those that are
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederexplicitly declared to be recursive ones. However, particularly in HOL
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuprimitive recursive definitions patterns are allowed in one parameter
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuonly. In order to translate function definitions with patterns in more
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithan one parameter, without resorting to using tuples and more complex
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskidefinitions (\emph{recdef} instead of \emph{primrec}), our
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescutranslations turn a multiple definition by top level pattern matching
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuinto a definition by case construct.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection{Classes}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederHaskell classes and instances are translated to Isabelle,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederrespectively, as classes with empty axiomatisation and as instances
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuwith trivial instantiation proof. The translation supports only
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescusingle-parameter classes --- in principle, more than one parameter
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicould be handled using tuples.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuBuilt-in classes --- Eq and Ord in particular --- are translated to
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescunewly defined classes in Isabelle; the corresponding axiomatisation
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuhowever here is not provided !!!
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuFunctions declarations associated to classes are translated to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIsabelle as independent function declarations with appropriate class
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettichannotation. Function definitions associated to instances are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitranslated as overloaded function definitions, relying on class
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuannotation of typed variables.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section*{Haskell2Isabelle}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe tool is designed to support the translation of simple but
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskirealistic Haskell programs to HOLCF and, with some restriction, to
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiHOL. Not all the syntactical features of Haskell are covered yet,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescualthough most of those used in the Prelude are. The most noticeable
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codesculimitations are related to built-in types, pattern-matching and local
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidefinitions. There are additional and more substantial restrictions
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiin the case of HOL, related to termination and to recursion.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThe application can be installed as part of Hets. It requires Haskell
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederGHC and Programatica. It is run by the command \emph{hets -t ...
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder [h|hc] file.hs} where the options stand for HOL and HOLCF,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederFor the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedermodule that contains the main translation function, carried out as
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedercomposition of a signature morphism and a theory morphism.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\emph{IsaSign.hs} contains the Hets representation of the Isabelle
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederbase logic and extensions.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThe general design of the translation functions, and particularly the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedertwo-layered recursion adopted for them, is similar to that used for
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederthe translation Haskell to Agda in Programatica.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\subsection{Monads}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederIsabelle does not allow for classes of type constructors, hence a
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederproblem in representing monads. We can deal with this problem,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederhowever, relying on an axiomatisation of monads that allows for the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederpresentation of monadic types as an axiomatic class, as provided in
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\cite{}. Therefore, monadic types can be translated to newly defined
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedertypes that are constrained to satisfy the monadic axioms. This
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederconstraining, carried out as an instantiation of type variables in the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedertheory of monads, takes the form of a theory morphism, and can be
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedercarried out automatically by AWE, an implementation of parametrisation
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand theory morphism on top of Isabelle basic logic, that may also be
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiused to extend HOL and HOLCF. The do notation can then be translated
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiby unpacking it into monadic operators. Attempting to translate
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimonadic notation without support AWE support will result in an error
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\section*{Conclusion}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe following is a list of constructs that are covered by all the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{itemize}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item predefined types: boolean, integer.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item predifed type constructors: funtion, cartesian product, list.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item declaration of recursive datatype, including mutually recursive ones.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item predefined functions: equality, booelan constructors,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder connectives, list constructors, head and tail list functions,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder arithmetic operations.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item non-recursive functions, including conditional,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederlet and case expressions.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item use of incomplete patterns (HOLCF) and of wildcards in case
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item total primitive recursive functions (HOL)
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederand partial recursive ones (HOLCF), including mutual ones (with
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederrestrictions in the HOL case).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item class and instance declarations.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item monad declarations and do notation.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe shallow embedding approach used by our translations should allow
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskito take as much advantage as possible of the automation currently
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiavailable on Isabelle, particularly in HOL.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederFurther work should include extending the translation to cover the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederwhole of the Haskell Prelude. We hope that this will make it possible
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederto support the verification of functional robotics programs.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederA further extension, in line with the work on Programtica, would be
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe translation of P-logic. This translation, due to the character of
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe P-logic typing system, could be more easily carried out relying on
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedersome form of universal quantification on type variables, or else
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederfurther relying on parametrisation.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\bibliographystyle{alpha}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\bibliography{case}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{document}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe translation of types is
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederOur general strategy for translating signatures is to map Haskell
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedertypes to Isabelle defined types.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder the fact that Haskell expressions are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskievaluated lazily, however it does not preserve The translation to HOL
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidoes not, and moreover requires that all the functions defined in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHaskell program are total ones...
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiAll types have a sort in Isabelle, defined by the set of the classes
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiof which it is a member. In HOL, all types belong to the class type;
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin HOLCF, they belong to class pcpo (pointed complete poset).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiAll Haskell function declarations are translated to Isabelle ones.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiType variables are assigned default sort type in HOL and pcpo in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiHOLCF. Names get translated by a function that preserves them, up to
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiavoidance of clashes with Isabelle keywords.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe only built-in types that are properly covered are booleans,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiunbounded integers and rationals. These get translated, in the case of
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiHOL, to Isabelle booleans, integers and rationals, respectively. Bound
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiintegers and floating point numbers would require low-level modelling,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiand have not been dealt with; anyway, bounded integers are accepted
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederand simply treated as unbounded by the application.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederIn the HOLCF translation, all built-in types get lifted to the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedercorresponding domains (pcpos), which by definion include the undefined
30256573a343132354b122097b0ee1215dda1364Till Mossakowskivalue, by using the lift HOLCF type constructor. In particular, type
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederboolean get translated to type tr (short for bool lift), and similarly
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederfor types integer and rational.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiRecursive data-types declarations can be translated to datatype
30256573a343132354b122097b0ee1215dda1364Till Mossakowskideclarations in HOL. In HOLCF they can be translated to domain
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederdeclarations. The two structure are quite similar, except that in
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidomains, which are pcpo, all the parameters are required to be pcpos
30256573a343132354b122097b0ee1215dda1364Till Mossakowskias well. Morevover, Isabelle domain declarations require to introduce
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinames for destructors. Mutually recursive Haskell datatypes can be
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitranslated to both logics, relying on the specific Isabelle syntax for
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederA type class in Isabelle is conceptually quite different from one in
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederHaskell. The former is associated to a set of axioms, whereas the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederlatter is associated to a set of function declarations. Isabelle
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederclasses may have at most a type parameter. Moreover, Isabelle does
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichnot allow for type constructor classes. The last limitation is the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimost serious of the three, since it makes quite hard to cope with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimonads. We can get around this obstacle relying on a method for the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiaxiomatic encoding of monads in HOL that uses parametrisation.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederParametrisation based on theory morphism has been implemented, as a
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiconservative extension of various Isabelle logics, in AWE, a tool
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederdesigned to support proof reuse \cite{AWE}.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe \emph{lift} type constructor, in particular, lifts each HOL type
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederto a flat domain, by adding a bottom element to them. We are going to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiuse it to lift the basic types. For the product we are going to use
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinon-strict product.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederformalisation on Isabele relies on axiomatic type classes \cite{},
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederwith \emph{pcpo} (pointed complete partial order) as the default
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederclass, in which the type of continuous functions can be represented as
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederfunction spaces, allowing for an elegant interpretation of recursion
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederby fixpoint operator. HOL types may be lifted to \emph{pcpo} by simply
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederadding a bottom element to them. This is what the type constructor
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\emph{lift} does, thus providing also a way of handling partiality ---
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederundefined cases can be mapped to the bottom element. HOLCF has also a
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedertype constructor \emph{u} that allows to deal with laziness, by
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederguaranteeing $\bot \neq \smath{up} \$ (\bot)$.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIn the case of HOLCF, the logic provides a computational
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinterpretation of function types as domains. In HOL there is no such
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfacility, therefore either appropriate types for the translation are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiintroduced --- as in \cite{}, or considerable semantical restrictions
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimust be accepted --- this is also the case for one of the translation
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederto FOL proposed in \cite{}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederDepending on the expressiveness of the logic, the translation of the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederprogramming language may be carried out at different levels of depth.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn general, the deeper is the embedding, the less it relies on
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskimeta-level features of the target language. This may be a plus, either
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifrom the point of view of semantic clarity, or from that of
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiexpressiveness. Taking advantage of meta-level feaures, on the other
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskihand, may be useful in order to make the theorem proving less tedious,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby allowing more constant use of generic proof methods. It may also
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichultimately affect positively the theorem prover economy, by
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskireinforcing the bias toward the development of proof methods that,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederhowever specific, can be more easily integrated with generic ones.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder% a point made in \cite{}. for example by allowing a straightforward
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder% operational interpretation ---
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe translations of Haskell to HOLCF and HOL that we are presenting in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthe following justify themselves in terms of denotational semantics.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe translation to HOLCF differs from that proposed in \cite{} in the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertreatment of types. We translate Haskell types directly into HOLCF
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederones, whereas they use HOLCF terms to embed Haskell types. We assume
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthat the HOLCF types are similar enough to the those of Haskell, in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichorder to guarantee the semantical correctness of our translations.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichMoreover, we rely on axiomatic classes to translate Haskell types
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiOur approach has the advantage of giving a shallower embedding,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskihowever it has the drawback of not bein complete --- notably, type
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiconstructor classes are missing. We plan to handle in future this
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiproblem (see section~\ref{sec:Monads}) by relying on an extension of
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIsabelle based on morphism between theories. The translation into HOL
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiis essentialy only a first experiment, it handles types very
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsimplistically, relying on drastic semantical restrictions for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcorrecteness. Under those restrictions, however, it gives expressions
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthat are comparatively quite simple to work with.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederA type class in Isabelle is conceptually quite different from one in
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederHaskell. The former is associated to a set of axioms, whereas the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlatter is associated to a set of function declarations. Isabelle
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederclasses may have at most a type parameter. Moreover, Isabelle does
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedernot allow for type constructor classes. The last limitation is the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermost serious of the three, since it makes quite hard to cope with
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermonads. We can get around this obstacle relying on a method for the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederaxiomatic encoding of monads in HOL that uses parametrisation.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederParametrisation based on theory morphism has been implemented, as a
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederconservative extension of various Isabelle logics, in AWE, a tool
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederdesigned to support proof reuse \cite{AWE}.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{Types}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederHOLCF allows has types for computable functions --- defined as sets of
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercontinuous functions of a type (!! fixpoints!!). It has a type
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederconstructor \emph{lift} that lifts HOL types to \emph{pcpo}s, thus
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederproviding a way of handling partiality --- undefined cases can be
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermapped to the bottom element. It has also a type constructor \emph{u}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthat allows to deal with laziness, by guaranteeing $\bot \neq
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\smath{u}(\bot)$.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthat can be used to embed Haskell function types.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe translation to HOLCF differs from that to HOL insofar as only the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfirst one relies on a denotational semantics for the full language,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederkeeping into account partiality and lazy evaluation, and associating
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederrecursive functions to corresponding fixed points, using on the Fixrec
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederextension of HOLCF. The translation to HOL is more restrictive; it
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederdoes not keep into account any form of partiality, and it restricts
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertranslation of recursive functions to the primitive recursive ones.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederIt would have been possible to give an account of partiality in HOL by
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederusing option types. However, we chose to keep the HOL translation as
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedersimple as possible for didactic purpose.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{maybe}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe translations of Haskell that we are presenting in the following,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederwe present translations of Haskell into some of the Isabelle logics.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThese translations are implemented as part of Hets, and are based on a
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedershallow embedding approach quite different from that used in
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederProgramatica. In our translations Haskell types are mapped to Isabelle
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertypes. We are assuming that the type systems of HOL and HOLCF are
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedersimilar enough to the type system of Haskell, in order to guarantee
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthe semantical correctness of our translations. Moreover, we rely on
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederaxiomatic classes to translate Haskell types classes.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederA type class in Isabelle is conceptually quite different from one in
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederHaskell. The former is associated to a set of axioms, whereas the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlatter is associated to a set of function declarations. Isabelle
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederclasses may have at most a type parameter. Moreover, Isabelle does
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedernot allow for type constructor classes. The last limitation is the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermost serious of the three, since it makes quite hard to cope with
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermonads. We can get around this obstacle relying on a method for the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederaxiomatic encoding of monads in HOL that uses parametrisation.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederParametrisation based on theory morphism has been implemented, as a
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederconservative extension of various Isabelle logics, in AWE, a tool
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederdesigned to support proof reuse \cite{AWE}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe translation to HOLCF differs from that to HOL insofar as only the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfirst one relies on a denotational semantics for the full language,
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckekeeping into account partiality and lazy evaluation, and associating
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskirecursive functions to corresponding fixed points, using on the Fixrec
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiextension of HOLCF. The translation to HOL is more restrictive; it
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskidoes not keep into account any form of partiality, and it restricts
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitranslation of recursive functions to the primitive recursive ones.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIt would have been possible to give an account of partiality in HOL by
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiusing option types. However, we chose to keep the HOL translation as
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskisimple as possible for didactic purpose.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{Type signature}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederOur general strategy for translating signatures is to map Haskell
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertypes to Isabelle defined types. The translation to HOLCF keeps into
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederaccount the fact that Haskell expressions are evaluated lazily. The
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertranslation to HOL does not, and moreover requires that all the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfunctions defined in the Haskell program are total ones...
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederAll types have a sort in Isabelle, defined by the set of the classes
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederof which it is a member. In HOL, all types belong to the class type;
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederin HOLCF, they belong to class pcpo (pointed complete poset).
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederAll Haskell function declarations are translated to Isabelle ones.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichType variables are assigned default sort type in HOL and pcpo in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichHOLCF. Names get translated by a function that preserves them, up to
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichavoidance of clashes with Isabelle keywords.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe only built-in types that are properly covered are booleans,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichunbounded integers and rationals. These get translated, in the case of
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichHOL, to Isabelle booleans, integers and rationals, respectively. Bound
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichintegers and floating point numbers would require low-level modelling,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichand have not been dealt with; anyway, bounded integers are accepted
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichand simply treated as unbounded by the application.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIn the HOLCF translation, all built-in types get lifted to the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcorresponding domains (pcpos), which by definion include the undefined
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichvalue, by using the lift HOLCF type constructor. In particular, type
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichboolean get translated to type tr (short for bool lift), and similarly
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfor types integer and rational.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichRecursive data-types declarations can be translated to datatype
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichdeclarations in HOL. In HOLCF they can be translated to domain
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichdeclarations. The two structure are quite similar, except that in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichdomains, which are pcpo, all the parameters are required to be pcpos
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichas well. Morevover, Isabelle domain declarations require to introduce
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichnames for destructors. Mutually recursive Haskell datatypes can be
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichtranslated to both logics, relying on the specific Isabelle syntax for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichwe present translations of Haskell into some of the Isabelle logics.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThese translations are implemented as part of Hets, and are based on a
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichshallow embedding approach quite different from that used in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichProgramatica. In our translations Haskell types are mapped to Isabelle
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichtypes. We are assuming that the type systems of HOL and HOLCF are
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsimilar enough to the type system of Haskell, in order to guarantee
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthe semantical correctness of our translations. Moreover, we rely on
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichaxiomatic classes to translate Haskell types classes.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIn the following, we present translations of Haskell into some of the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIsabelle logics. These translations are implemented as part of Hets,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichand are based on a shallow embedding approach quite different from
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthat used in Programatica. In our translations Haskell types are
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichmapped to Isabelle types. We are assuming that the type systems of HOL
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichand HOLCF are similar enough to the type system of Haskell, in order
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichto guarantee the semantical correctness of our translations. Moreover,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiwe rely on axiomatic classes to translate Haskell types classes.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich are those presented in \cite{}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichas well as in \cite{}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichtranslation of Haskell
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichinto FOL \cite{} and that into
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIn \cite{} Haskell is embedded in Martin-Loef
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichtype theory, implemented on Agda.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich is indeed a general difference between a lower level
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichapproach based on operational semantics, followed in \cite{agda} and
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\cite{miranda}, and a higher-level one, based essentially on
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichdenotational semantics, followed in \cite{}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe correctness of such embeddings
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichalways rests, ultimately, on the denotational semantics of Haskell,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichand on the possibility to encode it in a logic under consideration.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\cite{Thompson95}. Indeed, Haskell --- a strongly typed, purely
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfunctional language with lazy evaluation, based on a system of
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichpolymorphic types extended with type constructor classes, where monads
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederallow for side effects and pseudo-imperative code \cite{Hudak} --- has
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichalready been considered several times as a target for verification
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiAll the above-mentioned works provide embeddings of Haskell, either
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichpartial or total, into programming logic implemented on theorem
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiprovers. The correctness of such embeddings always rests, ultimately,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederon the denotational semantics of Haskell, and on the possibility to
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiencode it in a logic under consideration.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe tools, the logic and the ways in which the encoding can be done
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermay differ quite deeply. In \cite{} Haskell is embedded in Martin-Loef
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitype theory, implemented on Agda. All the other examples rely on
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIsabelle, a generic theorem-prover written in SML that allows for the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederformalisation of a variety of logics, including FOL, HOL and HOLCF
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{Paulson94isa}. The embedding in \cite{} rely on FOL, the
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIsabelle implementation of classical first-order logic.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiAll the other examples \cite{...} rely on higher-order logic. HOL is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithe implementation of classical higher-order logic based on simply
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskityped lambda calculus, extended with axiomatic type classes. HOLCF
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{holcf} is the extension of HOL with a formalisation of the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitheory of computable functions (LCF) based on axiomatic type classes.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% other words, we need to represent the program in a mechanised logic in
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% which the requirements can be expressed, as well.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% The representation can take different forms. It is possible to
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% associate the state-machine behavioural description to models in a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% logic. Another possibility is to represent the program in terms of a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% computational logic based on the operational semantics of the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% In both cases however, a significant part of the work has to
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% be carried out before the actual verification may take place.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIn order to verify a program, we need to associate its code to a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilogical representation that allows for requirements to be expressed
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiand for proofs to be carried out. There are different ways to do this.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe way we carry this out here is to embed Haskell into an expressive
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskihigher-order logic, together with providing an implementation of the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiembedding that allows for an automated translation of Haskell. From
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithe theoretical point of view, the correctness of the embdedding
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskidepends on the denotational semantics of the language. From the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederpractical point of view, once the program code can be translated
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiautomatically to the logic, all the burden of the verification can
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskirest on the theorem proving.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederDepending on the expressiveness of the logic, the translation of the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiprogrmaming language may be carried out at different levels of depth.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiIn general, the deeper is the embedding, the less it relies on
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maedermeta-level features of the target language. This may be a plus from
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederthe point of view of semantic clarity. Taking advantage of meta-level
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskifeaures, on the other hand, may be useful in order to make the theorem
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiproving less tedious.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiIsabelle is a generic theorem-prover written in SML that allows for
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithe formalisation of a variety of logics \cite{Paulson94isa}.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiIsabelle-HOL is the implementation of classical higher-order logic
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskibased on simply typed lambda calculus, extended with axiomatic type
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiclasses. Isabelle-HOLCF \cite{holcf} is the extension of HOL with a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiformalisation of the theory of computable functions (LCF) based on
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiaxiomatic type classes.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHets \cite{Hets} is a parsing, static analysis and proof management
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskitool designed to interface with various language specific tools, in
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiorder to support heterogeneous specification. In particular, for the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiparsing and static analysis of Haskell programs Hets relies on
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederProgramatica \cite{PTeam}, a tool that has its own proof management,
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederincluding a translation of Haskell to Isabelle-HOLCF.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederThe translations of Haskell that we are presenting in the following,
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederwe present translations of Haskell into some of the Isabelle logics.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederThese translations are implemented as part of Hets, and are based on a
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedershallow embedding approach quite different from that used in
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederProgramatica. In our translations Haskell types are mapped to Isabelle
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedertypes. We are assuming that the type systems of HOL and HOLCF are
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedersimilar enough to the type system of Haskell, in order to guarantee
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederthe semantical correctness of our translations. Moreover, we rely on
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederaxiomatic classes to translate Haskell types classes.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederA type class in Isabelle is conceptually quite different from one in
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederHaskell. The former is associated to a set of axioms, whereas the
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederlatter is associated to a set of function declarations. Isabelle
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederclasses may have at most a type parameter. Moreover, Isabelle does
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedernot allow for type constructor classes. The last limitation is the
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckemost serious of the three, since it makes quite hard to cope with
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckemonads. We can get around this obstacle relying on a method for the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederaxiomatic encoding of monads in HOL that uses parametrisation.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeParametrisation based on theory morphism has been implemented, as a
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederconservative extension of various Isabelle logics, in AWE, a tool
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdesigned to support proof reuse \cite{AWE}.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeThe translation to HOLCF differs from that to HOL insofar as only the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfirst one relies on a denotational semantics for the full language,
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckekeeping into account partiality and lazy evaluation, and associating
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckerecursive functions to corresponding fixed points, using on the Fixrec
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederextension of HOLCF. The translation to HOL is more restrictive; it
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdoes not keep into account any form of partiality, and it restricts
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecketranslation of recursive functions to the primitive recursive ones.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeIt would have been possible to give an account of partiality in HOL by
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiusing option types. However, we chose to keep the HOL translation as
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedersimple as possible for didactic purpose.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederThese translations are on the overall quite different from other ones
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederbased on deep embeddings, particularly from the Programatica
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedertranslation of Haskell into HOLCF \cite{Huff}, where the type system
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederis modelled at the logical level, as well as from translations of
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederMiranda and Haskell into FOL (Isabelle classical first-order logic)
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederwhere higher-order features have to be dealt with less directly
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\cite{Thompson95,Thompson92}.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\section*{The hs2thy tool}
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder(suggested change: from h2hf to hs2thy)
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederThe tool is designed to support the translation of simple but
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckerealistic Haskell programs to HOLCF and, with some restriction, to
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeHOL. Not all the syntactical features of Haskell are covered yet,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckealthough most of those used in the Prelude are. The most noticeable
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckelimitations are related to built-in types, pattern-matching and local
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckedefinitions. There are additional and more substantial restrictions
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiin the case of HOL, related to termination and to recursion.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederThe application can be installed as part of Hets. It requires Haskell
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederGHC and Programatica. It is run by the command \emph{h2hf
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder [h|hc|mh|mhc] file.hs} where the options stand, respectively, for
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeHOL, HOLCF, HOL extended with AWE and HOLCF extended with AWE.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeFor the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckemodule that contains the main translation function, carried out as
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketheory translation after a preliminary step of signature translation,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeand \emph{IsaSign.hs} contains the internal representation of Isabelle
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsection{Type signature}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeOur general strategy for translating signatures is to map Haskell
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketypes to Isabelle defined types. The translation to HOLCF keeps into
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeaccount the fact that Haskell expressions are evaluated lazily. The
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketranslation to HOL does not, and moreover requires that all the
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckefunctions defined in the Haskell program are total ones...
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeAll types have a sort in Isabelle, defined by the set of the classes
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeof which it is a member. In HOL, all types belong to the class type;
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckein HOLCF, they belong to class pcpo (pointed complete poset).
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiAll Haskell function declarations are translated to Isabelle ones.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiType variables are assigned default sort type in HOL and pcpo in
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHOLCF. Names get translated by a function that preserves them, up to
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiavoidance of clashes with Isabelle keywords.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeThe only built-in types that are properly covered are booleans,
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederunbounded integers and rationals. These get translated, in the case of
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederHOL, to Isabelle booleans, integers and rationals, respectively. Bound
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeintegers and floating point numbers would require low-level modelling,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeand have not been dealt with; anyway, bounded integers are accepted
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeand simply treated as unbounded by the application.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeIn the HOLCF translation, all built-in types get lifted to the
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maedercorresponding domains (pcpos), which by definion include the undefined
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckevalue, by using the lift HOLCF type constructor. In particular, type
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeboolean get translated to type tr (short for bool lift), and similarly
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckefor types integer and rational.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeRecursive data-types declarations can be translated to datatype
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckedeclarations in HOL. In HOLCF they can be translated to domain
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckedeclarations. The two structure are quite similar, except that in
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckedomains, which are pcpo, all the parameters are required to be pcpos
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeas well. Morevover, Isabelle domain declarations require to introduce
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckenames for destructors. Mutually recursive Haskell datatypes can be
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketranslated to both logics, relying on the specific Isabelle syntax for
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsection{Function definitions}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeHaskell function definitions are translated to corresponding Isabelle
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeones. Non-recursive definitions are translated to ordinary definitions
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke(keyword \emph{defs}), whereas recursive ones require specific
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckekeywords. The type of the function, inclusive of class annotation, is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiincluded in each of its definitions in order to allow for overloading.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederIn the translation to HOLCF, when the Haskell value is of built-in
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketype, the translated value has the lifted corresponding type --- this
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeis either the case of a lifted value (where \emph{Def} is the lifting
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederfunction) or the case of the undefined value (\emph{UU}).
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeAs to local definitions, they can be introduced in Haskell by let and
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckewhere expressions. Let expressions are translated to Isabelle let
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeexpressions, whereas where expressions are not covered.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsection{Recursive definitions}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeRecursive defitions is the topic that really sets HOL and HOLCF apart.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeIn HOLCF, where every type is a domain and every function is
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckecontinuous, all recursive functions can be defined by fixpoint
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskioperator. This is essentially a function that, given as argument the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskifunction definition body abstracted of the recursive call name,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskireturns the corresponding recursive function. Coding this directly
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiwould be rather cumbersome, particularly in the case of mutually
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskirecursive functions, where tuples of definition bodies and tupled
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiabstraction are needed. We can instead rely on the \emph{recdef}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskipackage, which allows to handle fixpoint definitions like ordinary
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskirecursive ones, offering nice syntax to deal with mutual recursion as
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe case of HOL is more compplex. There a distinction must be drawn
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskibetween primitive recursive functions and generic recursive ones. In
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskithe formers, termination is guaranteed by the fact that recursive
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskidefinitions are strictly associated with the datatype structure of a
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiparameter. In the latters, termination needs to be proved. This can be
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskidone, in a \emph{recdef} definition, by providing a measure for the
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskifunction parameter that can be proved to be strictly decreasing for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskieach occurrence of a recursive call in the definition. This requires a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskigenerally unbounded amount of ingenuity and cannot be carried out by a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskisimple translation.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederFor this reason, the translation of recursive functions to HOL is
30256573a343132354b122097b0ee1215dda1364Till Mossakowskirestricted to primitive recursive ones. Mutually recursive functions
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiare allowed under additional restrictions. These are: all the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifunctions should be recursive in the first argument, this should be of
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe same type for each of them, the constructors should be listed in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe same order in each of the case expressions, and also the variable
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinames in the case patterns are expected to be maintained.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe translation of mutually recursive functions $a \rightarrow b, \ldots a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidefined, for each case pattern, as the product of the values
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicorrespondingly taken by the original functions.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Pattern matching}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiSupport of pattern-matching in Isabelle is more restricted than in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHaskell. Nested patterns are disallowed; case expressions are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisensitive to the order of the constructors, which should be the same
30256573a343132354b122097b0ee1215dda1364Till Mossakowskias in the datatype declaration. In particular, the case variable si
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederrequired to be a variable. Translation of pattern-matching is
30256573a343132354b122097b0ee1215dda1364Till Mossakowskipotentially laborious. For this reason guarded expressions, list
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicomprehension and nested pattern-matching have been left out; they can
30256573a343132354b122097b0ee1215dda1364Till Mossakowskibe replaced without loss, anyway, using conditional expressions and
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimap functions.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFunction definition by top level pattern matching is not allowed in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIsabelle with ordinary definitions, but it is with those that are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiexplicitly declared to be recursive ones. However, particularly in HOL
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiprimitive recursive definitions patterns are allowed in one parameter
30256573a343132354b122097b0ee1215dda1364Till Mossakowskionly. In order to translate function definitions with patterns in more
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithan one parameter, without resorting to using tuples and more complex
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdefinitions (\emph{recdef} instead of \emph{primrec}), our
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitranslations turn a multiple definition by top level pattern matching
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinto a definition by case construct.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection{Classes}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHaskell classes and instances are translated to Isabelle,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskirespectively, as classes with empty axiomatisation and as instances
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwith trivial instantiation proof. The translation supports only
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisingle-parameter classes --- in principle, more than one parameter
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicould be handled using tuples.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiBuilt-in classes --- Eq and Ord in particular --- are translated to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinewly defined classes in Isabelle; the corresponding axiomatisation
30256573a343132354b122097b0ee1215dda1364Till Mossakowskihowever here is not provided.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFunctions declarations associated to classes are translated to
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIsabelle as independent function declarations with appropriate class
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiannotation. Function definitions associated to instances are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitranslated as overloaded function definitions, relying on class
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiannotation of typed variables.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{Monads}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\label{sec:Monads}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIsabelle does not allow for classes of type constructors, hence a
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiproblem in representing monads. We can deal with this problem,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskihowever, relying on an axiomatisation of monads that allows for the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskipresentation of monadic types as an axiomatic class, as provided in
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{}. Therefore, monadic types can be translated to newly defined
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitypes that are constrained to satisfy the monadic axioms. This
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiconstraining, carried out as an instantiation of type variables in the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitheory of monads, takes the form of a theory morphism, and can be
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicarried out automatically by AWE, an implementation of parametrisation
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiand theory morphism on top of Isabelle basic logic, that may also be
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiused to extend HOL and HOLCF. The do notation can then be translated
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiby unpacking it into monadic operators. Attempting to translate
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimonadic notation without support AWE support will result in an error
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section*{Conclusion}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe following is a list of constructs that are covered by all the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{itemize}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item predefined types: boolean, integer.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item predifed type constructors: funtion, cartesian product, list.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item declaration of recursive datatype, including mutually recursive ones.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item predefined functions: equality, booelan constructors,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski connectives, list constructors, head and tail list functions,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski arithmetic operations.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item non-recursive functions, including conditional,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilet and case expressions.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item use of incomplete patterns (HOLCF) and of wildcards in case
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item total primitive recursive functions (HOL)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiand partial recursive ones (HOLCF), including mutual ones (with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskirestrictions in the HOL case).
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item class and instance declarations.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item monad declarations and do notation.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe shallow embedding approach used by our translations should allow
30256573a343132354b122097b0ee1215dda1364Till Mossakowskito take as much advantage as possible of the automation currently
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiavailable on Isabelle, particularly in HOL.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFurther work should include extending the translation to cover the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhole of the Haskell Prelude. We hope that this will make it possible
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskito support the verification of functional robotics programs.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiA further extension, in line with the work on Programtica, would be
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe translation of P-logic. This translation, due to the character of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe P-logic typing system, could be more easily carried out relying on
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisome form of universal quantification on type variables, or else
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifurther relying on parametrisation.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\bibliographystyle{alpha}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\bibliography{case}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\end{document}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%Moreover, being such languages
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%as Haskell, ML and Miranda closely modelled on typed lambda-calculus,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski%their translations to specification formalisms, particularly to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%higher-order logics, turn out to be comparatively straighforward to be
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%defined in the main lines --- although not so to be carried out in
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%, due to the richness in syntax, the specific way evaluation is
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%implemented, as well as to issues associated with classes (Haskell),
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%overloading and side effects.
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%All functions are total in HOL. Partiality may be dealt with by
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%lifting types through the \emph{option} type constructor. HOL has an
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%implementation of recursive functions based on Tarski fixed-point
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%theorem. Defining a recursive function requires giving a specific
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski%measure and proving monotonicity about it.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% HOL has an implementation of recursive functions, based on Tarski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% fixed-point theorem. Their definition in general requires specific
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% measure to be given each time, for monotonicity to be proved.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% Moreover, partial functions are needed to programs that might not
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% terminate, but in HOL all functions are total. Partiality may be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% dealt with by lifting types through \emph{option}, a type
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder% constructor in HOL. This inevitably complicates case expressions.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder%There are different general approaches depending on the style of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%semantics. The expressiveness of the logical language may also make a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%big difference.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe Haskell classes Eq and Ord are translated to corresponding classes
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskideclared, respectively, in HsHOL.thy and HsHOLCF.thy. These classes
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifor the moment are taken to be absolutely generic ones (with empty
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederaxiomatisation).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{Isabelle-HOL}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiIsabelle-HOL as an implementation of classical higher-order logic
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedersupports the definition of datatypes and recursive functions.
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till MossakowskiHowever, it distinguishes between primitive recursion (keyword
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiemph{primrec}), in which termination is trivially guaranteed by
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidecrease in the complexity of a parameter, and recursion (keyword
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederemph{recdef}) for which an appropriate specific measure must be
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederprovided in order to get the termination proof to go through.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMoreover, HOL does not have a notion of undefined suitable for
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercomputations --- therefore all functions have to be total.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThis translation of recursive functions is restricted to total
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederprimitive recursive functions that are recursive in their first
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskidatatype argument. The Haskell definition should be a case expression
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederin which all the constructors are considered in their datatype
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskideclaration order, save for the use of a wildcard.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder%Wildcards cannot be used for constructor arguments.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder%Moreover, the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%case variable should not be used in the specific case expression (just
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski%replace it with the specific case pattern).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMutually recursive functions are allowed under additional
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskirestrictions. All the functions should be recursive in the same type,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe constructors should be listed in the same order in each of the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskicase expressions, and also the variable names in the case patterns are
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiexpected to be maintained.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe translation of mutually recursive functions $a \rightarrow b, \ldots a
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidefined, for each case pattern, as the product of the values
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedercorrespondingly taken by the original functions.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\subsection{Isabelle-HOLCF}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIsabelle-HOLCF is the implementation of the theory of computable
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifunctions on top of higher-order logic, relying on axiomatic classes.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIn comparison with HOL, the handling of partial functions is more
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskinatural, and the presence of the fixpoint operator allows for a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskigeneral treatment of recursive functions. However, types in HOLCF can
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederbe interpreted as pointed complete partial orders (pcpo), and this
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskirequires all standard types to be lifted.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIn the present translation, the type constructor \emph{lift} is used
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederto lift types, in association with the corresponding lifting function
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\emph{Def} and with the undefined value \emph{UU}. Datatypes are
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitranslated to domains --- complete with destructors from declaration.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe class \emph{pcpo} is added to the sort of each type variable.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiPartial recursive functions (defined by case expressions), including
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimutually recursive ones, are covered without any essential
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirestrictions, relying on the recdef package.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski as well as an
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederoperational, but is quite deep.