hs2isa.tex revision c4e48c487e8797c2a101d15b2fc542d2de4b2246
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{llncs}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\documentclass[a4paper,11pt]{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\textwidth 15.93cm
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\textheight 24cm
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\oddsidemargin 0.0cm
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\evensidemargin 0.0cm
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\topmargin 0.0cm
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\title{Translating Haskell to Isabelle}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\author{ Paolo Torrini\inst{1} \and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Christoph Lueth\inst{2}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Christian Maeder\inst{2}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Till Mossakowski\inst{2}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\institute{Verimag, {\tt Paolo.Torrini@imag.fr}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\and DFKI Lab Bremen, {\tt \{Christoph.Lueth,Christian.Maeder,Till.Mossakowski\}@dfki.de} }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% \date{\today}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{abstract}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski We present partial translations of Haskell programs to Isabelle that have
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski been implemented as part of the Heterogeneous Tool Set. The the target logic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski is Isabelle/HOLCF, and the translation is based on a shallow embedding
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski % The AWE package has been used to support a translation of monadic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski %operators based on theory morphisms.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{abstract}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Introduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAutomating translation from programming languages to the language of a generic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprover may provide useful support for the formal development and the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiverification of programs. It has been argued that functional languages can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimake the task of proving assertions about programs written in them easier,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiowing to the relative simplicity of their semantics
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Thompson92,Thompson95}. The idea of translating Haskell programs, came
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito us, more specifically, from an interest in the use of functional languages
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the specification of reactive systems. Haskell is a strongly typed, purely
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifunctional language with lazy evaluation, polymorphic types extended with type
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructor classes, and a syntax for side effects and pseudo-imperative code
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskibased on monadic operators \cite{HaskellRep}. Several languages based on
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell have been proposed for application to robotics \cite{phh99,Hudak2003}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn such languages, monadic constructors are extensively used to deal with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiside-effects. Isabelle is a generic theorem-prover implemented in SML
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisupporting several logics --- in particular, Isabelle/HOL is the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimplementation in Isabelle of classical higher-order logic based on simply
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskityped lambda calculus extended with axiomatic type classes. It provides
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisupport for reasoning about programming functions, both in terms of rich
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibraries and efficient automation. Isabelle/HOLCF \cite{holcf}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Paulson94isa,holcf} is Isabelle/HOL conservatively extended with the
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLogic of Computable Functions --- a formalisation of domain theory.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have implemented as functions of Hets translations of Haskell to
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF following an approach based on shallow embedding,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimapping Haskell types to Isabelle ones, therefore taking full
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiadvantage of Isabelle built-in type-checking. Hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{MossaTh,HetsUG,Hets} is an Haskell-based application designed to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisupport heterogeneous specification and the formal development of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprograms. It has an interface with Isabelle, and relies on
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiProgramatica \cite{Prog04} for parsing and static analysis of Haskell
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprograms. Programatica already includes a translation to
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF which, in contrast to ours, is based on an object-level
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimodelling of the type system \cite{Huff}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe paper is organised as follows: Section~\ref{sec:semantics} discusses
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe semantic background of the translation, while the subsequent sections
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare devoted to the translation of types, datatypes, classes and function
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidefinitions, respectively. Sect.~\ref{sec:ex} shows some example proof,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand Sect.~\ref{sec:conclusion} concludes the paper.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Section 2 gives some background, section 3 introduces the system, section 4
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%gives the sublanguages of Haskell that can be translated, in section 5 we
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%define the two translations.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%, in section 6 we sketch a denotational semantics
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%associated with the translation to Isabelle/HOLCF, in section 7 we show how translation
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%of monads is carried out with AWE.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Semantic Background of the Translation}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:semantics}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe firstly describe the subset of Haskell that we cover.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOur translation to Isabelle/HOLCF covers at present Booleans, integers, basic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructors (function, product, list, \emph{maybe}), equality,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisingle-parameter type classes (with some limitations), \emph{case} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{if} expressions, \emph{let} expressions without patterns, mutually
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirecursive data-types and functions.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%It relies on existing formalisations of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%lazy lists and \emph{maybe}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIt keeps into account partiality and laziness by
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifollowing, for the main lines, the denotational semantics of lazy evaluation
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigiven in \cite{winskel}. There are several limitations: \emph{Prelude} syntax
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis covered only partially; list comprehension, \emph{where} expressions and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{let} with patterns are not covered; further built-in types and type
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiclasses are not covered; imports are not allowed; constructor type classes are
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskinot covered at all --- and so for monadic types beyond list and \emph{maybe}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOf all these limitations, the only logically deep ones are those related to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiclasses --- all the other ones are just a matter of implementation.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor the translation, we have followed the informal description of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskioperational semantics given in the Haskell report \cite{HaskellRep},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand also consulted the complete static semantics for Haskell 98
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{journals/jfp/Faxen02}, as well as the (fragmentary) dynamic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisemantics \cite{oai:CiteSeerPSU:71374}. However, it should be noted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat there is no denotational semantics of Haskell! This also has
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibecome clear after a query that one of the authors has sent to the
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell mailing list \cite{HaskellMail05}. Hence, our translation to
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill MossakowskiIsabelle/HOLCF can be seen as the first denotational semantics given
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito a large subset of Haskell 98. This also means that there is no
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinotion of correctness of this translation, because it just
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{defines} the denotational semantics. Of course, an interesting
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiquestion is the coincidence of denotational and operational semantics.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHowever, this is beyond the scope of the paper.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%The base translation to Isabelle-HOL is more limited, insofar as it covers
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski%only total primitive recursive functions. A better semantics with respect to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%partiality could be obtained by lifting the type of function values with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\emph{option}, but this has not been pursued here. Still, \emph{option} has
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%been used to translate \emph{maybe}. On the other hand, laziness appears very
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%hard to be captured with Isabelle-HOL. It also seems hard to overcome the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%limitation to primitive recursion. Other limitations are similar to those
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%mentioned for the translation to Isabelle/HOLCF --- with the notable exception of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%\section{Translations in Hets}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski%The Haskell-to-Isabelle translation in Hets requires GHC, Programatica,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%Isabelle and AWE. The application is run by a command that takes as arguments
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski%a target logic and an Haskell program, given as a GHC source file. The latter
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%gets analysed and translated, the result of a successful run being an Isabelle
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%theory file in the target logic.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%The Hets internal representation of Haskell is similar to that of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%Programatica, whereas the internal representation of Isabelle is based on the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%ML definition of the Isabelle base logic, extended in order to allow for a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%simpler representation of Isabelle-HOL and Isabelle/HOLCF. Haskell programs and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%Isabelle theories are internally represented as Hets theories --- each of them
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%formed by a signature and a set of sentences, according to the theoretical
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%framework described in \cite{MossaTh}. Each translation, defined as
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski%composition of a signature translation with a translation of all sentences, is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%essentially a morphism from theories in the internal representation of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%source language to theories in the representation of the target language.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Translation of Types}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:types}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn Isabelle/HOL types are interpreted as sets (class \emph{type});
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifunctions are total and may not be computable. A non-primitive
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskirecursive function may require discharging proof obligations already
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiat the stage of definition --- in fact, a specific relation has to be
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskigiven for a function to be proved total. In Isabelle/HOLCF each type
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiis interpreted as a pointed complete partially ordered set (class
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\emph{pcpo}) i.e. a set with a partial order which has suprema of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$\omega$-chains and has a bottom. Isabelle's formalisation, based on
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiaxiomatic type classes \cite{Wenzel}, makes it possible to deal with
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicomplete partial orders in quite an abstract way. Functions are
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskigenerally partial and computability can be expressed in terms of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicontinuity. Recursion can be expressed in terms of least fixed-point
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskioperator, and so, in contrast with Isabelle/HOL, function definition
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidoes not depend on proofs. Nevertheless, proving theorems in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIsabelle/HOLCF may turn out to be comparatively hard. After being
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispared the need to discharge proof obligations at the definition
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskistage, one has to bear with assumptions on function continuity
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithroughout the proofs. A standard strategy is then to define as much
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias possible in Isabelle/HOL, using Isabelle/HOLCF type constructors to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilift types only when this is necessary.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe provision of pcpos, domains and continuous functions by
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIsabelle/HOLCF eases the translation of Haskell types and functions a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilot. However, special care is needed when trying to understand the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHaskell semantics. If one reads the section of the Haskell report
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidealing with types and classes, one could come to the conclusion that
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia function space in Haskell can be mapped to the space of the
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowskicontinuous functions in Isabelle/HOLCF --- this would correspond to a
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maederpurely lazy language. However, Haskell is a mixed eager and lazy
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilanguage, as it provides a function $seq$ that enforces eager
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskievaluation. This function is introduced in part 6 of the Haskell
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskireport, ``Predefined Types and Classes'', in section 6.2. We quote
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski However, the provision of $seq$ has important semantic consequences,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski because it is available at every type. As a consequence, $\bot$ is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski not the same as $\lambda x \rightarrow \bot$, since $seq$ can be
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski used to distinguish them.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIn order to enforce this distinction, each function space needs to be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilifted. The same holds for products. We define these liftings in a
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecific Isabelle/HOLCF theory \emph{HsHOLCF} (included in the Hets
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidistribution) as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidefaultsort pcpo
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidomain ('a,'b) lprod = lpair (lazy lfst :: 'a) (lazy lsnd :: 'b)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidomain 'a Lift = Lift (lazy 'a)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes ('a, 'b) "-->" = "('a -> 'b) Lift" (infixr 0)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski liftedApp :: "('a --> 'b) => ('a => 'b)" ("_$$_" [999,1000] 999)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* application *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski "liftedApp f x == case f of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Lift $ g => g $ x"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski liftedLam :: "('a => 'b) => ('a --> 'b)" (binder "Lam " 10)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* abstraction *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski "liftedLam f == Lift $ (LAM x . f x)"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOur translation of Haskell types to Isabelle types is defined
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirecursively. It is based on a translation of names for avoidance of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiname clashes that is not specified here. We write $\alpha'$ for both
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe recursive translation of item $\alpha$ and the renaming according
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskito the name translation. The translation of types is given by the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskifollowing rules:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\noindent Types
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski$$\begin{array}{ll}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski a & \Longrightarrow \ 'a::\{pcpo\} \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski () & \Longrightarrow \ unit \ \mbox{lift} \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Bool & \Longrightarrow \ bool \ \mbox{lift} \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Integer & \Longrightarrow \ int \ \mbox{lift} \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \tau_{1} \to \tau_{2} & \Longrightarrow
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \ \tau'_{1} \ \verb@-->@ \ \tau'_{2}) \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (\tau_{1},\tau_{2}) & \Longrightarrow
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \ (\tau'_{1} ~lprod~ \tau'_{2}) \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski {[\tau]} \ & \Longrightarrow \ \tau' \ llist \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiBuilt-in types are translated to the lifting of the corresponding HOL type.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe Isabelle/HOLCF type constructor \emph{lift} is used to lift types to flat
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidomains. The type constructor $llist$ is discussed in the next section.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Translation of Datatypes}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiAs explained in the Haskell report \cite{HaskellRep}, section 4.2.3,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe following four Haskell declarations
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski data D1 = D1 Int
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski data D2 = D2 !Int
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski newtype N = N Int
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskihave four different semantics. Indeed, the correct translation to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{verbatim}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskidomain D1 = D1 (lazy D1_1::"Int lift")
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskidomain D2 = D2 (D2_1::"Int lift")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes S = "Int lift"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskipcpodef N = "{x:: Int lift . True}"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\noindent In Isabelle/HOLCF, the keyword \emph{domain} defines a
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(possibly recursive) domain as solution of the corresponding domain
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiequation. The keyword \emph{lazy} ensures that the constructor $D1$ above
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis non-strict, i.e.\ $D1 \ \bot \ \neq \ \bot$. The keyword
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\emph{pcpodef} can be used to define sub-pcpos of existing pcpos;
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskihere, we use it just to introduce an isomorphic copy of an existing
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskipcpo --- this is the semantics of Haskell \emph{newtype} definitions.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski%Note that the constructor for N is Abs_N, the selector Rep_N.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiLists are translated to the domain \emph{llist}, defined as follows
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiin our prelude theory \emph{HsHOLCF}:
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{verbatim}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskidomain 'a llist = lNil | ### (lazy 'a) (lazy 'a llist)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{verbatim}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent allowing for partial list as well as for infinite ones \cite{holcf}.\\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor each datatype, we have to lift the constructors from the
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiHOLCF continuous function spaces to our lifted function spaces:
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski cont2lifted2 :: "('a -> 'b -> 'c) => ('a --> 'b --> 'c)"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski "cont2lifted2 f == Lam x . Lam y. f $ x $ y"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski llCons :: "'a --> 'a llist --> 'a llist"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski "llCons == cont2lifted2 (op ###)"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe general scheme for translation of mutually recursive lazy Haskell
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidatatypes to Isabelle/HOLCF domains is as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabbing}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$ data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j $ \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$ data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k \qquad \Longrightarrow $ \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$ \qquad $\=$ domain$\=$ \ \phi'_1 \ = \ $\=$ C'_{11} \ (lazy~ ::\ x'_1) \ \ldots \ (lazy~ :: \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\>\>\>$ \ \ldots \ | \ $\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\>\>\>$ C'_{1p} \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (lazy~ :: \ y'_1) \ \ldots \ (lazy~ :: \ y'_j) $\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\>$ and \ \ldots $\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\>$ and \ $\>$\phi'_n \ = \ C'_{n1} \ (lazy~ :: \ w'_1) \ \ldots \ (lazy~ :: \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski w'_h) \ | \ $\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\>\>\>$\ldots \ | $\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\>\>\>$\ C'_{nq} \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (lazy~ :: \ z'_1) \ \ldots \ (lazy~ :: \ z'_k) $\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiMutually recursive datatypes relies on specific Isabelle syntax
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(keyword \emph{and}).\footnote {Due to a bug in Isabelle/HOLCF 2005,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski declaration of mutually recursive lazy domains does not work.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski However, this will be fixed in Isabelle 2007; the fix currently is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski available in the development snapshot.} Order of declarations is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitaken care of. In case of strict arguments (indicated with ! in
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHaskell), the keyword \emph{lazy} is omitted.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe translation scheme for definitions of type synonyms is simply as follows:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$ type \ \tau \ = \ \tau_1 \quad \qquad \Longrightarrow \qquad
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ types \ \tau' \ = \ \tau'_1
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Translation of Kinds and Type Classes}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiType classes in Isabelle and Haskell associate a set of functions to a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitype class identifier (these functions are also called the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\emph{methods} of the class). In Isabelle, type classes are typically
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifurther specified using a set of axioms; for example, the class
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$\mathit{linorder}$ of total orders is specified using the usual total
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiorder axioms. Of course, such axiomatizations are not possible in
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHaskell. Indeed, in Haskell, there is no check that the class $Ord$
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiactually consists of total orders only, and hence it would be
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinappropriate to translate it to $\mathit{linorder}$ in Isabelle.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiInstead, we translate to a newly declared Isabelle class $Ord$. The
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskionly thing that we assume is that it is a subclass of $pcpo$, because
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiall Haskell types are translated to pcpos. Hence, type classes are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslated to Isabelle/HOLCF as subclasses of \emph{pcpo} with empty
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiaxiomatization. Methods declarations associated with Haskell classes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare translated to independent function declarations with appropriate
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiclass annotation on type variables.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiClass instance declarations declare that a particular type belongs to
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskia class. In Isabelle, instance declarations generate proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiobligations, namely that the methods for the type at hand indeed
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisatisfy the axioms of the class. Since our translation only generates
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiclasses without axioms (beyond those of $pcpo$), proofs are trivial
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiand proof obligation may be automatically discharged.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiA Haskell class instance declaration that declares type $T$
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskito belong to class $C$ may define the behaviour of $C$'s
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiclass methods for $T$. The same is possible with
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskinormal Isabelle constant definitions, if the type of the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiconstant (function) is specialised to $T$ in the definition.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiWith this, we avoid an explicit handling of dictionaries, as
c5e63ec138b908ac9d15e6843120033bf36a1862Till Mossakowskidescribed in the static semantics of Haskell \cite{journals/jfp/Faxen02}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski%Not all the problems have been solved with
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski%respect to arities that may conflict in Isabelle, although they correspond to
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski%compatible Haskell instantiations.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiA restriction of Isabelle is that it does neither allow for
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskimulti-parameter classes, nor for type constructor ones. Therefore, the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisame restrictions apply to our translation.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent Classes
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski$$\begin{array}{l}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski K \quad \Longrightarrow \quad K'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Type schemas
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$$\begin{array}{ll}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ (ctx \Rightarrow \tau)'
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ [(v'::s) / (v'::({K'} \cup s))] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \{ \ \} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{array}$$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell type variables are translated to variables of class
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{pcpo}. Each type is associated to a sort in Isabelle (in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell, the same concept is called ``kind''), defined by the set of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe classes of which it is member.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Class declarations
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \Longrightarrow \ class \ K' \ \subseteq
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ pcpo; \ Dec'_1; \ \ldots; \ Dec'_n \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Class instance definitions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{l}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad \qquad \qquad \qquad \qquad
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad \qquad \qquad \qquad \Longrightarrow \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad instance \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \in ctx\}, \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad \quad \quad \ldots, \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad \quad \quad
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \mbox{proof \ obligation}; \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad defs \ f'_{\tau 1} :: (ctx \Rightarrow \tau_1)' = t'_1; \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad \qquad \ldots; \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad f'_{\tau n} :: (ctx \Rightarrow \tau_n)' = t'_n
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{array}$$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Translation of Function Definitions and Terms}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTerms of built-in type are translated using Isabelle/HOLCF-defined lifting function
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{Def}. The bottom element $\bot$ is used for undefined terms.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF-defined $\mathit{flift1} :: \ ('a \Rightarrow \ 'b::pcpo) \Rightarrow ('a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\ \mathit{lift} \to \ 'b)$ and $\mathit{flift2} :: \ ('a \Rightarrow \ 'b) \Rightarrow ('a \ \mathit{lift}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\mathit{lift})$ are used to lift operators, as well as the following, defined in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\emph{HsHOLCF}.\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilliftbin :: "('a::type => 'b::type => 'c::type) =>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ('a lift --> 'b lift --> 'c lift)"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski"lliftbin f == cont2lifted2 (flift1 (%x. flift2 (f x)))"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent Boolean values are translated to values of \emph{bool lift}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(\emph{tr} in Isabelle/HOLCF) i.e. \emph{TT}, \emph{FF} and $\bot$, and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBoolean connectives to the corresponding Isabelle/HOLCF operators.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiIsabelle/HOLCF-defined \emph{If then else fi} and \emph{case} syntax are used
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskito translate conditional and case expressions, respectively. There are
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirestrictions, however, on case expressions, due to limitations in the
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskitranslation of patterns; in particular, only simple patterns are allowed (no
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskinested ones). On the other hand, Isabelle sensitiveness to the order of
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskipatterns in case expressions is dealt with. Multiple function definitions are
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskitranslated as definitions based on case expressions. In function definitions
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskias well as in case expressions, both wildcards --- not available in Isabelle
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski--- and incomplete patterns --- not allowed --- are dealt with by elimination,
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski$\bot$ being used as default value in the latter. Only let expressions
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiwithout patterns on the left are dealt with; guarded expressions are
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskitranslated as conditional ones; where expressions and list comprehension are
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski$$\begin{array}{l}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski f :: \phi \qquad \quad \Longrightarrow \qquad
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \ consts \ f' \ :: \ \phi' \\
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \quad \Longrightarrow \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \overline{x}_1 \to \ t_1); \
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \qquad \quad
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski defs \ f' :: \phi' \ = \ Lam \ \overline{x}'. \ t' \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (f_1 \ \overline{v_1} \ = \ t_1; \ \ldots;
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowski \ f_n \ \overline{v_n} \ = \ t_n) \qquad \Longrightarrow \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \qquad fixrec \ f'_1 :: \phi'_1 \ =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ (Lam \ \overline{v_1}'. \ t'_1) \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad \quad and \ \ldots \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \quad and \ f'_n :: \phi'_n \ =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ (Lam \ \overline{v_n}'. \ t'_n) \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \qquad \mbox{with} \ f_1::\phi_1, \ldots, f_n::\phi_n \
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \mbox{mutually \ recursive} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{array}$$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFunction declarations use Isabelle keyword \emph{consts}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNon-recursive definitions are translated to standard definitions using
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIsabelle keyword \emph{defs}. Recursive definitions rely on
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF package \emph{fixrec} which provides nice syntax for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifixed point definitions, including mutual recursion. Lambda
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiabstraction is translated as continuous abstraction for lifted
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifunction spaces (\emph{Lam}), function application as continuous
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiapplication (the \emph{\$\$} operator), see Sect.~\ref{sec:types}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\section{Example Proof}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:ex}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWe illustrate our translation with a sample proof about the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicompatibility of map and composition.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe Haskell declarations
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicomp :: (b -> c) -> (a -> b) -> a -> c
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicomp f g x = f (g x)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimap1 :: (a -> b) -> [a] -> [b]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskimap1 f [] = []
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskimap1 f (x:xs) = f x : map1 f xs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare translated to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiX_comp :: "('b --> 'c) --> ('a --> 'b) --> 'a --> 'c"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskimap1 :: "('a --> 'b) --> 'a llist --> 'b llist"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski"(X_comp :: ('b --> 'c) --> ('a --> 'b) --> 'a --> 'c) ==
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Lam f. Lam g. Lam x. f $$ (g $$ x)"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifixrec "(map1 :: ('a --> 'b) --> 'a llist --> 'b llist) =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (Lam qX1. (Lam qX2. case qX2 of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski lNil => lNil |
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski op ### $ pX1 $ pX2 =>
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski llCons $$ (qX1 $$ pX1) $$ (map1 $$ qX1 $$ pX2)))"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe fixrec definition leads to a bunch of theorems, one for simplification.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHowever, the latter makes the Isabelle simplifier loop, and hence needs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito be replaced with a more suitable simplification theorem:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilemmas map1_simps [simp del]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilemma map1_simp : "map1 $$ (f::('a --> 'b)) $$ (x::'a llist) =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (case x of lNil => lNil |
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski op ### $ pX1 $ pX2 =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski llCons $$ (f$$pX1)$$ (map1$$f$$pX2))"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski apply (subst map1_simps)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDue to the recursion, this theorem cannot be fed into the simplifier either.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHowever, using substitution, it helps in proving the following
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiexpected lemmas about the behaviour of $map1$:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilemma map1_UU [simp] : "map1 $$ f $$ UU = UU"
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski apply (subst map1_simp)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilemma map1_lNil[simp] : " map1 $$ f $$ lNil = lNil"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski apply (subst map1_simp)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilemma map1_cons1[simp] :
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski "map1 $$ f $$ (op ### $ x $ (xs::'a llist)) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski op ### $ (f $$ x) $ (map1 $$ f $$ xs)"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski apply (subst map1_simp)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski apply (simp add: cont2lifted2_def)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent With these, it is now easy to prove, via induction, that map
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidistributes over composition:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheorem compMap :
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski "X_comp $$ (map1 $$ f) $$ (map1 $$ g) $$ x =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski map1 $$ (X_comp $$ f $$ g) $$ x"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski apply (auto simp add: X_comp_def)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIsabelle/HOLCF also provides a coinduction method for recursive
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Conclusion and Related Work}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:conclusion}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe provide a shallow embedding of Haskell to Isabelle/HOLCF, which can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibe used for proving properties of Haskell programs. This translation
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskialso is the first denotational semantics that has been given to
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe main advantage of our shallow approach is to get as much as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipossible out of the automation currently available in Isabelle,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiespecially with respect to type checking. Isabelle/HOLCF in particular
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprovides with an expressive semantics covering lazy evaluation, as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as with a smart syntax --- also thanks to the \emph{fixrec}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipackage. It is interesting to note that Haskell functions and product
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitypes have to be lifted due to the mixture of eager and lazy evaluation
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat Haskell exhibits due to the presence of the $seq$ function.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiType classes in Haskell are similar enough to Isabelle's type classes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisuch that explicit handling of dictionaries can be avoided.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe main disadvantage of our approach is the lack of type
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructor classes. Anyway, it is possible to get around the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiobstacle, at least partially, by relying on an axiomatic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicharacterisation of monads and on a proof-reuse strategy that actually
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiminimises the need for interactive proofs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiConcerning related work, although there have been translations of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifunctional languages to first-order systems --- those to FOL of
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMiranda \cite{Thompson95,Thompson89,Thompson95b} and Haskell
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Thompson92}, both based on large-step operational semantics;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat of Haskell to Agda implementation of Martin-Loef type theory in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Abel} --- still, higher-order logic may be quite helpful in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiorder to deal with features such as currying and polymorphism.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMoreover, higher-order approaches may rely on denotational semantics
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski--- as for examples, \cite{Huff} translating Haskell to HOLCF, and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Pollack} translating ML to HOL --- allowing for program
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirepresentation closer to specification as well as for proofs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicomparatively more abstract and general.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe translation of Haskell to Isabelle/HOLCF proposed in \cite{Huff}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiuses deep embedding to deal with types. Haskell types are translated
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito terms, relying on a domain-theoretic modelling of the type system
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiat the object level, allowing explicitly for a clear semantics, and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproviding for an implementation that can capture most features,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiincluding type constructor classes. In contrast, we provide in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicase of Isabelle/HOLCF with a translation that follows the lines of a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotational semantics under the assumption that type constructors and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitype application in Haskell can be mapped to corresponding
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructors and built-in application in Isabelle without loss from
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe point of view of behavioural equivalence between programs --- in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiparticular, translating Haskell datatypes to Isabelle ones. Our
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisolution gives in general less expressiveness than the deeper approach
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski--- however, when we can get it to deal with cases of interest, it
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimight make proofs easier.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%On the other hand, the main novelty in our work is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%to rely on theory morphisms and on their implementation for Isabelle in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%package AWE \cite{AWE}, in order to deal with special cases of monadic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% Currently Hets provides with an extension of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%base translation to Isabelle/HOL which uses AWE and covers state monad types
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%inclusive of \emph{do} notation. Due to present limitations of AWE, this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%solution is available only for Isabelle/HOL at the moment, although in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%principle it could work for Isabelle/HOLCF as well.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFuture work should use this framework for proving properties of
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell programs. Currently Hets already provides some experimental
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslation of constructor classes and monads, also covering \emph{do}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinotation, using theory morphisms as provided by the package AWE
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{AWE}. However, there are (mainly syntactic) problems (with name
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiclashes) that currently prevent a proper integration with
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF. These problems should be solved in the near future.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor monadic programs, we are also planning to use the monad-based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidynamic Hoare and dynamic logic that already have been formalised in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle \cite{Walter05}. Our translation tool from Haskell to
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle is part of the Heterogeneous Tool Set Hets and can be
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidownloaded from \texttt{http://www.dfki.de/sks/hets}. More details
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiabout the translations can be found in \cite{Tlmm}.
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\subsection*{Acknowledgment}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis work has been supported by the {\em Deutsche
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Forschungsgemeinschaft} under grants KR \mbox{1191/5-2} and \mbox{KR
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski 1191/7-2 }. We thank Brian Huffmann for help with the Isabelle/HOLCF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipackage and Erwin R. Catesbeiana for pointing out an inconsistency.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\bibliographystyle{alpha} \bibliography{case}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{HOL}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe translation $\omega_s \ :: \ H_s \ \to \ HOL$ from programs in $H_s$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito theories in Isabelle/HOL extended with AWE can be defined with the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifollowing set of rules.\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Types
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski () & \Longrightarrow \ unit \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski a & \Longrightarrow \ 'a::\{type\} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Bool & \Longrightarrow \ boolean \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Integer & \Longrightarrow \ int \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \tau_{1} \to \tau_{2} & \Longrightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ \tau'_{1} \ \Rightarrow \ \tau'_{2} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (\tau_{1},\tau_{2}) & \Longrightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ (\tau'_{1} * \tau'_{2}) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {[\tau]} \ & \Longrightarrow \ \tau' \ list \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Maybe \ \tau & \Longrightarrow \ \tau' \ option \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Classes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Eq & \Longrightarrow \ Eq \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski K & \Longrightarrow \ K'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Type schemas
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ (ctx \Rightarrow \tau)'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ [(v'::s) / (v'::({K'} \cup s))] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{array}$$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere we highlight the main differences the translation to Isabelle/HOLCF and this,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisemantically rather more approximative one to Isabelle/HOL (thereafter simply
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHOL). Function type, product and list are used to translate the corresponding
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell constructors. Option types are used to translate \emph{Maybe}. Haskell
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidatatypes are translated to HOL datatypes. Type variables are of class
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiStandard lambda-abstraction ($\lambda $) and function application are used
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihere, instead of continuous ones. Non-recursive definitions are treated in an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianalogous way as in the translation to Isabelle/HOLCF. However, partial functions and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiparticularly case expressions with incomplete patterns are not allowed.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn HOL one has to pay attention to the distinction between \emph{primitive
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski recursive} functions (introduced by the keyword \emph{primrec}) and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigenerally recursive ones. Termination is guaranteed for each primitive
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirecursive function by the fact that recursion is based on the datatype
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructure of one of the parameters. In contrast, termination is no trivial
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimatter for recursion in general. A strictly decreasing measure needs to be
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassociation with the parameters. This cannot be dealt with automatically in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigeneral. Therefore here we restrict translation to primitive recursive
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMutual primitive recursion is allowed for under additional restrictions ---
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimore precisely, given a set $F$ of functions: 1) all the functions in $F$ are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirecursive in the first argument; 2) all recursive arguments in $F$ are of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisame type modulo variable renaming; 3) each type variable occurring in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitype of a function in $F$ already occurs in the type of the first argument.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe third conditions is a way to ensure that we do not end up with type
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskivariables which occurs on the right hand-side but not on the left hand-side of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskia definition. In fact, given mutually recursive functions $f_{1}, \ldots,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskif_{n}$ of type $A \rightarrow B_{1}, \ldots, A \rightarrow B_{n}$ after
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskivariable renaming, they are translated to projections of a new function of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitype $A \rightarrow (B_{1} * \ldots * B_{n})$ which is defined for cases of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiexpression $nth_n \ t$ used in the translation rule is simply an informal
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiabbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiextracts the $n$-th projection from a tuple no shorter than $n$.\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent Terms
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski x::\tau & \Longrightarrow \ x'::\tau' \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski () & \Longrightarrow \ () \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski True & \Longrightarrow \ True \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski False & \Longrightarrow \ False \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \&\& & \Longrightarrow \ \& \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski || & \Longrightarrow \ | \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski not & \Longrightarrow \ Not \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski c & \Longrightarrow \ c \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ t \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski negate \ x & \Longrightarrow \ - x \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski {[]} & \Longrightarrow \ {[]} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski t:ts & \Longrightarrow \ t'\#ts' \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski head & \Longrightarrow \ hd \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski tail & \Longrightarrow \ tl \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski == & \Longrightarrow \ hEq \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski /= & \Longrightarrow \ hNEq \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Just & \Longrightarrow \ Some \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Nothing & \Longrightarrow \ None \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski return & \Longrightarrow \ return \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski bind & \Longrightarrow \ mbind \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski C & \Longrightarrow \ C' \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski f & \Longrightarrow \ f' \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \backslash \overline{x} \ \to \ t & \Longrightarrow
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ \lambda \ \overline{x}'. \ t' \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski t_1 \ t_2 & \Longrightarrow \ t'_1 \ t'_2 \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fst & \Longrightarrow \ fst \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski snd & \Longrightarrow \ snd \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski let \ (x_1 = t_1; & \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \dots; & \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \qquad x_n = t_n) \quad in \ t & \Longrightarrow
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \ if \ t' \ then \ t'_1 \ else \ t'_2 \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski case \ x \ of \ (p_1 \to t_1; \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \qquad \qquad \ldots; & \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \qquad \qquad p_n \to t_n) & \Longrightarrow
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \Rightarrow t'_n \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \mbox{is \ a \ complete \ match} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \Rightarrow t'_{n-1} \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski p'_{n-1}, q_1, \ldots, q_k \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & \qquad \mbox{complete \ match}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{array}$$\\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent Declarations
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \Longrightarrow \ class \ K' \ \subseteq
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \ type; \ Dec'_1; \ \ldots; \ Dec'_n \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \ consts \ f' \ :: \ \phi' \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \ type \ \tau \ = \ \tau'_1 \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad datatype \ \phi'_1 \ = \ C'_{11} \ x'_1 \ \ldots \ x'_i \ | \ \ldots
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ | \ C'_{1p}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ y'_1 \ \ldots \ y'_j \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad and \ \ldots \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad and \ \phi'_n \ = \ C'_{n1} \ w'_1 \ \ldots \ w'_h \ | \ \ldots \ | \
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \ z'_1 \ \ldots \ z'_k \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\noindent Definitions
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \overline{x}_1 \to \ t_1); \
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski == \ \lambda \ \overline{x}'. \ t' \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski f_1 \ \ y_1 \ \overline{x_1} \ =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ t_1; \ \ldots; \ f_n \ y_n \
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \overline{x_n} \ = \ t_n \ \Longrightarrow \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \qquad decl \ f_{new} ::
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (\sigma_1(ctx_1) \ \cup \ \ldots \ \cup \ \sigma_n(ctx_n)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ \Rightarrow \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \qquad \qquad \sigma_1(\tau_{1a}) \ \to \
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (\sigma_1(\tau_1), \ldots, \sigma_n(\tau_n)))' \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad primrec \ f_{new} \ sp_1 \ =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ (\lambda \ \overline{x_1}'. \ t'_1 [y'_1/sp_1], \ldots, \ \lambda \
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \overline{x_n}'. t'_n [y'_n/sp_1]); \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \qquad \ldots; \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \qquad
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski f_{new} \ sp_k \ = \ (\lambda \ \overline{x_1}'. \ t'_1
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [y'_1/sp_k], \ldots,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ \lambda \ \overline{x_n}'. \ t'_n [y'_n/sp_k]); \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad defs \ f_1 \ x \ == \ nth_1 \ (f_{new} \ x); \ \ldots;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ f_n \ x \ == \ nth_n \ (f_{new} \ x) \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad \mbox{with} \ f_1:: (ctx_1 \Rightarrow \tau_{1a} \to \tau_1),
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \ \ldots, \ f_n::(ctx_n \Rightarrow \tau_{na} \to \tau_n) \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad \mbox{mutually \ recursive} \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ \Longrightarrow \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad instance \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \in ctx\}, \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \qquad \quad \quad
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ldots, \ \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \mbox{with \ proof \ obligation}; \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad defs \quad
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (ctx \Rightarrow \tau_n)' == t'_n\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski instance \ Monad \ \tau \ where \
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (def_{eta}; def_{bind}) \ \Longrightarrow \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad defs \quad def'_{eta}; \ def'_{bind}; \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad t\_instantiate \ Monad \ mapping \ m\_\tau' \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \qquad \mbox{where} \ m_\tau' \ \mbox{is \ defined \ as \
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski theory \ morphism \ associating} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \mbox{to} \ tau', \ def'_{eta}, \ def'_{bind} \
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \mbox{respectively;}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\end{array}$$\\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiType classes are translated to subclasses of \emph{type}. An axiomatisation of
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiHaskell equality for total functions can be found in \emph{HsHOL}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{ll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski heq :: & 'a \ \to \ 'a \ \to \ bool \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski hneq :: & 'a \ \to \ 'a \ \to \ bool \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$axclass \ Eq \ < \ type$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$eqAx: heq \ p \ q \ = \ Not \ (hneq \ p \ q)$\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiGiven the restriction to total functions, equality on built-in types can be
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidefined as HOL equality.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Semantics (for HOLCF)}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDenotational semantics con be given as basis for the translation to Isabelle/HOLCF.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiEssentially, the claim here is that the expressions on the left hand-side of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe following tables represent the denotational meaning of the Haskell
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiexpressions on the right hand-side, as well as of the Isabelle/HOLCF expressions to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiwhich they are translated. The language on the left hand-side is still based
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskion Isabelle/HOLCF where type have been extended with abstraction ($\Lambda$) and fixed
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowskipoint ($\mu$) in order to represent the denotational meaning of domain
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowskideclarations.\\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{ll}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \lceil a \rceil & = \ 'a::pcpo \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil () \rceil & = \ unit \ lift \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil Bool \rceil & = \ bool \ lift \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil Integer \rceil & = \ int \ lift \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil \to \rceil & = \ \to \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil (,) \rceil & = \ * \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil [] \rceil & = \ seq \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil Maybe \rceil & = \ maybe \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil T_1 \ T_2 \rceil & = \ \lceil T_1 \rceil \ \lceil T_2 \rceil \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% \lceil TC \rceil & = & \mu X. (\Lambda \ v_1, \ldots, v_n.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% \ \lceil \tau_1 \rceil + \ldots + \lceil \tau_{k} \rceil)[X/TC] \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% \mbox{when \ there \ is \ a \ declaration} \ data \ TC \ v_1 \ \ldots \ v_n
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% \ = \ C_1::\tau_1 | \ldots |
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% C_k::\tau_k \\
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski \lceil TC_{i} \rceil & = \ let \ F \ = \ \mu \ (X_1*\ldots*X_k). \\
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski & \quad ((\Lambda \ v_{11}, \ldots, v_{1m}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ \lceil \tau_{11} \rceil + \ldots + \lceil \tau_{1p} \rceil),
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & \quad (\Lambda \ v_{k1}, \ldots, v_{kn}. \ \ldots,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ \lceil \tau_{k1} \rceil + \ldots + \lceil \tau_{kq} \rceil))
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski & in \ nth_i(F) \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \quad \mbox{with} \ 0 < i \leq k, & \mbox{when} \ data \ TC_1 \ v_{11} \ \ldots \ v_{1m} \ = \ C_{11}::\tau_{11}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | \ldots | C_{1p}::\tau_{1p}; \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & \quad \ldots; \ data \ TC_k \ v_{k1} \ \ldots \ v_{kn} \ =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ C_{k1}::\tau_{k1} | \ldots |
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski C_{kq}::\tau_{kq} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \mbox{are \ mutually \ recursive \ declarations} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{array}$$\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe representation of term denotation is similar to what we get from the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitranslation, except that for functions we give the representation of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimeaning of \emph{fixrec} definitions ($FIX$ is the Isabelle/HOLCF fixed point
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \lceil x::a \rceil & = \ x'::\lceil a \rceil \\
a231094086321e19f9a689de4745512c91e00e4bTill Mossakowski \lceil c \rceil & = \ c' \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \lceil \backslash x \ \to \ f \rceil & = \ LAM \ x_{t}. \ \lceil f \rceil \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \lceil (a,b) \rceil & = \ (\lceil a \rceil, \lceil b \rceil) \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil t_1 \ t_2 \rceil & = \ \lceil t_1 \rceil \ \cdot \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \lceil t_2 \rceil \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & = \ let \ \lceil
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \lceil f_i \rceil & = \ let \ g \ =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski FIX \ (x_1,\ldots,x_n). \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (\lceil t_1 \rceil, \ldots, \lceil t_{n} \rceil [f_1/x_1,\ldots,f_n/x_n] \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & in \ nth_i (g) \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \quad \mbox{with} \ 0 < i \leq n,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & \mbox{where} \ f_1 = t_1, \ f_n = t_n \ \mbox{are \ mutually \ recursive
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \ definitions}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% \ldots \lceil a_{n} \rceil \ TyCons_{t}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\section{Monads with AWE}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiA monad is a type constructor with two operations that can be specified
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiaxiomatically --- \emph{eta} (injective) and \emph{bind} (associative, with
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\emph{eta} as left and right unit) \cite{moggi89}. Isabelle does not have
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitype constructor classes, therefore monads cannot be translated directly. The
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiindirect solution that we are pursuing, is to translate monadic types as types
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithat satisfy the monadic axioms. This solution can be expressed in terms of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitheory morphisms --- maps between theories, associating signatures to
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskisignatures and axioms to theorems in ways that preserve operations and
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiarities, entailing the definition of maps between theorems. Theory morphisms
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiallow for theorems to be moved between theories by translating their proof
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiterms, making it possible to implement parametrisation at the theory level
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski(see \cite{AWE} for details). A \emph{parameterised theory} $\mathit{Th}$ has
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskia sub-theory $\mathit{Th}_P$ which is the parameter --- this may contain
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiaxioms, constants and type declarations. Building a theory morphism from
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$\mathit{Th}_P$ to a theory $I$ provides the instantiation of the parameter
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwith $I$, and makes it possible to translate the proofs made in the abstract
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskisetting of $\mathit{Th}$ to the concrete setting of $I$ --- the result being
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskian extension of $I$. AWE is an extension of Isabelle that can assist in the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiconstruction of theory morphisms \cite{AWE}.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiA notion of monad \cite{AWE2} can be built in AWE by defining, on an abstract
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilevel, a hierarchy of theories culminating in \emph{Monad}, based on the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskideclaration of a unary type constructor $M$ (in \emph{MonadType}) with the two
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimonad operations (contained in \emph{MonadOpEta} and \emph{MonadOpBind},
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskirespectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskispecific type constructor forms a monad, we have to construct a theory
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimorphism from \emph{MonadAxms} to the specific theory; this involves giving
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskispecific definitions of the operators, as well as discharging proof
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiobligations associated with specific instances of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithe axioms. The following gives an example. \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $data \ LS \ a \ = \ N \ | \ C \ a \ (LS \ a)$
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $instance \ Monad \ LS \ where$
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{ll}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski return \ x & = \ C \ x \ N \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski x \ >>= \ f & = \ case \ x \ of \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & N \ \to \ N \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & C \ a \ b \ \to \ cnc \ (f \ a) \ (b \ >>= \ f)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$cnc :: \ LS \ a \ \to \ LS \ a \ \to \ LS \ a $
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{ll}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskicnc \ x \ y & = \ case \ x \ of \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & N \ \to \ y \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & C \ w \ z \ \to \ cnc \ z \ (C \ w \ y)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent These definitions are plainly translated to HOL, as follows. Note
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithat these are not overloaded definitions. \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent $datatype \ 'a \ LS \ = \ N \ | \ C \ 'a \ ('a \ LS)$
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $consts $
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{ll}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski return\_LS & :: \ 'a \ \Rightarrow 'a \ LS \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski mbind\_LS & :: \ 'a \ LS \ \Rightarrow \ ('a \ \Rightarrow \ 'b \ LS) \
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \Rightarrow \ 'b \ LS \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski cnc & :: \ 'a \ LS \ \Rightarrow \ 'a \ LS \ \Rightarrow \ 'a \ LS \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $defs $
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{l}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskireturn\_LS\_def : \ return\_LS:: \ ('a \ LS \ \Rightarrow 'a) \ == \
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \lambda x. \ C \ x \ N
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $primrec $
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{ll}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimbind\_LS \ N & = \ \lambda f. \ N \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimbind\_LS \ (C \ pX1 \ pX2) & = \ \lambda f. \ cnc \ (f \ pX1) \ (mbind\_LS \ pX2 \ f)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $primrec $
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{ll}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskicnc \ N & = \ \lambda b. \ b \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskicnc \ (C \ pX1 \ pX2) & = \ \lambda b. \ cnc \ pX2 \ (C \ pX1 \ b)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent In order to build up the instantiation of \textit{LS} as a monad,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskihere it is defined the morphism $m\_LS$ from \emph{MonadType} to the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiinstantiating theory \emph{Tx}, by associating $M$ to $LS$.\\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$thymorph \ m\_LS : \ MonadType \ \longrightarrow \ Tx $
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{l}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski maps \ [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski renames: \ [(MonadOpEta.eta \mapsto return\_LS),
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (MonadOpBind.bind \mapsto mbind\_LS)] \\
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiRenaming is used in order to avoid name clashes in case of more than one
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimonads --- here again, note the difference with overloading. Morphism
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\emph{m\_LS} is then used to instantiate the parameterised theory
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\emph{MonadOps}.\\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $t\_instantiate \ MonadOps \ mapping \ m\_LS$ \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent This instantiation gives the declaration of the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiinstantiated methods, which may now be defined.\\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent $defs $
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{l}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiLS\_eta\_def: \ LS\_eta \ == \ return\_LS \\
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiLS\_bind\_def: \ LS\_bind \ == \ mbind\_LS
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\noindent In order to construct a mapping from \emph{MonadAxms} to
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskicase, by straightforward simplification). The translation will print out
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\emph{sorry} instead.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski$$\begin{array}{ll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskilemma \ LS\_lunit : & LS\_bind \ (LS\_eta \ x) \ t \ = \ t \ x \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskilemma \ LS\_runit : & LS\_bind \ (t:: \ 'a \ LS) \ LS\_eta \ = \ t \\
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskilemma \ LS\_assoc : & LS\_bind \ (LS\_bind \ (s:: \ 'a \ LS) \ t) \ u \ = \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & LS\_bind \ s \ (\lambda x. \ LS\_bind \ (t \ x) \ u) \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilemma \ LS\_eta\_inj : & LS\_eta \ x \ = \ LS\_eta \ y \ \Longrightarrow \ x \ = \ y
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Now, the morphism from \emph{MonadAxms} to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{Tx} can be built, and then used to instantiate \emph{Monad}. This gives
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiautomatically access to the theorems proven in \emph{Monad} and, modulo
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirenaming, the monadic syntax which is defined there. \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$thymorph \ mon\_LS : \ MonadAxms \ \longrightarrow \ Tx $
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski maps & [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & [(MonadOpEta.eta \ \mapsto \ Tx.LS\_eta), \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & (MonadOpBind.bind \ \mapsto \ Tx.LS\_bind)]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$t\_instantiate \ Monad \ mapping \ mon\_LS$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$renames: \ [ \ldots ]$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent The \emph{Monad} theory allows for the characterisation of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisingle parameter operators. In order to cover other monadic operators, a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipossibility is to build similar theories for type constructors of fixed arity.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAn approach altogether similar to the one shown for HOL could be used, in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprinciple, for Isabelle/HOLCF as well.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{comment}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere is a simple example. \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $ fn3 \ :: \ AC \ a \ b \to (a \to a) \to AC \ a \ b $
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifn3 \ k \ f & = \ case \ k \ of \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & Ct \ x \to Ct \ (f \ x) \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & Rt \ x \ y \to Rt \ (fn4 \ x) \ y \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent $ fn4 \ :: \ AC \ a \ b \to AC \ a \ b $
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifn4 \ k & = \ case \ k \ of \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & Rt \ x \ y \to Rt \ (fn3 \ x \ (\backslash z \to z)) \ y \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & Ct \ x \to Ct \ x \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent It translates to HOL as follows.\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $consts$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll} fn3 \ :: & ('a, 'b) \ AC \Rightarrow ('a \Rightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski 'a) \Rightarrow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ ('a, 'b) \ AC \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fn4 \ :: & ('a, 'b) \ AC \Rightarrow
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ ('a, 'b) \ AC \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fn3\_Xfn4\_X :: & ('a, 'b) \ AC \Rightarrow
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ (('a \Rightarrow 'a) \Rightarrow \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & ('a, 'b) \ AC) *
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \ (('a \Rightarrow 'a) \Rightarrow
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ ('a, 'b) \ AC) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent $defs$
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$$\begin{array}{lll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifn3\_def : & fn3 \ == \ \lambda k \ f. \ fst \ (( fn3\_Xfn4\_X :: \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & \ ('a, 'b) \ AC \Rightarrow (('a \Rightarrow 'a) \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & \Rightarrow ('a, 'b) \ AC) * ((unit \Rightarrow unit) \Rightarrow \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & ('a, 'b) \ AC) ) \ k) \ f \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fn4\_def : & fn4 \ == \ \lambda k \ f. \ snd \ (( fn3\_Xfn4\_X :: \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & ('a, 'b) \ AC \Rightarrow \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) * \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) ) \ k) \ f \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent $primrec$
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$\begin{array}{lll}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifn3\_Xfn4\_X & (Ct \ pX1) \ = & (\lambda f. \ Ct \ (f \ pX1), \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & & \lambda f. \ Ct \ pX1) \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifn3\_Xfn4\_X & (Rt \ pX1 \ pX2) & = \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & (\lambda f. \ Rt \ (snd & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2, \\
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowski & \lambda f. \ Rt \ (fst & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2) \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiIn the following, we give a definition of the sub-language of Haskell
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$H_c$ that is covered by the translation to Isabelle/HOLCF.\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent Types
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowski$$\begin{array}{lll}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \tau \ = () \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & Integer & \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & v & \mbox{type \ variable}\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & \tau_1 \to \tau_2 & \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & (\tau_1,\tau_2) & \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% & Either \ tau_1 \ tau_2 \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & [\tau] & \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & Maybe \ \tau & \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & T \ \tau_{1} \ \ldots \tau_{n} & \mbox{either \ datatype \ or \
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski defined \ type}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% & T \ \tau_{1} \ \ldots \ \tau_{n} \qquad \mbox{defined \ type}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent Type classes
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{lll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski K \ = & Eq & \mbox{with \ default \ methods} \ ==, \ /= \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & K & \mbox{defined \ type \ class} \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent Contexts
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{lll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski ctx \ = & \{K \ v\} \ \cup \ ctx & \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & \{\} & \mbox{empty \ context} \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent Type schemas
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$\begin{array}{ll}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \phi \ = & ctx \Rightarrow \tau \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & \qquad \mbox{where \ all \ variables \ in} \ ctx \ \mbox{are \ in} \ \tau
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent Simple patterns
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{lll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski sp \ = & \_ & \mbox{wildcard} \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & v & \mbox{variable \ of \ datatype}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & C \ \overline{v} & \mbox{case \ of \ datatype}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\noindent Terms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{lll} t \ =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & c \in \aleph & \mbox{Integer \ constant} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & t \in \{:,head,tail\} & \mbox{on list} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & t \in \{Just,Nothing\} & \mbox{on \ \emph{maybe} \ types} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & t \in \{fst,snd\} & \mbox{on \ pairs} \\