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