hs2isa.tex revision 5175cc8f6f6980c8f39123859284391ff51f5f55
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Author: Paolo Torrini <paolot@helios.dai.ed.ac.uk>
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Created: Mon Feb 15 1999
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\documentclass[a4paper,12pt]{article}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage[dvips]{graphics}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{amsfonts}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{amssymb}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%\usepackage{psfig}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{fancybox}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{epsfig}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{graphicx}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{color}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%\usepackage{semrot}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Use \includegraphics{*.eps} for pictures
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Enlarge printing area a bit:
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\textwidth}{16cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\oddsidemargin}{0cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\evensidemargin}{0cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\topmargin}{-0.94cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\textheight}{23cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\begin{document}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\title{Translating Haskell programs to Isabelle by shallow embedding}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\author{Paolo Torrini, Till Mossakowski, Christian Maeder}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% \\ Fachbereich Mathematik und Informatik, Universitaet Bremen}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\abstract{\small We present a tool for the translation of Haskell
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini programs to Isabelle HOLCF and Isabelle HOL based on a shallow
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini embdedding approach, implemented as part of the Hets system, on top
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini of the static analysis
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini carried out by Programatica. The translation of monads uses the AWE extension of Isabelle.}\\
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\noindent It has been suggested that, owing to their relative
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisemantical simplicity, programs written in functional languages are a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininatural target for verification \cite{Thompson95}. Haskell is indeed a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinistrongly typed, purely functional language with lazy evaluation, based
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinion a type system of polymorphic types with type and type constructor
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniclasses, where side effects are modelled using monads (introduced as a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitype costructor class), and allowing for a pseudo-imperative
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprogramming style (do notation) \cite{Hudak}.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% other words, we need to represent the program in a mechanised logic in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% which the requirements can be expressed, as well.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% The representation can take different forms. It is possible to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% associate the state-machine behavioural description to models in a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% logic. Another possibility is to represent the program in terms of a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% computational logic based on the operational semantics of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% In both cases however, a significant part of the work has to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% be carried out before the actual verification may take place.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn order to verify a program, we need to associate its code to a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilogical representation that allows for requirements to be expressed
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand for proofs to be carried out. There are different ways to do this.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe way we carry this out here is to embed Haskell into an expressive
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinihigher-order logic, together with providing an implementation of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniembedding that allows for an automated translation of Haskell. From
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe theoretical point of view, the correctness of the embdedding
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidepends on the denotational semantics of the language. From the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipractical point of view, once the program code can be translated
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniautomatically to the logic, all the burden of the verification can
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirest on the theorem proving.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniDepending on the expressiveness of the logic, the translation of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprogrmaming language may be carried out at different levels of depth.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn general, the deeper is the embedding, the less it relies on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimeta-level features of the target language. This may be a plus from
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe point of view of semantic clarity. Taking advantage of meta-level
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifeaures, on the other hand, may be useful in order to make the theorem
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniproving less tedious.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle is a generic theorem-prover written in SML that allows for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe formalisation of a variety of logics \cite{Paulson94isa}.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle-HOL is the implementation of classical higher-order logic
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibased on simply typed lambda calculus, extended with axiomatic type
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniclasses. Isabelle-HOLCF \cite{holcf} is HOL extended with a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniformalisation of the theory of computable functions (LCF) based on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaxiomatic type classes.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHets \cite{Hets} is a parsing, static analysis and proof management
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitool designed to interface with various language specific tools, in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniorder to support heterogeneous specification. In particular, for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniparsing and static analysis of Haskell programs Hets relies on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniProgramatica \cite{PTeam}, a tool that has its own proof management,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniincluding a translation of Haskell to Isabelle-HOLCF.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn the following, we present translations of Haskell into some of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle logics. These translations are implemented as part of Hets,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand are based on a shallow embedding approach quite different from
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithat used in Programatica. In our translations Haskell types are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimapped to Isabelle types. We are assuming that the type systems of HOL
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand HOLCF are similar enough to the type system of Haskell, in order
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinito guarantee the semantical correctness of our translations. Moreover,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwe rely on axiomatic classes to translate Haskell types classes.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniA type class in Isabelle is conceptually quite different from one in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell. The former is associated to a set of axioms, whereas the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilatter is associated to a set of function declarations. Isabelle
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininot allow for type constructor classes. The last limitation is the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimost serious of the three, since it makes quite hard to cope with
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimonads. We can get around this obstacle relying on a method for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniParametrisation based on theory morphism has been implemented, as a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidesigned to support proof reuse \cite{AWE}.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe translation to HOLCF differs from that to HOL insofar as only the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifirst one relies on a denotational semantics for the full language,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinikeeping into account partiality and lazy evaluation, and associating
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirecursive functions to corresponding fixed points, using on the Fixrec
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniextension of HOLCF. The translation to HOL is more restrictive; it
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidoes not keep into account any form of partiality, and it restricts
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslation of recursive functions to the primitive recursive ones.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIt would have been possible to give an account of partiality in HOL by
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniusing option types. However, we chose to keep the HOL translation as
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisimple as possible for didactic purpose.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThese translations are on the overall quite different from other ones
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibased on deep embeddings, particularly from the Programatica
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslation of Haskell into HOLCF \cite{Huff}, where the type system
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniis modelled at the logical level, as well as from translations of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniMiranda and Haskell into FOL (Isabelle classical first-order logic)
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwhere higher-order features have to be dealt with less directly
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\cite{Thompson95,Thompson92}.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\section*{The hs2thy tool}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini(suggested change: from h2hf to hs2thy)
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe tool is designed to support the translation of simple but
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirealistic Haskell programs to HOLCF and, with some restriction, to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOL. Not all the syntactical features of Haskell are covered yet,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinialthough most of those used in the Prelude are. The most noticeable
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilimitations are related to built-in types, pattern-matching and local
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefinitions. There are additional and more substantial restrictions
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniin the case of HOL, related to termination and to recursion.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe application can be installed as part of Hets. It requires Haskell
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniGHC and Programatica. It is run by the command \emph{h2hf
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini [h|hc|mh|mhc] file.hs} where the options stand, respectively, for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOL, HOLCF, HOL extended with AWE and HOLCF extended with AWE.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFor the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimodule that contains the main translation function, carried out as
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitheory translation after a preliminary step of signature translation,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand \emph{IsaSign.hs} contains the internal representation of Isabelle
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Type signature}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniOur general strategy for translating signatures is to map Haskell
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitypes to Isabelle defined types. The translation to HOLCF keeps into
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaccount the fact that Haskell expressions are evaluated lazily. The
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslation to HOL does not, and moreover requires that all the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunctions defined in the Haskell program are total ones...
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniAll types have a sort in Isabelle, defined by the set of the classes
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniof which it is a member. In HOL, all types belong to the class type;
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniin HOLCF, they belong to class pcpo (pointed complete poset).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniAll Haskell function declarations are translated to Isabelle ones.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniType variables are assigned default sort type in HOL and pcpo in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOLCF. Names get translated by a function that preserves them, up to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniavoidance of clashes with Isabelle keywords.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe only built-in types that are properly covered are booleans,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniunbounded integers and rationals. These get translated, in the case of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOL, to Isabelle booleans, integers and rationals, respectively. Bound
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniintegers and floating point numbers would require low-level modelling,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand have not been dealt with; anyway, bounded integers are accepted
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand simply treated as unbounded by the application.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn the HOLCF translation, all built-in types get lifted to the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicorresponding domains (pcpos), which by definion include the undefined
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinivalue, by using the lift HOLCF type constructor. In particular, type
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniboolean get translated to type tr (short for bool lift), and similarly
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifor types integer and rational.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniRecursive data-types declarations can be translated to datatype
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclarations in HOL. In HOLCF they can be translated to domain
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclarations. The two structure are quite similar, except that in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidomains, which are pcpo, all the parameters are required to be pcpos
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinias well. Morevover, Isabelle domain declarations require to introduce
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininames for destructors. Mutually recursive Haskell datatypes can be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslated to both logics, relying on the specific Isabelle syntax for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Function definitions}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell function definitions are translated to corresponding Isabelle
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniones. Non-recursive definitions are translated to ordinary definitions
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini(keyword \emph{defs}), whereas recursive ones require specific
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinikeywords. The type of the function, inclusive of class annotation, is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniincluded in each of its definitions in order to allow for overloading.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn the translation to HOLCF, when the Haskell value is of built-in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitype, the translated value has the lifted corresponding type --- this
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniis either the case of a lifted value (where \emph{Def} is the lifting
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunction) or the case of the undefined value (\emph{UU}).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniAs to local definitions, they can be introduced in Haskell by let and
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwhere expressions. Let expressions are translated to Isabelle let
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniexpressions, whereas where expressions are not covered.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Recursive definitions}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniRecursive defitions is the topic that really sets HOL and HOLCF apart.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn HOLCF, where every type is a domain and every function is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicontinuous, all recursive functions can be defined by fixpoint
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinioperator. This is essentially a function that, given as argument the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunction definition body abstracted of the recursive call name,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinireturns the corresponding recursive function. Coding this directly
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwould be rather cumbersome, particularly in the case of mutually
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirecursive functions, where tuples of definition bodies and tupled
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniabstraction are needed. We can instead rely on the \emph{recdef}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipackage, which allows to handle fixpoint definitions like ordinary
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirecursive ones, offering nice syntax to deal with mutual recursion as
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe case of HOL is more compplex. There a distinction must be drawn
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibetween primitive recursive functions and generic recursive ones. In
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe formers, termination is guaranteed by the fact that recursive
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefinitions are strictly associated with the datatype structure of a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniparameter. In the latters, termination needs to be proved. This can be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidone, in a \emph{recdef} definition, by providing a measure for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunction parameter that can be proved to be strictly decreasing for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinieach occurrence of a recursive call in the definition. This requires a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinigenerally unbounded amount of ingenuity and cannot be carried out by a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisimple translation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFor this reason, the translation of recursive functions to HOL is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestricted to primitive recursive ones. Mutually recursive functions
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniare allowed under additional restrictions. These are: all the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunctions should be recursive in the first argument, this should be of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe same type for each of them, the constructors should be listed in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe same order in each of the case expressions, and also the variable
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininames in the case patterns are expected to be maintained.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe translation of mutually recursive functions $a \rightarrow b, \ldots a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefined, for each case pattern, as the product of the values
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicorrespondingly taken by the original functions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Pattern matching}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniSupport of pattern-matching in Isabelle is more restricted than in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell. Nested patterns are disallowed; case expressions are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisensitive to the order of the constructors, which should be the same
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinias in the datatype declaration. In particular, the case variable si
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirequired to be a variable. Translation of pattern-matching is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipotentially laborious. For this reason guarded expressions, list
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicomprehension and nested pattern-matching have been left out; they can
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibe replaced without loss, anyway, using conditional expressions and
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimap functions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFunction definition by top level pattern matching is not allowed in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle with ordinary definitions, but it is with those that are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniexplicitly declared to be recursive ones. However, particularly in HOL
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprimitive recursive definitions patterns are allowed in one parameter
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinionly. In order to translate function definitions with patterns in more
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithan one parameter, without resorting to using tuples and more complex
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefinitions (\emph{recdef} instead of \emph{primrec}), our
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslations turn a multiple definition by top level pattern matching
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniinto a definition by case construct.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Classes}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell classes and instances are translated to Isabelle,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirespectively, as classes with empty axiomatisation and as instances
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwith trivial instantiation proof. The translation supports only
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisingle-parameter classes --- in principle, more than one parameter
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicould be handled using tuples.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinihowever here is not provided.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFunctions declarations associated to classes are translated to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle as independent function declarations with appropriate class
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniannotation. Function definitions associated to instances are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslated as overloaded function definitions, relying on class
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniannotation of typed variables.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Monads}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle does not allow for classes of type constructors, hence a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniproblem in representing monads. We can deal with this problem,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinihowever, relying on an axiomatisation of monads that allows for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipresentation of monadic types as an axiomatic class, as provided in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\cite{}. Therefore, monadic types can be translated to newly defined
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitypes that are constrained to satisfy the monadic axioms. This
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniconstraining, carried out as an instantiation of type variables in the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitheory of monads, takes the form of a theory morphism, and can be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicarried out automatically by AWE, an implementation of parametrisation
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand theory morphism on top of Isabelle basic logic, that may also be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniused to extend HOL and HOLCF. The do notation can then be translated
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniby unpacking it into monadic operators. Attempting to translate
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimonadic notation without support AWE support will result in an error
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\section*{Conclusion}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe following is a list of constructs that are covered by all the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\begin{itemize}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item predefined types: boolean, integer.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item predifed type constructors: funtion, cartesian product, list.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item declaration of recursive datatype, including mutually recursive ones.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item predefined functions: equality, booelan constructors,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini connectives, list constructors, head and tail list functions,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini arithmetic operations.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item non-recursive functions, including conditional,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilet and case expressions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item use of incomplete patterns (HOLCF) and of wildcards in case
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item total primitive recursive functions (HOL)
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand partial recursive ones (HOLCF), including mutual ones (with
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestrictions in the HOL case).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item class and instance declarations.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item monad declarations and do notation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe shallow embedding approach used by our translations should allow
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinito take as much advantage as possible of the automation currently
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniavailable on Isabelle, particularly in HOL.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFurther work should include extending the translation to cover the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwhole of the Haskell Prelude. We hope that this will make it possible
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinito support the verification of functional robotics programs.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniA further extension, in line with the work on Programtica, would be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe translation of P-logic. This translation, due to the character of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe P-logic typing system, could be more easily carried out relying on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisome form of universal quantification on type variables, or else
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifurther relying on parametrisation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\bibliographystyle{alpha}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\bibliography{case}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\end{document}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe Haskell classes Eq and Ord are translated to corresponding classes
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclared, respectively, in HsHOL.thy and HsHOLCF.thy. These classes
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifor the moment are taken to be absolutely generic ones (with empty
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaxiomatisation).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Isabelle-HOL}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle-HOL as an implementation of classical higher-order logic
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisupports the definition of datatypes and recursive functions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHowever, it distinguishes between primitive recursion (keyword
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniemph{primrec}), in which termination is trivially guaranteed by
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidecrease in the complexity of a parameter, and recursion (keyword
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniemph{recdef}) for which an appropriate specific measure must be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprovided in order to get the termination proof to go through.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniMoreover, HOL does not have a notion of undefined suitable for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicomputations --- therefore all functions have to be total.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThis translation of recursive functions is restricted to total
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprimitive recursive functions that are recursive in their first
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidatatype argument. The Haskell definition should be a case expression
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniin which all the constructors are considered in their datatype
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclaration order, save for the use of a wildcard.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%Wildcards cannot be used for constructor arguments.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%Moreover, the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%case variable should not be used in the specific case expression (just
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%replace it with the specific case pattern).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniMutually recursive functions are allowed under additional
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestrictions. All the functions should be recursive in the same type,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe constructors should be listed in the same order in each of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicase expressions, and also the variable names in the case patterns are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniexpected to be maintained.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe translation of mutually recursive functions $a \rightarrow b, \ldots a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefined, for each case pattern, as the product of the values
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicorrespondingly taken by the original functions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\subsection*{Isabelle-HOLCF}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle-HOLCF is the implementation of the theory of computable
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunctions on top of higher-order logic, relying on axiomatic classes.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn comparison with HOL, the handling of partial functions is more
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininatural, and the presence of the fixpoint operator allows for a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinigeneral treatment of recursive functions. However, types in HOLCF can
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibe interpreted as pointed complete partial orders (pcpo), and this
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirequires all standard types to be lifted.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn the present translation, the type constructor \emph{lift} is used
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinito lift types, in association with the corresponding lifting function
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\emph{Def} and with the undefined value \emph{UU}. Datatypes are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslated to domains --- complete with destructors from declaration.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe class \emph{pcpo} is added to the sort of each type variable.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniPartial recursive functions (defined by case expressions), including
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimutually recursive ones, are covered without any essential
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestrictions, relying on the recdef package.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\end{document}