hs2isa.tex revision 8241bc853cd629fb5c6299e6b8d5d546ee731343
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{llncs}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\documentclass[a4paper,11pt]{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\textwidth 15.93cm
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\textheight 24cm
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\oddsidemargin 0.0cm
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%\evensidemargin 0.0cm
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%\topmargin 0.0cm
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{document}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\title{Translating Haskell to Isabelle}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\author{ Paolo Torrini\inst{1} \and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Christoph Lueth\inst{2}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Christian Maeder\inst{2}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Till Mossakowski\inst{2}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\institute{Verimag, Grenoble, {\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 Heterogenous 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder %operators based on theory morphisms.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{abstract}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Introduction}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAutomating the translation from programming languages to the languagee of a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskigeneric prover may provide useful support for the formal development and the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiverification of programs. It has been argued that functional languages can
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimake the task of proving assertions about programs written in them easier,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till 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,
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOL is the implementation in Isabelle of classical higher-order logic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibased on simply typed lambda calculus extended with axiomatic type classes. It
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiprovides support for reasoning about programming functions, both in terms of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirich libraries and efficient automation.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF \cite{holcf} \cite{Paulson94isa,holcf} is Isabelle/HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconservatively extended with the Logic of Computable Functions --- a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiformalisation of domain theory.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have implemented as functions of Hets translations of Haskell to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIsabelle/HOLCF following an approach based on shallow embedding,
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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 proofs,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand Sect.~\ref{sec:conclusion} concludes the paper.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%Section 2 gives some background, section 3 introduces the system, section 4
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%gives the sublanguages of Haskell that can be translated, in section 5 we
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%define the two translations.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%, in section 6 we sketch a denotational semantics
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%associated with the translation to Isabelle/HOLCF, in section 7 we show how translation
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%of monads is carried out with AWE.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Semantic Background of the Translation}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\label{sec:semantics}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWe firstly describe the subset of Haskell that we cover.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOur translation to Isabelle/HOLCF covers at present Booleans, integers, basic
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiconstructors (function, product, list, \emph{maybe}), equality,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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 comprension, \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
5277e290ad70afdf97f359019afd8fb5816f4102Till 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},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand also consulted the complete static semantics for Haskell 98
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{journals/jfp/Faxen02}, as well as the (fragmentary) dynamic
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskisemantics \cite{oai:CiteSeerPSU:71374}. However, it should be noted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat there is no denotational semantics of Haskell! This also has been
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconfirmed in the answers to a query that one of the authors has sent
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito the Haskell mailing list. There is a static semantics for Haskell
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHence, our translation to Isabelle/HOLCF can be seen as the first
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotational semantics given to a large subset of Haskell 98.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis also means that there is no notion of correctness of this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslation, because it just \emph{defines} the denotational semantics.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOf course, an interesting question is the coincidence of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotational and operational semantics. However, this is beyond the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiscope of the paper.
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski%The base translation to Isabelle-HOL is more limited, insofar as it covers
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%only total primitive recursive functions. A better semantics with respect to
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%hard to be captured with Isabelle-HOL. It also seems hard to overcome the
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder%limitation to primitive recursion. Other limitations are similar to those
e91e02579a34e005734059ad09e0d1d1304a03e0Till Mossakowski%mentioned for the translation to Isabelle/HOLCF --- with the notable exception of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\section{Translations in Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%The Haskell-to-Isabelle translation in Hets requires GHC, Programatica,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%Isabelle and AWE. The application is run by a command that takes as arguments
5277e290ad70afdf97f359019afd8fb5816f4102Till 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.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%The Hets internal representation of Haskell is similar to that of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%Programatica, whereas the internal representation of Isabelle is based on the
376b6600e1ccebd180299471f732b008a96027d4Till 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
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%Isabelle theories are internally represented as Hets theories --- each of them
376b6600e1ccebd180299471f732b008a96027d4Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%composition of a signature translation with a translation of all sentences, is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%essentially a morphism from theories in the internal representation of the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%source language to theories in the representation of the target language.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Translation of Types}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\label{sec:types}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIn Isabelle/HOL types are interpreted as sets (class \emph{type});
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfunctions are total and may not be computable. A non-primitive
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederrecursive function may require discharging proof obligations already
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederat the stage of definition --- in fact, a specific relation has to be
30256573a343132354b122097b0ee1215dda1364Till Mossakowskigiven for a function to be proved total. In Isabelle/HOLCF each type
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis interpreted as a pointed complete partially ordered set (class
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\emph{pcpo}) i.e. a set with a partial order which has suprema of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$\omega$-chains and has a bottom. Isabelle's formalisation, based on
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiaxiomatic type classes \cite{Wenzel}, makes it possible to deal with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicomplete partial orders in quite an abstract way. Functions are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskigenerally partial and computability can be expressed in terms of
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicontinuity. Recursion can be expressed in terms of least fixed-point
30256573a343132354b122097b0ee1215dda1364Till Mossakowskioperator, and so, in contrast with Isabelle/HOL, function definition
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidoes not depend on proofs. Nevertheless, proving theorems in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIsabelle/HOLCF may turn out to be comparatively hard. After being
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispared the need to discharge proof obligations at the definition
30256573a343132354b122097b0ee1215dda1364Till Mossakowskistage, one has to bear with assumptions on function continuity
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithroughout the proofs. A standard strategy is then to define as much
30256573a343132354b122097b0ee1215dda1364Till Mossakowskias possible in Isabelle/HOL, using Isabelle/HOLCF type constructors to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilift types only when this is necessary.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe provision of pcpos, domains and continuous functions by
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF eases the translation of Haskell types and functions a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilot. However, special care is needed when trying to understand the
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell semantics. If one reads the section of the Haskell report
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskidealing with types and classes, one could come to the conclusion that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia function space in Haskell can be mapped to the space of the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedercontinuous functions in Isabelle/HOLCF --- this would correspond to a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipurely lazy language. However, Haskell is a mixed eager and lazy
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilanguage, and it provides a function $seq$ that enforces eager
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskievaluation. This function is introduced in part 6 of the Haskell
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskireport, ``Predefined Types and Classes'', in section 6.2. We quote
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski However, the provision of $seq$ has important semantic consequences,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski because it is available at every type. As a consequence, $\bot$ is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski not the same as $\lambda x \rightarrow \bot$, since $seq$ can be
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski used to distinguish them.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiIn order to enforce this distinction, each function space needs to be
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilifted. The same holds for products. We define these liftings in a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecific Isabelle theory \emph{HsHOLCF} (included in the Hets
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskidistrubution) as follows:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskidefaultsort pcpo
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidomain ('a,'b) lprod = lpair (lazy lfst :: 'a) (lazy lsnd :: 'b)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidomain 'a Lift = Lift (lazy 'a)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertypes ('a, 'b) "-->" = "('a -> 'b) Lift" (infixr 0)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski liftedApp :: "('a --> 'b) => ('a => 'b)" ("_$$_" [999,1000] 999)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* application *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski "liftedApp f x == case f of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Lift $ g => g $ x"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski liftedLam :: "('a => 'b) => ('a --> 'b)" (binder "Lam " 10)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* abstraction *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski "liftedLam f == Lift $ (LAM x . f x)"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{verbatim}
881ab7022a03f9a6fa697d3067d05d61844929cbChristian MaederOur translation of Haskell types to Isabelle types is defined
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirecursively. It is based on a translation of names for avoidance of
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiname clashes that is not specified here. We write $\alpha'$ for both
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe recursive translation of item $\alpha$ and the renaming according
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskito the name translation. The translation of types is given by the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskifollowing rules:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\noindent Types
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$$\begin{array}{ll}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski a & \Longrightarrow \ 'a::\{pcpo\} \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski () & \Longrightarrow \ unit \ \mbox{lift} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Bool & \Longrightarrow \ bool \ \mbox{lift} \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Integer & \Longrightarrow \ int \ \mbox{lift} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \tau_{1} \to \tau_{2} & \Longrightarrow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ \tau'_{1} \ \verb@-->@ \ \tau'_{2}) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (\tau_{1},\tau_{2}) & \Longrightarrow
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \ (\tau'_{1} ~lprod~ \tau'_{2}) \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder {[\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 ths corresponding HOL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitype. The Isabelle/HOLCF type constructor \emph{lift} is used to lift
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes to flat domains. The type constructor $llist$ is dicussed in the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Translation of Datatypes}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskihave four different semantics. Indeed, the correct translation to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidomain D1 = D1 (lazy D1_1::"Int \mathit{lift}")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidomain D2 = D2 (D2_1::"Int \mathit{lift}")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes S = "Int \mathit{lift}"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskipcpodef N = "{x:: Int \mathit{lift} . True}"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{verbatim}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\noindent In Isabelle/HOLCF, the keyword \emph{domain} defines a
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(possibly recursive) domain as solution of the corresponding domain
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiequation. The keyword \emph{lazy} ensures that the constructor $D1$
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;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskihere, we use it just to introduce an isomorphic copy of an existing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskipcpo --- this is the semantic of Haskell \emph{newtype} definitions.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%Note that the constructor for N is Abs_N, the selector Rep_N.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiLists are translated to the domain \emph{llist}, defined as follows
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiin our prelude theory \emph{HsHOLCF}:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$domain \ 'a\ llist \ = \ nil \ | \ \#\# \ (lazy\ HD :: \ 'a) \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(lazy \ TL :: \ 'a \ llist) $\\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\noindent allowing for partial list as well as for infinite ones \cite{holcf}.\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe general scheme for translation of mutually recursive lazy Haskell
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidatatypes to Isabelle/HOLCF domains is as follows:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabbing}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski$ data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k \ \Longrightarrow $\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$ \qquad $\=$ domain$\=$ \ \phi'_1 \ = \ $\=$ C'_{11} \ (lazy~d_{111} ::\ x'_1) \ \ldots \ (lazy~ d_{11i} :: \
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\>\>\>$ \ \ldots \ | \ $\\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\>\>\>$ C'_{1p} \
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (lazy~ d_{1p1} :: \ y'_1) \ \ldots \ (lazy~ d_{1pj} :: \ y'_j) $\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\>$ and \ \ldots $\\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\>$ and \ $\>$\phi'_n \ = \ C'_{n1} \ (lazy~ d_{n11} :: \ w'_1) \ \ldots \ (lazy~ d_{n1h}~:: \
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski w'_h) \ | \ $\\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\>\>\>$\ldots \ | $\\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\>\>\>$\ C'_{nq} \
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (lazy~ d_{nq1} :: \ z'_1) \ \ldots \ (lazy~ d_{nqk} :: \ z'_k) $\\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHere, the $d_{nqk}$ are the selectors. Mutually recursive datatypes
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirelies on specific Isabelle syntax (keyword \emph{and}). Order of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskideclarations is taken care of. In case of strict arguments (indicated
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwith ! in Haskell), the keyword \emph{lazy} is omitted.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe translation scheme for type synonyms simply is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$ type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \ types \ \tau \ = \ \tau'_1
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\section{Translation of Kinds and Type Classes}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiType classes in Isabelle and Haskell associate a set of functions to a
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertype class identifier (these are also called the \emph{methods} of the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichclass). In Isabelle, type classes are typically further specified
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichusing a set of axioms; for example, the class
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski$\mathit{linorder}$ of total orders is specified using the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiusual total order axioms. Of course, such axiomatizations are not
30256573a343132354b122097b0ee1215dda1364Till Mossakowskipossible in Haskell. Indeed, in Haskell, there is no check that the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiclass $Ord$ actually consists of total orders only, and hence it would
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskibe inappropriate to translate it to $\mathit{linorder}$ in Isabelle.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiInstead, we translate to a newly declared Isabelle class $Ord$.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe only thing that we assume is that it is a subclass of $pcpo$,
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskibecause all Haskell types are translated to pcpos.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHence, tpye classes are translated to Isabelle/HOLCF as subclasses of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\emph{pcpo} with empty axiomatization.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMethods declarations associated with
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHaskell classes are translated to independent function declarations with
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiappropriate class annotation on type variables.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiClass instance declarations declare that a particular type belongs to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia class. In Isabelle, instance declarations generate proof
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiobligations, namely that the methods for the type at hand indeed
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskisatisfy the axioms of the class. Since our translations only
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskigenerates classes without axioms (beyond those of $pcpo$), proofs are trivial and proof obligation
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskimay be automatically discharged.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA Haskell class instance declaration that declares type $T$
30256573a343132354b122097b0ee1215dda1364Till Mossakowskito belong to class $C$ may define the behaviour of the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiclass methods for $T$. The same is possible with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinormal Isabelle constant definitions, if the type of the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiconstant (function) is specialised to $T$ in the definition.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiWith this, we avoid an explicit handling of dictionaries, as
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidescribed in the static semantics of Haskell \cite{journals/jfp/Faxen02}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%Not all the problems have been solved with
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%respect to arities that may conflict in Isabelle, although they correspond to
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%compatible Haskell instantiations.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA restriction of Isabelle is that it does neither allow for
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimulti-parameter classes, nor for type constructor ones. Therefore, the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisame restrictions apply to our translation.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent Classes
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$\begin{array}{ll}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski K & \Longrightarrow \ K'
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski\noindent Type schemas
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$\begin{array}{ll}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ (ctx \Rightarrow \tau)'
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \ [(v'::s) / (v'::({K'} \cup s))] \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{array}$$\\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHaskell type variables are translated to variables of class
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\emph{pcpo}. Each type is associated to a sort in Isabelle (in
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHaskell, the same concept is called ``kind''), defined by the set of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe classes of which it is member.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent Class declarations
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \Longrightarrow \ class \ K' \ \subseteq
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski \ pcpo; \ Dec'_1; \ \ldots; \ Dec'_n \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent Class instance definitions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$$\begin{array}{l}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinstance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski \ \Longrightarrow \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \qquad instance \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski \in ctx\}, \ \ldots, \\
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski \qquad \qquad \qquad \quad \quad
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \qquad \qquad \mbox{with \ proof \ obligation}; \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \qquad defs \ f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (ctx \Rightarrow \tau_n)' == t'_n
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{array}$$\\
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\section{Translation of Function Definitions and Terms}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiTerms of built-in type are translated using Isabelle/HOLCF-defined lifting function
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\emph{Def}. The bottom element $\bot$ is used for undefined terms.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle/HOLCF-defined $flift1 :: \ ('a \Rightarrow 'b::pcpo) \Rightarrow ('a \ lift
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\to 'b)$ and $flift2 :: \ ('a \Rightarrow 'b) \Rightarrow ('a \ lift \to 'b \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilift)$ are used to lift operators, as well as the following, defined in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\emph{HsHOLCF}.\\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \Rightarrow ('a \ lift \to \ 'b \ lift \to \ 'c \ lift) $
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski$fliftbin \ f \ == \ flift1 \ (\lambda x. \ flift2 \ (f \ x))$\\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\noindent Boolean values are translated to values of \emph{bool lift}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski(\emph{tr} in Isabelle/HOLCF) i.e. \emph{TT}, \emph{FF} and $\bot$, and Boolean
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiconnectives to the corresponding Isabelle/HOLCF operators. Isabelle/HOLCF-defined \emph{If then
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski else fi} and \emph{case} syntax are used to translate conditional and case
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiexpressions, respectively. There are restrictions, however, on case
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiepressions, due to limitations in the translation of patterns; in particular,
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskionly simple patterns are allowed (no
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskinested ones). On the other hand, Isabelle sensitiveness to the order of
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskipatterns in case expressions is dealt with. Multiple function definitions are
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitranslated as definitions based on case expressions. In function definitions
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskias well as in case expressions, both wildcards --- not available in Isabelle
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski--- and incomplete patterns --- not allowed --- are dealt with by elimination,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski$\bot$ being used as default value in the latters. Only let expressions
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiwithout patterns on the left are dealt with; where expressions, guarded
c5e63ec138b908ac9d15e6843120033bf36a1862Till Mossakowskiexpressions and list comprehension are not covered.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski$$\begin{array}{l}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \ consts \ f' \ :: \ \phi' \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \overline{x}_1 \to \ t_1); \
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski == \ Lam \ \overline{x}'. \ t' \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (f_1 \ \overline{v_1} \ = \ t_1; \ \ldots;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \ f_n \ \overline{v_n} \ = \ t_n) \ \Longrightarrow \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \qquad fixrec \ f'_1 :: \phi'_1 \ =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \ (Lam \ \overline{v_1}'. \ t'_1) \ and \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \qquad \quad \ldots \\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \qquad \quad and \ f'_n :: \phi'_n \ =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ (Lam \ \overline{v_n}'. \ t'_n) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNon-recursive definitions are translated to standard definitions using
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIsabelle keyword \emph{defs}. Recursive definitions rely on
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIsabelle/HOLCF package \emph{fixrec} which provides nice syntax for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifixed point definitions, including mutual recursion. Lambda
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiabstraction is translated as continuous abstraction for lifted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifunction spaces (\emph{Lam}), function application as continuous
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiapplication (the \emph{\$\$} operator), see Sect.~\ref{sec:types}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Example Proofs}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:ex}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Conclusion and Related Work}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:conclusion}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe provide a shallow embedding of Haskell to Isabelle/HOLCF,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhich can be used for proving properties of Haskell programs,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibut also is the first denotational semantics that has been
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedergiven to Haskell.
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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertypes have to be lifted due to the mixture of eager and lazy evaluation
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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 lies with 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\cite{Thompson92}, both based on large-step operational semantics;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithat of Haskell to Agda implementation of Martin-Loef type theory in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\cite{Abel} --- still, higher-order logic may be quite helpful in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiorder to deal with features such as currying and polymorphism.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiMoreover, higher-order approaches may rely on denotational semantics
30256573a343132354b122097b0ee1215dda1364Till Mossakowski--- as for examples, \cite{Huff} translating Haskell to HOLCF, and
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{Pollack} translating ML to HOL --- allowing for program
30256573a343132354b122097b0ee1215dda1364Till Mossakowskirepresentation closer to specification as well as for proofs
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicomparatively more abstract and general.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe translation of Haskell to Isabelle/HOLCF proposed in \cite{Huff}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiuses deep embedding to deal with types. Haskell types are translated
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito terms, relying on a domain-theoretic modelling of the type system
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiat the object level, allowing explicitly for a clear semantics, and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiproviding for an implementation that can capture most features,
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiincluding type constructor classes. In contrast, we provide in the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicase of Isabelle/HOLCF with a translation that follows the lines of a
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidenotational semantics under the assumption that type constructors and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertype application in Haskell can be mapped to corresponding
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiconstructors and built-in application in Isabelle without loss from
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskithe point of view of behavioural equivalence between programs --- in
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiparticular, translating Haskell datatypes to Isabelle ones. Our
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskisolution gives in general less expressiveness than the deeper approach
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski--- however, when we can get it to deal with cases of interest, it
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskimight make proofs easier.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%On the other hand, the main novelty in our work is
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski%to rely on theory morphisms and on their implementation for Isabelle in the
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski%package AWE \cite{AWE}, in order to deal with special cases of monadic
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski% Currently Hets provides with an extension of the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%base translation to Isabelle/HOL which uses AWE and covers state monad types
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski%inclusive of \emph{do} notation. Due to present limitations of AWE, this
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski%solution is available only for Isabelle/HOL at the moment, although in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%principle it could work for Isabelle/HOLCF as well.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiFuture work should use this framework for proving properties of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHaskell programs. Currently Hets already provides some experimental
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitranslation of constructor classes and monads, also covering \emph{do}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskinotation, using theory morphisms as provided by the package AWE
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\cite{AWE}. However, there are mainly syntactic problems with name
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiclashes that currently prevent a proper integration with
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIsabelle/HOLCF. These problems should be solved in the near future.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFor monadic programs, we are also planning to use the monad-based
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidynamic Hoare and dynamic logic that already have been formalised in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIsabelle \cite{Walter05}. Our translation tool from Haskell to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIsabelle is part of the Heterogeneous Tool Set Hets and can be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidownloaded from \texttt{http://www.dfki.de/sks/hets}. More details
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiabout the translations can be found in \cite{Tlmm}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%This translation, due to the character of the P-logic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%typing system, could be more easily carried out relying on some form
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%of universal quantification on type variables, or else further relying
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%on parametrisation.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection*{Acknowledgment}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThis work has been supported by the {\em Deutsche
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Forschungsgemeinschaft} under grants KR \mbox{1191/5-2} and \mbox{KR
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\bibliographystyle{alpha} \bibliography{case}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{document}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\subsection{HOL}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe translation $\omega_s \ :: \ H_s \ \to \ HOL$ from programs in $H_s$
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskito theories in Isabelle/HOL extended with AWE can be defined with the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifollowing set of rules.\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent Types
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski () & \Longrightarrow \ unit \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski a & \Longrightarrow \ 'a::\{type\} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Bool & \Longrightarrow \ boolean \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Integer & \Longrightarrow \ int \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \tau_{1} \to \tau_{2} & \Longrightarrow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ \tau'_{1} \ \Rightarrow \ \tau'_{2} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (\tau_{1},\tau_{2}) & \Longrightarrow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ (\tau'_{1} * \tau'_{2}) \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder {[\tau]} \ & \Longrightarrow \ \tau' \ list \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Maybe \ \tau & \Longrightarrow \ \tau' \ option \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski T \ \tau_1 \ \ldots \ \tau_n & \Longrightarrow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ \tau'_1 \ \ldots \ \tau'_n \ T' \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\noindent Classes
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$$\begin{array}{ll}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Eq & \Longrightarrow \ Eq \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder K & \Longrightarrow \ K'
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent Type schemas
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$$\begin{array}{ll}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (\{K \ v\} \ \cup \ ctx) \ \Rightarrow \ \tau & \Longrightarrow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ (ctx \Rightarrow \tau)'
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ [(v'::s) / (v'::({K'} \cup s))] \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \{\} \ \Rightarrow \ \tau & \Longrightarrow \ \tau'
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{array}$$\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHere we highlight the main differences the translation to Isabelle/HOLCF and this,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisemantically rather more approximative one to Isabelle/HOL (thereafter simply
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHOL). Function type, product and list are used to translate the corresponding
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiHaskell constructors. Option types are used to translate \emph{Maybe}. Haskell
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidatatypes are translated to HOL datatypes. Type variables are of class
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiStandard lambda-abstraction ($\lambda $) and function application are used
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskihere, instead of continuous ones. Non-recursive definitions are treated in an
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskianalogous way as in the translation to Isabelle/HOLCF. However, partial functions and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiparticularly case expressions with incomplete patterns are not allowed.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn HOL one has to pay attention to the distinction between \emph{primitive
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski recursive} functions (introduced by the keyword \emph{primrec}) and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedergenerally recursive ones. Termination is guaranteed for each primitive
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirecursive function by the fact that recursion is based on the datatype
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructure of one of the parameters. In contrast, termination is no trivial
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermatter for recursion in general. A strictly decreasing measure needs to be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiassociation with the parameters. This cannot be dealt with automatically in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskigeneral. Threferore here we restrict translation to primitive recursive
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMutual primitive recursion is allowed for under additional restrictions ---
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskimore precisely, given a set $F$ of functions: 1) all the functions in $F$ are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirecursive in the first argument; 2) all recursive arguments in $F$ are of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskivariables which occurs on the right hand-side but not on the left hand-side of
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedervariable renaming, they are translated to projections of a new function of
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskitype $A \rightarrow (B_{1} * \ldots * B_{n})$ which is defined for cases of
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiexpression $nth_n \ t$ used in the translation rule is simply an informal
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiabbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiextracts the $n$-th projection from a tuple no shorter than $n$.\\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent Terms
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$$\begin{array}{ll}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski x::\tau & \Longrightarrow \ x'::\tau' \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski () & \Longrightarrow \ () \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski True & \Longrightarrow \ True \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski False & \Longrightarrow \ False \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \&\& & \Longrightarrow \ \& \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski || & \Longrightarrow \ | \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder not & \Longrightarrow \ Not \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski c & \Longrightarrow \ c \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ t \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski negate \ x & \Longrightarrow \ - x \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski {[]} & \Longrightarrow \ {[]} \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski t:ts & \Longrightarrow \ t'\#ts' \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski head & \Longrightarrow \ hd \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder tail & \Longrightarrow \ tl \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski == & \Longrightarrow \ hEq \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski /= & \Longrightarrow \ hNEq \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski Just & \Longrightarrow \ Some \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski Nothing & \Longrightarrow \ None \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski return & \Longrightarrow \ return \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski bind & \Longrightarrow \ mbind \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski C & \Longrightarrow \ C' \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski f & \Longrightarrow \ f' \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \backslash \overline{x} \ \to \ t & \Longrightarrow
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \ \lambda \ \overline{x}'. \ t' \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski t_1 \ t_2 & \Longrightarrow \ t'_1 \ t'_2 \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski fst & \Longrightarrow \ fst \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski snd & \Longrightarrow \ snd \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski let \ (x_1 = t_1; & \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \qquad \dots; & \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \qquad x_n = t_n) \quad in \ t & \Longrightarrow
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \ if \ t' \ then \ t'_1 \ else \ t'_2 \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case \ x \ of \ (p_1 \to t_1; \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \qquad \qquad \ldots; & \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad p_n \to t_n) & \Longrightarrow
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \Rightarrow t'_n \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder \mbox{is \ a \ complete \ match} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \Rightarrow t'_{n-1} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p'_{n-1}, q_1, \ldots, q_k \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & \qquad \mbox{complete \ match}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{array}$$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Declarations
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{l} class \ K \ where \ (Dec_1; \ldots; Dec_n \rceil) \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \Longrightarrow \ class \ K' \ \subseteq
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ type; \ Dec'_1; \ \ldots; \ Dec'_n \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski f :: \phi \qquad \qquad \qquad \quad \Longrightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ consts \ f' \ :: \ \phi' \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type \ \tau \ = \ \tau_1 \qquad \qquad \Longrightarrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ type \ \tau \ = \ \tau'_1 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (data \ \phi_1 \ = \ C_{11} \ x_1 \ldots x_i
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ | \ \ldots \ | \ C_{1p} \ y_1 \ldots y_j; \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski data \ \phi_n \ = \ C_{n1} \ w_1 \ldots w_h
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ | \ \ldots \ | \ C_{1q} \ z_1 \ldots z_k) \ \Longrightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad datatype \ \phi'_1 \ = \ C'_{11} \ x'_1 \ \ldots \ x'_i \ | \ \ldots
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ | \ C'_{1p}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ y'_1 \ \ldots \ y'_j \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad and \ \ldots \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad and \ \phi'_n \ = \ C'_{n1} \ w'_1 \ \ldots \ w'_h \ | \ \ldots \ | \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ z'_1 \ \ldots \ z'_k \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \mbox{where} \ \phi_1, \ \phi_n \ \mbox{are \ mutually \ recursive \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Definitions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{l} f \ \overline{x} \ p_1 \ \overline{x}_1 \ = \ t_1; \
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \ f \ \overline{x} \ p_n \ \overline{x}_n \ = \ t_n \ \Longrightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad (f \ \overline{x} \ = \ case \ y \ of \ (p_1 \to (\backslash
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \overline{x}_1 \to \ t_1); \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ldots; \ p_n (\to \backslash \overline{x}_n \to \ t_n)))' \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski f \ \overline{x} \ = \ t \qquad \qquad \Longrightarrow \ defs \ f' :: \phi'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski == \ \lambda \ \overline{x}'. \ t' \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder f_1 \ \ y_1 \ \overline{x_1} \ =
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \ t_1; \ \ldots; \ f_n \ y_n \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \overline{x_n} \ = \ t_n \ \Longrightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad decl \ f_{new} ::
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (\sigma_1(ctx_1) \ \cup \ \ldots \ \cup \ \sigma_n(ctx_n)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ \Rightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad \qquad \sigma_1(\tau_{1a}) \ \to \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (\sigma_1(\tau_1), \ldots, \sigma_n(\tau_n)))' \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad primrec \ f_{new} \ sp_1 \ =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ (\lambda \ \overline{x_1}'. \ t'_1 [y'_1/sp_1], \ldots, \ \lambda \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \overline{x_n}'. t'_n [y'_n/sp_1]); \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad \ldots; \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski f_{new} \ sp_k \ = \ (\lambda \ \overline{x_1}'. \ t'_1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [y'_1/sp_k], \ldots,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ \lambda \ \overline{x_n}'. \ t'_n [y'_n/sp_k]); \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad defs \ f_1 \ x \ == \ nth_1 \ (f_{new} \ x); \ \ldots;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ f_n \ x \ == \ nth_n \ (f_{new} \ x) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \mbox{with} \ f_1:: (ctx_1 \Rightarrow \tau_{1a} \to \tau_1),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ \ldots, \ f_n::(ctx_n \Rightarrow \tau_{na} \to \tau_n) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \mbox{mutually \ recursive} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski instance \ ctx \ \Rightarrow \ K_T \ (T \ v_1 \ \ldots \ v_n) \ where \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \qquad (f_1::\tau_1 = t_1; \ldots; \ f_n::\tau_n = t_n)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ \Longrightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad instance \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \qquad \qquad \tau' :: \ K_{T}' \ (\{pcpo\} \ \cup \ \{K':(K \ v_1)
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski \in ctx\}, \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \qquad \quad \quad
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ldots, \ \{pcpo\} \ \cup \ \{K':(K \ v_n) \in ctx\}) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \mbox{with \ proof \ obligation}; \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad defs \quad
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski f'_1 :: (ctx \Rightarrow \tau_1)' == t'_1; \ \ldots; \ f'_n ::
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (ctx \Rightarrow \tau_n)' == t'_n\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski instance \ Monad \ \tau \ where \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (def_{eta}; def_{bind}) \ \Longrightarrow \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad defs \quad def'_{eta}; \ def'_{bind}; \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad t\_instantiate \ Monad \ mapping \ m\_\tau' \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \mbox{where} \ m_\tau' \ \mbox{is \ defined \ as \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski theory \ morphism \ associating} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \qquad \mbox{to} \ tau', \ def'_{eta}, \ def'_{bind} \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \mbox{respectively;}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{array}$$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiType classes are translated to subclasses of \emph{type}. An axiomatisation of
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell equality for total functions can be found in \emph{HsHOL}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski heq :: & 'a \ \to \ 'a \ \to \ bool \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski hneq :: & 'a \ \to \ 'a \ \to \ bool \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$axclass \ Eq \ < \ type$
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$eqAx: heq \ p \ q \ = \ Not \ (hneq \ p \ q)$\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiGiven the restriction to total functions, equality on built-in types can be
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidefined as HOL equality.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Semantics (for HOLCF)}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDenotational semantics con be given as basis for the translation to Isabelle/HOLCF.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiEssentially, the claim here is that the expressions on the left hand-side of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe following tables represent the denotational meaning of the Haskell
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexpressions on the right hand-side, as well as of the Isabelle/HOLCF expressions to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhich they are translated. The language on the left hand-side is still based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion Isabelle/HOLCF where type have been extended with abstraction ($\Lambda$) and fixed
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipoint ($\mu$) in order to represent the denotational meaning of domain
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskideclarations.\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil a \rceil & = \ 'a::pcpo \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil () \rceil & = \ unit \ lift \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil Bool \rceil & = \ bool \ lift \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil Integer \rceil & = \ int \ lift \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil \to \rceil & = \ \to \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil (,) \rceil & = \ * \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil [] \rceil & = \ seq \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil Maybe \rceil & = \ maybe \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil T_1 \ T_2 \rceil & = \ \lceil T_1 \rceil \ \lceil T_2 \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \lceil TC \rceil & = & \mu X. (\Lambda \ v_1, \ldots, v_n.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \ \lceil \tau_1 \rceil + \ldots + \lceil \tau_{k} \rceil)[X/TC] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \mbox{when \ there \ is \ a \ declaration} \ data \ TC \ v_1 \ \ldots \ v_n
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \ = \ C_1::\tau_1 | \ldots |
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% C_k::\tau_k \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil TC_{i} \rceil & = \ let \ F \ = \ \mu \ (X_1*\ldots*X_k). \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \quad ((\Lambda \ v_{11}, \ldots, v_{1m}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ \lceil \tau_{11} \rceil + \ldots + \lceil \tau_{1p} \rceil),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \quad (\Lambda \ v_{k1}, \ldots, v_{kn}. \ \ldots,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ \lceil \tau_{k1} \rceil + \ldots + \lceil \tau_{kq} \rceil))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & in \ nth_i(F) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \quad \mbox{with} \ 0 < i \leq k, & \mbox{when} \ data \ TC_1 \ v_{11} \ \ldots \ v_{1m} \ = \ C_{11}::\tau_{11}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | \ldots | C_{1p}::\tau_{1p}; \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \quad \ldots; \ data \ TC_k \ v_{k1} \ \ldots \ v_{kn} \ =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ C_{k1}::\tau_{k1} | \ldots |
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslation, except that for functions we give the representation of the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermeaning of \emph{fixrec} definitions ($FIX$ is the Isabelle/HOLCF fixed point
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{ll}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil x::a \rceil & = \ x'::\lceil a \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil c \rceil & = \ c' \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil \backslash x \ \to \ f \rceil & = \ LAM \ x_{t}. \ \lceil f \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil (a,b) \rceil & = \ (\lceil a \rceil, \lceil b \rceil) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil t_1 \ t_2 \rceil & = \ \lceil t_1 \rceil \ \cdot \
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \lceil t_2 \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & = \ let \ \lceil
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \lceil f_i \rceil & = \ let \ g \ =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski FIX \ (x_1,\ldots,x_n). \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (\lceil t_1 \rceil, \ldots, \lceil t_{n} \rceil [f_1/x_1,\ldots,f_n/x_n] \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & in \ nth_i (g) \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \quad \mbox{with} \ 0 < i \leq n,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \mbox{where} \ f_1 = t_1, \ f_n = t_n \ \mbox{are \ mutually \ recursive
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ definitions}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% \ldots \lceil a_{n} \rceil \ TyCons_{t}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Monads with AWE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiA monad is a type constructor with two operations that can be specified
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiaxiomatically --- \emph{eta} (injective) and \emph{bind} (associative, with
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{eta} as left and right unit) \cite{moggi89}. Isabelle does not have
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitype constructor classes, therefore monads cannot be translated directly. The
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiindirect solution that we are pursuing, is to translate monadic types as types
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat satisfy the monadic axioms. This solution can be expressed in terms of
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitheory morphisms --- maps between theories, associating signatures to
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskisignatures and axioms to theorems in ways that preserve operations and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiarities, entailing the definition of maps between theorems. Theory morphisms
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiallow for theorems to be moved between theories by translating their proof
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiterms, making it possible to implement parametrisation at the theory level
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(see \cite{AWE} for details). A \emph{parameterised theory} $\mathit{Th}$ has
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskia sub-theory $\mathit{Th}_P$ which is the parameter --- this may contain
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiaxioms, constants and type declarations. Building a theory morphism from
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder$\mathit{Th}_P$ to a theory $I$ provides the instantiation of the parameter
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiwith $I$, and makes it possible to translate the proofs made in the abstract
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisetting of $\mathit{Th}$ to the concrete setting of $I$ --- the result being
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskian extension of $I$. AWE is an extension of Isabelle that can assist in the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiconstruction of theory morphisms \cite{AWE}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiA notion of monad \cite{AWE2} can be built in AWE by defining, on an abstract
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilevel, a hierarchy of theories culminating in \emph{Monad}, based on the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskideclaration of a unary type constructor $M$ (in \emph{MonadType}) with the two
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimonad operations (contained in \emph{MonadOpEta} and \emph{MonadOpBind},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskirespectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecific type constructor forms a monad, we have to construct a theory
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimorphism from \emph{MonadAxms} to the specific theory; this involves giving
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecific definitions of the operators, as well as discharging proof
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiobligations associated with specific instances of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe axioms. The following gives an example. \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $data \ LS \ a \ = \ N \ | \ C \ a \ (LS \ a)$
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\noindent $instance \ Monad \ LS \ where$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{ll}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return \ x & = \ C \ x \ N \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski x \ >>= \ f & = \ case \ x \ of \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & N \ \to \ N \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & C \ a \ b \ \to \ cnc \ (f \ a) \ (b \ >>= \ f)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski$cnc :: \ LS \ a \ \to \ LS \ a \ \to \ LS \ a $
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski$$\begin{array}{ll}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicnc \ x \ y & = \ case \ x \ of \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski & N \ \to \ y \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski & C \ w \ z \ \to \ cnc \ z \ (C \ w \ y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent These definitions are plainly translated to HOL, as follows. Note
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithat these are not overloaded definitions. \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent $datatype \ 'a \ LS \ = \ N \ | \ C \ 'a \ ('a \ LS)$
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\noindent $consts $
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$$\begin{array}{ll}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return\_LS & :: \ 'a \ \Rightarrow 'a \ LS \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski mbind\_LS & :: \ 'a \ LS \ \Rightarrow \ ('a \ \Rightarrow \ 'b \ LS) \
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \Rightarrow \ 'b \ LS \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski cnc & :: \ 'a \ LS \ \Rightarrow \ 'a \ LS \ \Rightarrow \ 'a \ LS \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $defs $
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu$$\begin{array}{l}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederreturn\_LS\_def : \ return\_LS:: \ ('a \ LS \ \Rightarrow 'a) \ == \
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu \lambda x. \ C \ x \ N
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\noindent $primrec $
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski$$\begin{array}{ll}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskimbind\_LS \ N & = \ \lambda f. \ N \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskimbind\_LS \ (C \ pX1 \ pX2) & = \ \lambda f. \ cnc \ (f \ pX1) \ (mbind\_LS \ pX2 \ f)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\noindent $primrec $
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski$$\begin{array}{ll}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskicnc \ N & = \ \lambda b. \ b \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicnc \ (C \ pX1 \ pX2) & = \ \lambda b. \ cnc \ pX2 \ (C \ pX1 \ b)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent In order to build up the instantiation of \textit{LS} as a monad,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskihere it is defined the morphism $m\_LS$ from \emph{MonadType} to the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiinstantiating theory \emph{Tx}, by associating $M$ to $LS$.\\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$thymorph \ m\_LS : \ MonadType \ \longrightarrow \ Tx $
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{l}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski maps \ [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski renames: \ [(MonadOpEta.eta \mapsto return\_LS),
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (MonadOpBind.bind \mapsto mbind\_LS)] \\
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiRenaming is used in order to avoid name clashes in case of more than one
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskimonads --- here again, note the difference with overloading. Morphism
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\emph{m\_LS} is then used to instantiate the parameterised theory
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\emph{MonadOps}.\\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent $t\_instantiate \ MonadOps \ mapping \ m\_LS$ \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent This instantiation gives the declaration of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstantiated methods, which may now be defined.\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent $defs $
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski$$\begin{array}{l}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiLS\_eta\_def: \ LS\_eta \ == \ return\_LS \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiLS\_bind\_def: \ LS\_bind \ == \ mbind\_LS
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich\noindent In order to construct a mapping from \emph{MonadAxms} to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicase, by straightforward simplification). The translation will print out
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{sorry} instead.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilemma \ LS\_lunit : & LS\_bind \ (LS\_eta \ x) \ t \ = \ t \ x \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilemma \ LS\_runit : & LS\_bind \ (t:: \ 'a \ LS) \ LS\_eta \ = \ t \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilemma \ LS\_assoc : & LS\_bind \ (LS\_bind \ (s:: \ 'a \ LS) \ t) \ u \ = \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & LS\_bind \ s \ (\lambda x. \ LS\_bind \ (t \ x) \ u) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilemma \ LS\_eta\_inj : & LS\_eta \ x \ = \ LS\_eta \ y \ \Longrightarrow \ x \ = \ y
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent Now, the morphism from \emph{MonadAxms} to
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\emph{Tx} can be built, and then used to instantiate \emph{Monad}. This gives
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiautomatically access to the theorems proven in \emph{Monad} and, modulo
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskirenaming, the monadic syntax which is defined there. \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$thymorph \ mon\_LS : \ MonadAxms \ \longrightarrow \ Tx $
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski maps & [('a \ MonadType.M \ \mapsto \ 'a \ Tx.LS)] \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & [(MonadOpEta.eta \ \mapsto \ Tx.LS\_eta), \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & (MonadOpBind.bind \ \mapsto \ Tx.LS\_bind)]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$t\_instantiate \ Monad \ mapping \ mon\_LS$\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$renames: \ [ \ldots ]$\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent The \emph{Monad} theory allows for the characterisation of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisingle parameter operators. In order to cover other monadic operators, a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipossibility is to build similar theories for type constructors of fixed arity.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiAn approach altogether similar to the one shown for HOL could be used, in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiprinciple, for Isabelle/HOLCF as well.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{comment}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere is a simple example. \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent $ fn3 \ :: \ AC \ a \ b \to (a \to a) \to AC \ a \ b $
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifn3 \ k \ f & = \ case \ k \ of \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & Ct \ x \to Ct \ (f \ x) \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & Rt \ x \ y \to Rt \ (fn4 \ x) \ y \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent $ fn4 \ :: \ AC \ a \ b \to AC \ a \ b $
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{ll}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifn4 \ k & = \ case \ k \ of \\
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder & Rt \ x \ y \to Rt \ (fn3 \ x \ (\backslash z \to z)) \ y \\
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder & Ct \ x \to Ct \ x \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\noindent It translates to HOL as follows.\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\noindent $consts$
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$$\begin{array}{ll} fn3 \ :: & ('a, 'b) \ AC \Rightarrow ('a \Rightarrow
30256573a343132354b122097b0ee1215dda1364Till Mossakowski 'a) \Rightarrow
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \ ('a, 'b) \ AC \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski fn4 \ :: & ('a, 'b) \ AC \Rightarrow
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \ ('a, 'b) \ AC \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski fn3\_Xfn4\_X :: & ('a, 'b) \ AC \Rightarrow
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ (('a \Rightarrow 'a) \Rightarrow \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & ('a, 'b) \ AC) *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ (('a \Rightarrow 'a) \Rightarrow
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \ ('a, 'b) \ AC) \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\noindent $defs$
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$$\begin{array}{lll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifn3\_def : & fn3 \ == \ \lambda k \ f. \ fst \ (( fn3\_Xfn4\_X :: \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & \ ('a, 'b) \ AC \Rightarrow (('a \Rightarrow 'a) \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & \Rightarrow ('a, 'b) \ AC) * ((unit \Rightarrow unit) \Rightarrow \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & ('a, 'b) \ AC) ) \ k) \ f \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski fn4\_def : & fn4 \ == \ \lambda k \ f. \ snd \ (( fn3\_Xfn4\_X :: \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & ('a, 'b) \ AC \Rightarrow \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) * \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AC) ) \ k) \ f \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\noindent $primrec$
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski$$\begin{array}{lll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifn3\_Xfn4\_X & (Ct \ pX1) \ = & (\lambda f. \ Ct \ (f \ pX1), \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & & \lambda f. \ Ct \ pX1) \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifn3\_Xfn4\_X & (Rt \ pX1 \ pX2) & = \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & (\lambda f. \ Rt \ (snd & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2, \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski & \lambda f. \ Rt \ (fst & (fn3\_Xfn4\_X \ pX1) \ f) \ pX2) \\
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIn the following, we give a definition of the sub-language of Haskell
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$H_c$ that is covered by the translation to Isabelle/HOLCF.\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\noindent Types
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$$\begin{array}{lll}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \tau \ = () \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & Integer & \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & v & \mbox{type \ variable}\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & \tau_1 \to \tau_2 & \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & (\tau_1,\tau_2) & \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% & Either \ tau_1 \ tau_2 \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & [\tau] & \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & Maybe \ \tau & \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & T \ \tau_{1} \ \ldots \tau_{n} & \mbox{either \ datatype \ or \
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder defined \ type}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% & T \ \tau_{1} \ \ldots \ \tau_{n} \qquad \mbox{defined \ type}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\noindent Type classes
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski$$\begin{array}{lll}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski K \ = & Eq & \mbox{with \ default \ methods} \ ==, \ /= \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & K & \mbox{defined \ type \ class} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent Contexts
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$$\begin{array}{lll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ctx \ = & \{K \ v\} \ \cup \ ctx & \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski & \{\} & \mbox{empty \ context} \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent Type schemas
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{ll}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \phi \ = & ctx \Rightarrow \tau \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & \qquad \mbox{where \ all \ variables \ in} \ ctx \ \mbox{are \ in} \ \tau
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\noindent Simple patterns
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{lll}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski sp \ = & \_ & \mbox{wildcard} \\
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski & v & \mbox{variable \ of \ datatype}\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & C \ \overline{v} & \mbox{case \ of \ datatype}
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder\noindent Terms
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$$\begin{array}{lll} t \ =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & c \in \aleph & \mbox{Integer \ constant} \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & t \in \{:,head,tail\} & \mbox{on list} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & t \in \{Just,Nothing\} & \mbox{on \ \emph{maybe} \ types} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & t \in \{fst,snd\} & \mbox{on \ pairs} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & x & \mbox{variable} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & f & \mbox{function \ symbol} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & C & \mbox{data \ constructor} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & if \ t \ then \ t_1 \ else \ t_2 \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & let \ (x_1 = t_1; \ \ldots; \ x_n = t_n) \ in \ t
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\noindent Declarations
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski$$\begin{array}{ll}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Decl \ = & type \ T \ \overline{v} \ = \ \tau \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & data \ ctx \ \Rightarrow \ T \ \overline{v} \ =
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \ C_{1} \ \overline{x}_1 \ | \ \ldots \ | \ C_{k} \ \overline{x}_k \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% & \qquad \mbox{with} \ {\overline{x}}_1, {\overline{x}}_k \ \subseteq \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% \overline{v} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & ctx \ \Rightarrow \ f \ :: \ \tau \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & class \ K \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich where \ (f_{1}:: \tau_{1}; \ldots; f_{n}::\tau_{n}) \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{where} \ \tau_{1}, \tau_{n} \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \mbox{have \ only \ one \ type \ variable}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\noindent Definitions
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich$$\begin{array}{ll}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Def \ = & f \ \overline{v} \ = \ t \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & f \ \overline{v}_{1} \ sp_1 \ {\overline{w}}_{1} \ = \ t_1; \ \ldots;
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ f \ \overline{v}_{n} \ sp_n \ {\overline{w}}_{n} \ = \ t_n \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & instance \ ctx \Rightarrow K \ \tau \ where \
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (f_1 = t_1; \ldots; \ f_n = t_n) \\
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich & \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ methods \ of} \ K
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{array}$$\\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\subsection{HOL}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiIn contrast, the following gives a definition of the Haskell sub-language
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$H_s$ that is covered by the translation to HOL.\\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\noindent Types, Type classes, Contexts, Type schemas, Simple patterns,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \emph{as before}\\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\noindent Type constructor classes
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\noindent Terms
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich$$\begin{array}{lll} t \ =
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & t \in \{True,False,\&\&,||,not\} & \mbox{on \ Boolean} \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & c \in \aleph & \mbox{Integer \ constant} \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & t \in \{+,*,-,div,mod,negate,<,>\} & \mbox{on \ Integer} \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & t \in \{:,head,tail\} & \mbox{on list} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & t \in \{==,\ /=\} & \mbox{on \ equality \ types} \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & t \in \{Just,Nothing\} & \mbox{on \ Maybe} \\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski & t \in \{return,bind\} & \mbox{on \ monadic \ types} \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski & t \in \{fst,snd\} & \mbox{on \ pairs} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & x & \mbox{variable} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & f & \mbox{function \ symbol} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & C & \mbox{data \ constructor} \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski & if \ t \ then \ t_1 \ else \ t_2 \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski & case \ x \ of \ (sp_{1} \to t_1; \ \ldots; \ sp_{n} \to t_n) \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{with} \ sp_1, \ldots, sp_n \ \mbox{complete \ match} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & let \ (x_1 = t_1; \ \ldots; \ x_n = t_n) \ in \ t
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\noindent Definitions
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich$$\begin{array}{ll}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Def \ = & f \ \overline{v} \ = \ t \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ recursive} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & f \ \overline{v}_1 \ sp_1 \ \overline{w}_1 \ = \ t_1; \ \ldots;
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ f \ \overline{v}_n \ sp_n \ \overline{w}_n \ = \ t_n \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ recursive} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & f_1 \ v_1::\tau \ \overline{w_1} \ = \ t_1; \ ldots; \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich f_n \ v_n::\tau \ \overline{w_n} \ = \ t_n \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{where} \ f_1::\phi_1, \ldots, f_n::\phi_n \ \mbox{are \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich totally \ defined, \ mutually} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{primitive \ recursive \ in \ the \ first \ argument, \ and \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad 0 < i \leq n \ \mbox{there \ exists \ type
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ variable \ renaming} \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \sigma_i \ \mbox{such} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{that} \ \tau_1 = \sigma_i(\tau_i) \ \mbox{and \ all \ the \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich variables \ in} \ \phi_i \ \mbox{appear \ in} \ \tau_i \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & instance \ ctx \Rightarrow K \ \tau \ where \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (f_1 = t_1; \ldots; \ f_n = t_n) \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{where} \ f_1, \ldots, f_n \ \mbox{are \ totally \ defined, \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich primitive \ recursive} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{methods \ of} \ K
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{array}$$\\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\noindent Terms
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich$$\begin{array}{ll}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich x::\tau & \Longrightarrow \ x'::\tau' \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich () & \Longrightarrow \ Def \ () \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich True & \Longrightarrow \ TT \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich False & \Longrightarrow \ FF \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \&\& & \Longrightarrow \ trand \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich || & \Longrightarrow \ tror \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich not & \Longrightarrow \ neg \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich c & \Longrightarrow \ Def \ c \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich t \in \{+,-,*,div,mod,<,>\} & \Longrightarrow \ fliftbin \ t \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich negate & \Longrightarrow \ flift2 \ - \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich {[]} & \Longrightarrow \ nil \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich t:ts & \Longrightarrow \ t'\#\#ts' \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich head & \Longrightarrow \ HD \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich tail & \Longrightarrow \ TL \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich == & \Longrightarrow \ hEq \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich /= & \Longrightarrow \ hNEq \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Just & \Longrightarrow \ return \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Nothing & \Longrightarrow \ fail \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich C & \Longrightarrow \ C' \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich f & \Longrightarrow \ f' \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \backslash \overline{x} \ \to \ t & \Longrightarrow
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ LAM \ \overline{x}'. \ t' \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich t_1 \ t_2 & \Longrightarrow \ t'_1 \ \cdot \ t'_2 \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (t_1,t_2) & \Longrightarrow \ (t'_1, \ t'_2) \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich fst & \Longrightarrow \ cfst \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski snd & \Longrightarrow \ csnd \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski let \ (x_1 = t_1; & \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \qquad \dots; & \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \qquad x_n = t_n) \quad in \ t & \Longrightarrow
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ let \ (x'_1 = t'_{1}; \ \dots; \ x'_n = t'_{n}) \ in \ t' \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich if \ t \ then \ t_1 \ else \ t_2 & \Longrightarrow
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ If \ t' \ then \ t'_1 \ else \ t'_2 \ fi \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich case \ x \ of \ (p_1 \to t_1; & \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \qquad \qquad \ldots; & \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \qquad \qquad p_n \to t_n) & \Longrightarrow
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Rightarrow t'_n \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{if} \ p'_1, \ldots, p'_n \neq \_ \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \mbox{is \ a \ complete \ match} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & case \ x' \ p'_1 \Rightarrow t'_1 \ | \ \ldots \ | \ p'_{n-1}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Rightarrow t'_{n-1} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \qquad \qquad | \ q_{1} \Rightarrow t'_n
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \ | \ \ldots \ | \ q_{k} \Rightarrow t'_n \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich p'_{n-1}, q_1, \ldots, q_k \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{complete \ match} \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & case \ x' \ p'_{1} \Rightarrow t'_1 \ | \ \ldots \ | \ p'_n
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Rightarrow t'_n \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder & \qquad \qquad \qquad | \ q_{1} \Rightarrow \bot \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | \ \ldots q_{k} \Rightarrow \bot \\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich & \qquad \mbox{with} \ p'_1, \ldots, p'_{n}, q_1, \ldots, q_k \
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \mbox{complete \ match}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{array}$$\\