hs2isa.tex revision c60dd75d214d1b29462ee2262d4e0f468a962450
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Author: Paolo Torrini <paolot@helios.dai.ed.ac.uk>
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Created: Mon Feb 15 1999
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\documentclass{llncs}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%%\documentclass{/home/polh/Documents/Hs2Isa/llcns}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%%\documentstyle{/home/polh/Documents/Hs2Isa/llcns}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo 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}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%\input{newmacros}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Use \includegraphics{*.eps} for pictures
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\begin{document}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\title{Translating Haskell into Isabelle}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\author{Paolo Torrini, Till Mossakowski, Christian Maeder}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\institute {Informatik, Universitaet Bremen}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\abstract{\scriptsize \bf Two partial translations of Haskell into Isabelle
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini higher-order logics have been implemented as functions of Hets, a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini Haskell-based system for proof-management and program development that
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini allows for integration with other verification tools. Our application can
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini translate simple Haskell programs to HOLCF and, under stronger restrictions,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini to HOL. Both translations use the static analysis of Programatica and are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini based on a shallow embedding of denotations.}\\
984e73d7bd9693bb0f113d956969b7d1483f5925Paolo Torrini% The translation of monads uses the AWE extension of Isabelle.}\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniTranslations between programming and specification languages, as well as the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicorresponding integration of compilers, analyzers and theorem-provers, can
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniprovide useful support to the formal development and verification of programs.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThis task involves translating programs to a logic in which requirements can
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinibe expressed, in order to prove the corresponding correctness statements.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniProgram translation should rest on a formal semantics of the programming
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilanguage allowing for proofs that are as easy as possible. In fact, it has
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilong been argued that functional languages, based on notions closer to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinigeneral, mathematical ones, can make the task of proving assertions on them
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinieasier, owing to the relative clarity and simplicity of their semantics
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\cite{Thompson92}.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIn the following we are presenting automated translations of Haskell programs
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniinto Isabelle higher-order logics that can be justified in terms of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidenotational semantics. Haskell is a strongly typed, purely functional
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilanguage with lazy evaluation, polymorphic types extended with type
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniconstructor classes, and a syntax for side effects and pseudo-imperative code
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinibased on monadic operators \cite{HaskellRep}. The translations are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniimplemented as functions of Hets \cite{Hets}, an Haskell-based application
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidesigned to support heterogeneous specification and formal development of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniprograms. Hets supplies with parsing, static analysis and proof management, as
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwell as with interfaces to various language-specific tools. As far as
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniinteractive proofs are concerned, it relies on an interface with Isabelle, a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinigeneric theorem-prover written in SML that includes the formalization of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniseveral useful logics \cite{Paulson94isa}. Moreover, Hets relies on
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniProgramatica \cite{Prog04} for the parsing and the static analysis of Haskell
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniprograms. Programatica (built at OGI) is another Haskell-specific system for
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniformal development and it has a proof management on its own, including a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinispecification logic and translations to different proof tools, notably to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle \cite{Huff}, albeit following a different approach from ours (see
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinisection~\ref{sec:Translations}).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Isabelle}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle-HOL (hereafter HOL) is the implementation in Isabelle of classical
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinihigher-order logic based on simply typed lambda calculus extended with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaxiomatic type classes. It provides considerable support for reasoning about
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniprogramming functions, both in terms of rich libraries and efficient
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniautomation. Since the late nineties, it has essentially superseded FOL
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini(classical first-order logic) in standard use. HOL has an implementation of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirecursive functions based on Knaster-Tarski fixed-point theorem. All functions
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniare total; partiality may be dealt with by lifting types through the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{option} type constructor.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniOn the other hand, HOLCF \cite{holcf} is HOL conservatively extended with the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilogic of computable functions --- a formalization of domain theory. In HOL,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitypes --- elements of class \emph{type} --- are just sets; functions may not
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinibe computable, and a recursive function may require discharging proof
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniobligations already at the stage of definition --- in fact, a specific measure
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinihas to be given for the function to be proved monotonic. In contrast, HOLCF
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinihas each type interpreted as an element of class \emph{pcpo} (pointed complete
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinipartially ordered sets) i.e. as a set with a partial order which is closed
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniw.r.t. $\omega$-chains and has a bottom. In particular, the Isabelle
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniformalization of HOLCF is based on axiomatic type classes \cite{Wenzel},
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimaking it possible to deal with complete partial orders in quite an abstract
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniDomain theory offers a good basis for the semantical analysis of programming
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilanguages. All functions defined over domains, including partial ones, are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicontinuous, therefore computable. Recursion can be expressed in terms of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinileast fixed-point operator, and so, in contrast with HOL, function definition
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidoes not depend on proofs. Nevertheless, proving theorems may turn out to be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomparatively hard. After being spared the need to discharge proof
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniobligations at the stage of giving definitions, one has to bear with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniassumptions over the continuity of functions while actually carrying out the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniproofs. A standard strategy to get the best out of the two systems, is to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefine as much as possible in HOL, using HOLCF type constructors to lift types
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinionly when this is necessary.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Translations}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:Translations}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniTranslations can depend on the expressiveness of the target logic. As
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniexamples, the translations into FOL of Miranda
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\cite{Thompson95,Thompson89,Thompson95b} and Haskell \cite{Thompson92}, both
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinibased on large-step operational semantics, appear to struggle with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinihigher-order features such as currying. The translation of Haskell to the Agda
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniimplementation of Martin-Loef type theory in \cite{Abel} seems to struggle
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwith Haskell polymorphism. Higher-order logic may in fact quite help overcome
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisuch obstacles. It also allows for higher-level approaches based on
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidenotational semantics, such as already proposed in \cite{Huff} for a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslation of Haskell into HOLCF, and in \cite{Pollack} for a translation of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniML into HOL. By using denotational semantics, one may hope to give
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirepresentations of programs that are closer to their specification, and to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinigive proofs that are relatively more abstract and general.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniA shallow embedding into a logical language is one that relies heavily on its
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniextra-logical features, possibly taking advantage of built-in packages
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniprovided with the implementation of that language, particularly with respect
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinito types and recursion. On the contrary, a deep embedding relies on the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilogical definition of all the relevant notions. This may give a plus in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisemantical clarity and possibly, provided the logic is expressive enough, in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinigenerality as well. Taking advantage of built-in features, on the other hand,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimay help make theorem proving less specific and tedious.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe translation of ML in \cite{Pollack} based on the definition of a class of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitypes with bottom elements in HOL gives an example of the deep sort. The
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslation of Haskell to HOLCF proposed in \cite{Huff} relies on a generic
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniformalization of domain theory and particularly on the \emph{fixrec} package
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifor recursive functions, created to provide a friendly syntax covering also
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimutually recursive definitions. However, in order to capture type constructor
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniclasses --- an important feature of the Haskell type system --- a deep
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniembedding approach is used there, as well. Haskell types are translated to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniterms, relying on a domain-theoretic modelling of the type system at the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniobject level. The practical drawback of this approach is that it leads to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniplenty of the automation built into Isabelle type checking needing to be
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinireimplemented.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIn contrast with \cite{Huff}, both the translations of Haskell to HOLCF and
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHOL presented here are based on a shallow embedding approach. In the case of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHOLCF we use as well the \emph{fixrec} package. Moreover, we tend to rely as
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimuch as possible on similarities between type systems, translating Haskell
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitypes to HOLCF types in a comparatively direct way. Haskell classes are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslated to Isabelle axiomatic classes. Since we are trying to keep things
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinias simple as possible, the modelling we rely on is not very deep either: our
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniclaim is that the equivalence between Haskell programs and their translation
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinito HOLCF can be justified up to the level of typeable output. This translation
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicovers a significant part of the syntax used in the Prelude, however there are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniseveral limitations related to built-in types, pattern-matching, local
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefinitions, import and export. In particular, it does not cover type
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniconstructor classes yet, although we have plans for an extention that should
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaddress this aspect.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe translation to HOL, similar in matter of shallow approach, is nevertheless
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimuch more limited. First, it only covers primitive recursive functions. This
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilimitation appears relatively hard to overcome, given the way syntax for full
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirecursion is defined in HOL. Moreover, we have to restrict to total functions.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniOperational equivalence for a larger fragment could be obtained using option
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitypes, but this is not pursued here.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\section{Translations in Hets}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniInformation about Hets may be found in \cite{HetsUG} and \cite{HetsUG}. The
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell-to-Isabelle translation requires GHC, Isabelle 2006 and Programatica.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe command to run the application is
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{hets -v[1--5] -t Haskell2Isabelle[HOLCF | HOL] -o thy out in.hs}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent where arguments set options for verbosity, the logic, extension and name of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithe output file, the last one being the input --- a Haskell program given as a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniGHC file (\emph{in.hs}). This gets analyzed and translated, the result of a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisuccessful run being an Isabelle theory file (\emph{out.thy}) in the given
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%The application requires essentially Haskell GHC and Programatica. It
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%is run by the command \emph{hets -t ... [h|hc] file.hs} where the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%options stand for HOL and HOLCF, respectively.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe internal representation of Haskell in Hets (modules \emph{Logic\_Haskell}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniand \emph{HatAna}) is the same as in Programatica, whereas the internal
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirepresentation of Isabelle (modules \emph{Logic\_Isabelle} and \emph{IsaSign})
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniis essentially a Haskell reworking of the ML definition of Isabelle's own base
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilogic, extended in order to allow for a straightforward representation of HOL
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell programs and Isabelle theories are internally represented as Hets
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitheories --- each of them formed by a signature and a set of sentences,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaccording to the theoretical framework described in \cite{MossaTh}. Each
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslation, defined in module \emph{Haskell2IsabelleHOLCF} as composition of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinia signature translation with a translation of all sentences, is essentially a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimorphism from theories in the internal representation of the source language
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinito those in the representation of the target language. The module
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{IsaPrint} contains functions for the pretty-printing of Isabelle
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniEach translation relies on an Isabelle theory, respectively \emph{HsHOLCF},
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniextending HOLCF, and \emph{HsHOL}, extending HOL, which contain some useful
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrininotions --- notably definitions of lifting functions and an axiomatisation for
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell equality.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\section{Naming conventions} \label{section:nam}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniNames of types as well as of terms are translated by a renaming function that
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinipreserves them, up to avoidance of clashes with Isabelle keywords. We also
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinineed to reserve a few names, as follows.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini1) Names for type variables, in the translation to HOL: \emph{'vX}; any string
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniterminating with \emph{'XXn} where $n$ is an integer.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini2) Names for term constants, in the translation to HOL: strings obtained by
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinijoining together names of defined functions, using \emph{\_X} as end sequence
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniand separator.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini3) Names for term variables, in both translations: \emph{pXn}, \emph{qXn},
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwith $n$ integer.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini4) Names for type destructors, in the translation to HOLCF: \emph{C\_n},
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwhere \emph{C} is a data constructor name and $n$ is an integer.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Correspondingly, the translation function is defined as the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%composition of signature translation with the translation of all
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%structure of a morphism from Hets theories written in the language of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%the source internal representation to those in the language
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%representation of the target language. Internally, the information
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%about types is collected into a signature, whereas datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%declarations and definitions are associated with sentences.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% module that contains the main translation function, carried out as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% composition of a signature morphism and a theory morphism.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \emph{IsaSign.hs} contains the Hets representation of the Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% base logic and extensions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% The general design of the translation functions, and particularly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% the two-layered recursion adopted for them, is similar to that used
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% for the translation Haskell to Agda in Programatica.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\subsection{Types}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniOur type translation are shallow and based on relative similarity of type
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisystems. Isabelle, as well as Haskell, is based on simple types with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinipolymorphism (which means, essentially, type variables, function and product
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitypes). They both have built-in types for Boolean values and integers, and a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitype constructor for lists. Both allows for sums, recursive and mutually
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirecursive types in the form of datatype declarations. Finally, they both have
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinia class mechanism --- although not quite the same.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe translation to HOLCF keeps into account partiality, i.e. the fact that a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifunction might be undefined for certain values, either because definition is
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimissing, or because the program does not terminate. It also keeps into
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaccount laziness, i. e. the fact that by default function values in Haskell
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniare passed by name and evaluated only when needed. However, the idea that
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniunderlies the translation is rather a simplifying one: although raising an
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniexception is different from running forever, and both are different from
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinistopping short of evaluation, still, from the point of view of the printable
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinioutput of ground types, these behaviours are similar and can be treated
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisemantically as such, i.e. using one and the same bottom element. So,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniessentially, we are following the main lines of the ``crude'' denotational
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisemantics for lazy evaluation in \cite{winskel}, pp. 216--217.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% In order to ease the translation of some notions, the Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% theory \emph{HsHOLCF.thy}, that extends HOLCF has been defined and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% included in the Hets distribution.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% It is often convenient to define in Isabelle notions that match the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% translation of some itmes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% Haskell datatype and function declarations are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% declarations in HOLCF. Names are translated by a function that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% preserves them, up to avoidance of clashes with HOLCF keywords.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell type variables are translated to HOLCF ones, of class \emph{pcpo}.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniEach type in Isabelle has a sort, defined by the set of the classes of which
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniit is a member. Each built-in type is translated to the lifting of its
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicorresponding HOL type. The translation covers properly only Haskell Booleans
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniand unbounded integers, respectively associated to HOL Booleans and integers.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniBound integers and floating point numbers would require low-level modelling,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniand have not been covered. Bounded integers are simply treated as unbounded.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe HOLCF type constructor \emph{lift} is used to lift HOL types to flat
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidomains. In the case of Booleans, HOLCF provides with type \emph{tr}, defined
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinias $bool \ lift$. In the case of integers, we define \emph{dInt} as $int \
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilift$ in \emph{HsHOLCF}. The types of Haskell functions and product are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslated, respectively, to HOLCF function spaces and lazy product --- i.e.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisuch that $\bot = (\bot * \bot) \neq (\bot*'a) \neq ('a * \bot)$, consistently
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwith lazy evaluation. Type constructors are translated to corresponding HOLCF
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniones (notably, parameters precede type constructors in Isabelle syntax). In
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniparticular, lists are translated to the domain \emph{llist} defined in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{HsHOLCF}.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini% H%Rationals need to be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%imported in order to be used in Haskell, so they are not covered by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%the translation at the present stage (import has not been dealt with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%and rationals.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniType translation to HOLCF, apart from mutual dependencies, may be summed up as
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifollows (where $t$ is a renaming function):
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% Haskell datatype and function declarations are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% declarations in HOLCF.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lcl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \rceil & = & 'a_{t}::pcpo \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil Bool \rceil & = & tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil Integer \rceil & = & dInt \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \to b \rceil & = & \lceil a \rceil \to \lceil b \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil [a] \rceil & = & \lceil a \rceil \ llist \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe translation to HOL is more crude. It takes into account neither partiality
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrininor laziness; therefore, we need to require that all functions in the program
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniare total ones. An account of partiality could be obtained, but here it is
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrininot, using the \emph{option} type constructor to lift types, along lines
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisimilar to those followed in HOLCF with \emph{lift}.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell types are mapped into corresponding, unlifted HOL ones --- thus so for
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniBooleans and integers. All variables are of class \emph{type}. HOL function
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitype, product and list are used to translate the corresponding Haskell
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniconstructors. Type translation to HOL, apart from mutual dependencies, may be
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisummed up as follows.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$$\begin{array}{lcl}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini \lceil a \rceil & = & 'a_{t}::type \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini \lceil Bool \rceil & = & bool \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini \lceil Integer \rceil & = & int \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini \lceil a \to b \rceil & = & \lceil a \rceil \Rightarrow \lceil b \rceil \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini \lceil [a] \rceil & = & \lceil a \rceil \ list \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Under each translation, function declarations
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniare associated, by using the keyword \emph{consts}, to the corresponding ones
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniin HOLCF and HOL, respectively. Datatype declarations are associated to the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicorresponding ones, as well, but this involve some difference in the two
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicases. In HOLCF datatype declarations define types of class \emph{pcpo} by the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinikeyword \emph{domain} (hence we may call them \emph{domain declarations}). In
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHOL they define types of class \emph{type} by the keyword \emph{datatype}.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniNotably, in contrast with Haskell and HOL, HOLCF datatype declarations require
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinian explicit introduction of destructors; these are provided automatically
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaccording to the naming pattern in Section~\ref{section:nam}, point 4. Apart
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifrom this aspect, the meta-level features of the the two type translations are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniessentially similar.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniTranslation of mutually recursive datatypes, as the one shown in the following
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniexample, relies on specific Isabelle syntax (using the keyword \emph{and}).\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$data \ AType \ a \ b \ = \ ABase \ a \ | \ AStep \ (AType \ a \ b) \ (BType \ a \ b) $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$data \ BType \ a \ b \ = \ BBase \ b \ | \ BStep \ (BType \ a \ b) \ (AType \ a \ b) $\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Translation to HOLCF gives the following.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rr} domain & \ ('a::pcpo, 'b::pcpo) \ BType \ = \ BBase \ (BBase\_1::'b) \ | \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & BStep \ (BStep\_1::('a, 'b) \ BType) \ (BStep\_2::('a, 'b) \ AType) \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini and & \ ('a::pcpo, 'b::pcpo) \ AType \ = \ ABase \ (ABase\_1::'a) \ | \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & AStep \ (AStep\_1::('a, 'b) \ AType) \ (AStep\_2::('a, 'b) \ BType) \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Translation to HOL gives the following.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$$\begin{array}{rll} datatype & \ ('a, 'b) \ BType & = \ BBase \ 'b \ | \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & BStep \ (('a, 'b) \ BType) \ (('a, 'b) \ AType) \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini and & \ ('a, 'b) \ AType & = \ ABase \ 'a \ | \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & AStep \ (('a, 'b) \ AType) \ (('a, 'b) \ BType) \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent In contrast with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell, order of declarations matters in Isabelle, where they should always
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinibe listed according to their dependency. Both translations take care of this
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaspect automatically.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOLCF: Sentences}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniEssentially, each function definition is translated to a corresponding ones.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniNon-recursive definitions are translated to standard Isabelle definitions
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini(introduced by the keyword \emph{defs}), whereas the translation of recursive
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefinitions relies on the \emph{fixrec} package. Lambda abstraction is
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslated as continuous abstraction (\emph{LAM}), function application as
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicontinuous application (the \emph{dot} operator). These notions coincide with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithe corresponding ones in HOL, i.e. with lambda abstraction (\emph{\%}) and
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinistandard function application, whenever all arguments are continuous.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% As to the translation of terms containing either values or operators
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% of built-in type, it is often the case that we translate them to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% lifted HOL operators. The lifting function is \emph{Def}; $\bot$ is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% used for the undefined case.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniTerms of built-in type (Boolean and integer) are translated to lifted HOL
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinivalues, using the HOLCF-defined lifting function \emph{Def}. The bottom
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinielement $\bot$ is used for all the undefined terms. We use the following
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinioperator, defined in \emph{HsHOLCF}, to map binary arithmetic functions to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilifted functions over lifted integers.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \Rightarrow ('a \ lift \to \ 'b \ lift \to \ 'c \ lift) $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$fliftbin \ f \ == \ LAM \ y x. \ (flift1 \ (\%u. \ flift2 \ (\%v. \ f \ v \ u))) \cdot x \ \cdot y $\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Boolean values are translated to values of \emph{tr} --- i.e.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{TT}, \emph{FF} and $\bot$. Boolean connectives are translated to the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicorresponding HOLCF lifted operators. HOLCF-defined \emph{If then else fi} and
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{case} syntax are used to translate conditional and case expressions,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirespectively. There are some restrictions, however, on the latter, due to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinilimitations in the translation of patterns (see Section~\ref{sec:Patterns});
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniin particular, the case term should always be a variable, and no nested
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipatterns are allowed.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe translation of lists relies on the following domain, defined in \emph{HsHOLCF}.\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$domain \ 'a\ llist \ = \ lNil \ | \ lCons \ (lHd :: \ 'a) \ (lTl :: \ 'a \ llist) $\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Under the given interpretation, an infinite list as well as
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinian undefined one evaluate to $\bot$. However, the value of finite prefixes,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniand particularly the printable output associated to them, will be the expected
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinione, since the model of evaluation is lazy.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell allows for local definitions by means of \emph{let} and \emph{where}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniexpressions. Those \emph{let} expressions in which the left-hand side is a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinivariable are translated to similar Isabelle ones; neither other \emph{let}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniexpressions (i.e. those containing patterns on the left hand-side) nor
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{where} expressions are covered. The translation of terms (minus mutual
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirecursion) may be summed up, essentially, as follows:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lcl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil c \rceil & = & c_{t} \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil \backslash x \ \to \ f \rceil & = & LAM \ x_{t}. \ \lceil f \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil f \ a_{1} \ldots a_{n} \rceil & = & FIX \ f_{t}. \ f_{t} \ \cdot \
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \rceil \ldots \cdot \ \lceil a_{n} \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini & let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \ldots \lceil a_{n} \rceil \ TyCons_{t}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%In HOLCF, where every type is a domain and every function is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent In HOLCF all recursive functions can be defined by fixpoint
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinioperator --- a function that, given as argument the defining term abstracted
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniof the recursive call name, returns the corresponding recursive function.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniCoding this directly turns out to be rather cumbersome, particularly in the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicase of mutually recursive functions, where tuples of defining terms and
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitupled abstraction would be needed. In contrast, the \emph{fixrec} package
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniallows us to handle fixpoint definitions in a way quite more similar to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniordinary Isabelle recursive definitions, providing also with friendly syntax
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifor mutual recursion. \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ fun1 \ :: \ (a \to c) \ \to \ (b \to d) \
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\to \ AType \ a \ b \ \to \ AType \ c \ d $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1 & f \ g \ k & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ x & \to \ ABase \ (f \ x) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ x \ y & \to \ AStep \ (fun1 \ f \ g \ x) \ (fun2 \ f \ g \
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{array} $$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ fun2 \ :: \ (a \to c) \ \to \ (b \to d) \ \to \ BType \ a \ b \ \to \ BType \ c \ d $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun2 & f \ g \ k & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & BBase \ x & \to \ BBase \ (g \ x) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & BStep \ x \ y & \to \ BStep \ (fun2 \ f \ g \ x) \ (fun1 \ f \ g \ y)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{array} $$
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent As an example, the above code translates to HOLCF as follows.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts $
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\begin{array}{ll} fun1 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to 'd::pcpo) \ \to \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('a::pcpo, 'b::pcpo) \ AType \ \to \ ('c::pcpo, 'd::pcpo) \ AType \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini fun2 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini 'd::pcpo) \ \to \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ('a::pcpo, 'b::pcpo) \ BType \ \to \ ('c::pcpo, 'd::pcpo) \ BType
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rccl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fixrec & fun1 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & ABase \cdot pX1 \ => \ ABase \cdot (f \cdot pX1) \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & AStep \cdot pX1 \cdot pX2 \ => \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & \ AStep \cdot (fun1 \cdot f \cdot g \cdot pX1) \cdot (fun2 \cdot f \cdot g \cdot pX2)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini and & fun2 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & BBase \cdot pX1 \ => \ BBase \cdot (g \cdot pX1) \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & BStep \cdot pX1 \cdot pX2 \ => \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & \ BStep \cdot (fun2 \cdot f \cdot g \cdot pX1) \cdot (fun1 \cdot f \cdot g \cdot pX2)) \end{array}$$
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent The translation take care automatically of the fact that,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniin contrast with Haskell, Isabelle requires patterns in case expressions to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifollow the order of datatype declarations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Sentences}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniNon-recursive definitions are treated in an analogous way as in the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslation to HOLCF. Standard lambda-abstraction ($\%$) and function
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniapplication are used here, instead of continuous ones. Partial functions, and
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniparticularly case expressions with incomplete patterns, are not allowed. The
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslation of terms (minus recursion and case expressions) may be summed up
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lcl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil c \rceil & = & c_{t} \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil \backslash x \ \to \ f \rceil & = & \% \ x_{t}. \ \lceil f \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil f \ a_{1} \ldots a_{n} \rceil & = & f_{t} \ \lceil a \rceil \ldots \ \lceil a_{n} \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini & let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \ldots \lceil a_{n} \rceil \ TyCons_{t}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Recursive definitions set HOL and HOLCF apart. In HOL one has to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinipay attention to the distinction between primitive recursive functions
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini(introduced by the keyword \emph{primrec}) and generic recursive ones (keyword
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{recdef}). Termination is guaranteed for each of the former, by the fact
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithat recursion is based on the datatype structure of one of the parameters. In
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicontrast, termination is not a trivial matter for the latter. A strictly
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidecreasing measure needs to be provided, in association with the parameters of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithe defined function. This requires a degree of ingenuity that cannot be
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinieasily dealt with automatically. For this reason, the translation to HOL is
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirestricted to primitive recursive functions. Mutual recursion is allowed for
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniunder some additional restrictions --- more precisely:
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini1) all the functions involved are recursive in the first argument;
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini2) recursive arguments are of the same type in each function.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniAs an example, the translation of mutually recursive functions of type $a
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\rightarrow b, \ldots a \rightarrow d$, respectively, introduces a new
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifunction of type $a \rightarrow (b * \ldots * d)$ which is recursively
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefined, for each case pattern, as the product of the values correspondingly
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitaken by the original ones. The following is a concrete example.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ fun3 \ :: \ AType \ a \ b \to (a \to a) \to AType \ a \ b $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3 \ k \ f & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ a \to ABase \ (f \ a) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ a \ b \to AStep \ (fun4 \ a) \ b \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ fun4 \ :: \ AType \ a \ b \to AType \ a \ b $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun4 \ k & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ x \ y \to AStep \ (fun3 \ x \ (\backslash z \to z)) \ y \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ x \to ABase \ x \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent The translation to HOL of these two functions gives the following.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini fun3 \ :: & ('a::type, 'b::type) \ AType \Rightarrow ('a \Rightarrow
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini 'a) \Rightarrow \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ('a, 'b) \ AType \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini fun4 \ :: & ('a::type, 'b::type) \ AType \Rightarrow ('a \Rightarrow
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini 'a) \Rightarrow\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ('a, 'b) \ AType \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini fun3\_Xfun4\_X :: & ('a::type, 'b::type) \ AType \Rightarrow \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & (('aXX1::type \Rightarrow 'aXX1::type) \Rightarrow \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ('aXX1, 'bXX1) \ AType) * \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & (('aXX2::type \Rightarrow 'aXX2::type) \Rightarrow \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ('aXX2, 'bXX2) \ AType) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3\_def : & fun3 \ == \ \% k \ f. \ fst \ (( fun3\_Xfun4\_X :: \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & \ ('a::type, 'b::type) \ AType \Rightarrow (('a \Rightarrow 'a) \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & \Rightarrow ('a, 'b) \ AType) * ((unit \Rightarrow unit) \Rightarrow \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & (unit, unit) \ AType) ) \ k) \ f \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini fun4\_def : & fun4 \ == \ \% k \ f. \ snd \ (( fun3\_Xfun4\_X :: \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ('a::type, 'b::type) \ AType \Rightarrow \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ((unit \Rightarrow unit) \Rightarrow (unit, unit) \ AType) * \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & (('a \Rightarrow 'a) \Rightarrow ('a, 'b) \ AType) ) \ k) \ f \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $primrec$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3\_Xfun4\_X & (ABase \ pX1) \ = & (\% f. \ ABase \ (f \ pX1), \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & \% f. \ ABase \ pX1) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3\_Xfun4\_X & (AStep \ pX1 \ pX2) & = \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (\% f. \ AStep \ (snd & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2, \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & \% f. \ AStep \ (fst & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2) \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent One may note that the type of the recursive function,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifor each of its call in the body of non-recursive definitions, is given by
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniinstantiations where the Isabelle unit type is replaced for each type variable
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwhich is not occurring on the right hand-side, i.e. for each variable which is
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrininot constrained by the type of the defined function. This is required by
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle, in order to avoid definitions from which inconsistencies could be
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniderivable. Other meta-level features are essentially common to both
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Patterns}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:Patterns}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% not allowed in Isabelle with ordinary definitions (keyword
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \emph{Defs}), but it is allowed with the syntax for recursive ones.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniMultiple function definitions using top level pattern matching are translated
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinias definitions based on a single case expression. This syntactical choice has
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimore to do with HOL than with HOLCF. In fact, multiple definitions in Isabelle
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniare only allowed with the syntax of recursive ones. In primitive recursive
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefinitions, HOL allows for patterns only in one parameter. Therefore, in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniorder to translate definitions having patterns in more than one, before
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniresorting to a more complex syntax (with tuples and \emph{recdef} instead of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\emph{primrec}), it turns out comparatively easier to internally deal with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimultiple definitions as with case expressions. An example follows.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ctl \ :: \ Bool \to Bool \to Bool \to Bool$ \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ False \ a \ False \ = \ a $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ True \ a \ False \ = \ False $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ False \ a \ True = \ True $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ True \ a \ True \ = \ a $\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Translation to HOL gives the following.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts \ ctl :: \ bool \Rightarrow bool \Rightarrow bool \Rightarrow bool$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$$\begin{array}{llll}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini ctl\_def : & ctl \ == & \% qX1 \ qX2 \ qX3. & case \ qX1 \ of \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & False \Rightarrow case \ qX3 & of \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & False \Rightarrow qX2 \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & | \ True \Rightarrow True \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & | \ True \Rightarrow case \ qX3 & of \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & | \ False \Rightarrow False \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & True \Rightarrow qX2 \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent This example cannot be handled by the translation to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHOLCF, owing to the mapping of Boolean values to type \emph{tr}, which is not
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinia recursive datatype. The following, where a defined datatype is used instead
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniof Boolean, gives the closest alternative that can be dealt with.\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent $data \ TV \ = F \ | \ T $\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent $ctlx :: \ TV \to TV \to TV \to TV $ \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$ctlx \ F \ a \ F \ = \ a $ \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$ctlx \ T \ a \ F \ = \ F $ \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$ctlx \ F \ a \ T \ = \ T $ \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini$ctlx \ T \ a \ T \ = \ a $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent This translates to HOLCF as follows.\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent $domain \ TV \ = \ F \ | \ T $
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent $consts \ ctlx :: \ TV \to TV \to TV \to TV $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{llll}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini ctlx\_def : & ctlx \ == & LAM \ qX1 \ qX2 & qX3. \ case \ qX1 \ of \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & F \Rightarrow case \ qX3 & of \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & F \Rightarrow qX2 \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & | \ T \Rightarrow T \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & | \ T \Rightarrow case \ qX3 & of \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & F \Rightarrow F \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & & & | \ T \Rightarrow qX2 \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniSupport of patterns in definitions and case expressions is more restricted in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle than in Haskell. Nested patterns are overall disallowed. In case
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniexpressions, the case term is required to be a variable. Both of these
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirestrictions apply to our translations. A further Isabelle limitation ---
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisensitiveness to the order of patterns in case expressions --- is dealt with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniautomatically. Similarly, wildcards, not available in Isabelle, are dealt
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwith and may be used, in case expressions as well as in function definition,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithough not in nested position. The translation to HOLCF can also handle
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniincomplete patters, also not allowed by Isabelle, in function definitions as
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwell as in case expressions, by using $\bot$ as default value. As nested
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinipatterns are not covered, guarded expressions and list comprehension are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinineither; anyway these can be avoided easily enough, using conditional
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniexpressions and \emph{map} instead.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Classes}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniConceptually, type classes in Isabelle are quite different from those in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHaskell. The former are associated with sets of axioms, whereas the latter
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicome with sets of function declarations. Moreover, Isabelle allows only for
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniclasses with a single type parameter. Most importantly, Isabelle does not
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniallow for type constructor classes. The last limitation is rather serious,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisince it makes hard to cope with essential Haskell features such as monads and
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithe \emph{do} notation. In alternative to the method proposed in \cite{Huff},
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniwe would like to get around the obstacle by relying on an extension of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle based on theory morphism (see section~ \ref{sec:Monads}). The AWE
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinisystem \cite{AWE} is in fact an implementation of such an extension.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniDefined classes are translated to Isabelle as classes with empty
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaxiomatization. Every class is declared as a subclass of \emph{type} --- also
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniin the case of HOLCF, in order to allow for instantiation with lifted built-in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitypes, as well. The translations stay simple and cover only classes with no
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinimore than one type parameter --- one could probably do something more using
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinituples, but this would surely involve considerable complication dealing with
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniconditional instantiations.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniInstance declarations are translated to corresponding ones in Isabelle.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle instances in general require proofs that class axioms are satisfied
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniby the types, but as long as there are no axioms the proofs are trivial and
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicarried out automatically. Method declarations are translated to independent
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifunction declarations with appropriate class annotation on type variables.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniMethod definitions associated with instance declarations are translated to
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinioverloaded function definitions, using type annotation. An example follows.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent $class \ ClassA \ a \ where$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$abase :: \ a \to Bool $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ astep :: \ a \to Bool $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $instance \ (ClassA \ a, \ ClassA \ b) \Rightarrow ClassA \ (AType \ a \ b) \ where $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabase \ x \ = & case \ x \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ u \ \to \ True \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & \_ \ \to \ False \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent The translation of this code to HOLCF gives the following.\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent $axclass \ ClassA < type$
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent $instance \ AType::(\{pcpo, ClassA\}, \{pcpo, ClassA\}) \ ClassA$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$by \ intro\_classes$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabase :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniastep :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_abase :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_astep :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rl}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniAType\_abase\_def : \ abase :: & \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini ('a::\{ClassA, pcpo\}, & 'b::\{ClassA, pcpo\}) \ AType \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini == & LAM x. \ case \ x \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \cdot pX1 \Rightarrow TT \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \cdot pX2 \cdot pX1 \Rightarrow FF \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniAType\_astep\_def : \ astep :: & \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini ('a::\{ClassA, pcpo\}, & 'b::\{ClassA, pcpo\}) \ AType \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & == default\_astep \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Translation to HOL, on the other hand, gives the following.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $axclass \ ClassA < type$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $instance \ AType::(\{type, ClassA\}, \{type, ClassA\}) \ ClassA$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$by \ intro\_classes$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniastep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_abase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_astep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rl}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniAType\_abase\_def : \ abase :: & \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini ('a::\{ClassA, type\}, & 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini == & \% x. \ case \ x \ of \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & ABase \ pX1 \Rightarrow True \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & | \ AStep \ pX2 \ pX1 \Rightarrow False \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniAType\_astep\_def : \ astep :: & \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini ('a::\{ClassA, type\}, & 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini == & default\_astep\\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe additional functions declared for default use in method definition are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniclose mirrors of an internal feature of the Programatica representation.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIn the Programatica internal representation of Haskell, for each function,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniinformation about the class of type parameters is encoded by including in the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniinternal representation of the function some extra arguments (\emph{dictionary
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini parameters}) on top of the original ones. This is particularly useful in the
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicase of overloaded definitions. On the other hand, class information in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle can be represented by direct annotation on the arguments. Therefore,
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithe translation eliminates dictionary parameters and gives function
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefinitions based on their external representation instead. However, for each
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefinition, our translations gives a function explicitly annotated with its
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitype, inclusive of class annotation, in order to allow for overloading (just
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifor the sake of formatting, this type annotation has been delated in some of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithe examples shown).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Equality}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniEquality is the only built-in class which is covered by the two translations.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniAxiomatizations for the associated methods are provided in the base theories
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini--- \emph{HsHOLCF} and \emph{HsHOL}, respectively. Both axiomatizations are
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinibased on the abstract definition of equality and inequality given in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\cite{HaskellRep}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorrinihEq :: & ('a::Eq) \ lift \ \to \ 'a \ lift \ \to \ tr \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorrinihNEq :: & ('a::Eq) \ lift \ \to \ 'a \ lift \ \to \ tr\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $axioms$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniaxEq: & ALL \ x. \ (hEq \cdot p \cdot q \ = \ Def \ x) \ = \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini & (hNEq \cdot p \cdot q \ = \ Def \ (\sim x)) \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe definition of Boolean equality in \emph{HsHOLCF} is obtained by lifting
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniHOL equality, so that $\bot$ is returned whenever one of the argument is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $tr\_hEq\_def: \ hEq \ == \ fliftbin \ (\% (a::bool) \ b. \ a \ = \ b)$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%ax1: & hEq \cdot p \cdot p \ == \ Def \ true \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%ax2: & [| \ hEq \cdot q \cdot r \ = \ Def \ true; \ hEq \cdot p \cdot q \ = \ Def \ true \ |] \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% & ==> \ hEq \cdot p \cdot r \ = \ Def \ true \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniAll built-in methods for built-in types are defined in a similar way.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIn \emph{HsHOL} equality is axiomatized under the implicit assumption of
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinirestricting to terminating programs.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini hEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini hNEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $axioms$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini axEq: & hEq \ p \ q \ == \ \sim hNEq \ p \ q \\
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\noindent Under that assumption, equality for built-in types can be
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniidentified with HOL equality.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% ax1: & hEq \ p \ p \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% ax2: & [| \ hEq \ q \ r; \ hEq \ p \ q \ |] ==> hEq \ p \ r \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Monads}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:Monads}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniIsabelle does not allow for classes of type constructors --- hence the problem
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniin representing monads. We could deal with this problem relying on an
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniaxiomatization of monads that allows for the representation of monadic types
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinias an axiomatic class, as presented in \cite{Lueth}. Monadic types should be
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinitranslated to newly defined types that satisfy monadic axioms. This would
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniinvolve defining a theory morphism, as an instantiation of type variables in
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinithe theory of monads. We are planning to rely on AWE \cite{AWE}, an
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniimplementation of theory morphism on top of Isabelle base logic that may be
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniused to extend HOL as well.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Conclusion}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following is a list of features that are covered by our
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{itemize}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\item predefined types: Boolean, Integer.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\item predefined type constructors: function, Cartesian product, list.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item declaration of recursive datatype, including mutually recursive ones.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\item predefined functions: equality, Boolean operators, connectives, list
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini constructors, head and tail list functions, arithmetic operators.
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini\item non-recursive functions, including conditional, \emph{case} and
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini \emph{let} and expressions (with restriction related to use of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item use of incomplete patterns (in HOLCF) and of wildcards in case
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\item total primitive recursive functions (in HOL) and partial recursive ones
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini (in HOLCF), including mutually recursive ones (with restrictions in the HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item single-parameter class and instance declarations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \item monad declarations and do notation.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo TorriniThe shallow embedding approach makes it possible to get most of the benefit
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniout of the automation currently available on Isabelle. Further work might
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinicarry an extension to cover P-logic \cite{KiebPl}, a specification formalism
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinifor Haskell programs that is included in the Programatica toolset.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%This translation, due to the character of the P-logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%typing system, could be more easily carried out relying on some form
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%of universal quantification on type variables, or else further relying
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%on parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliographystyle{alpha}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliography{case}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{document}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn our example,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation gives the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun1 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('a::type, 'b::type) \ Prelude\_AType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_AType \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun1\_Xfun2\_X & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (('bXX1::type \Rightarrow 'dXX1::type) \ \Rightarrow \\ & ('aXX1::type, 'bXX1::type) \ Prelude\_AType \ \Rightarrow \\ & ('cXX1::type, 'dXX1::type) \ Prelude\_AType) * \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (('bXX2::type \Rightarrow 'dXX2::type) \ \Rightarrow \\ & ('aXX2::type, 'bXX2::type) \ Prelude\_BType \ \Rightarrow \\ & ('cXX2::type, 'dXX2::type) \ Prelude\_BType) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun2 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('a::type, 'b::type) \ Prelude\_BType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_BType \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun1\_def : & fun1 \ == \ \% f. \% g. \% k. \ fst (fun1\_Xfun2\_X \ f) \ g \ k \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun2\_def : & fun2 \ == \ \% f. \% g. \% k. \ snd (fun1\_Xfun2\_X \ f) \ g \ k
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $primrec$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (ABase \ pX1) & = \ (\% g. \% k. \ ABase \ (f \ pX1)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (BBase \ pX1) & = \ (\% g. \% k. \ BBase \ (g \ pX1)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (AStep \ pX1 \ pX2) & = \ (\% g. \% k. \ AStep \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (BStep \ pX1 \ pX2) & = \ (\% g. \% k. \ BStep \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Equality: HOLCF}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Equality: HOL}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell classes and instances are translated to Isabelle,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirespectively, as classes with empty axiomatisation and as instances
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith trivial instantiation proof. The translation supports only
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisingle-parameter classes --- in principle, more than one parameter
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicould be handled using tuples.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever here is not provided !!!
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFunctions declarations associated to classes are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle as independent function declarations with appropriate class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation. Function definitions associated to instances are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated as overloaded function definitions, relying on class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation of typed variables.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% ...xxx...!!! check out for stuff to include in Classes ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNon-recursive definitions are translated to ordinary definitions (keyword
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{defs}), whereas recursive ones require specific keywords. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype of the function, inclusive of class annotation, is included in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinievery definitions in order to allow for overloading.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%For values of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%built-in type, the lifting function is \emph{Def}; the undefined case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%collapses on $\bot$.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn HOLCF, where every type is a domain and every function is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicontinuous, all recursive functions can be defined by fixpoint
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperator. This is essentially a function that, given as argument the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction definition body abstracted of the recursive call name,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireturns the corresponding recursive function. Coding this directly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwould be rather cumbersome, particularly in the case of mutually
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions, where tuples of definition bodies and tupled
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabstraction are needed. We can instead rely on the \emph{recdef}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipackage, which allows to handle fixpoint definitions like ordinary
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive ones, offering nice syntax to deal with mutual recursion as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Type signature}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe present translation to HOL is very basic, and does take into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaccount neither partiality nor laziness. Essentially, it left to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell programmer to check that all the functions are total ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAn account of partiality -- although possibly not aof laziness ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicould be obtained using the option type constructor to lift types,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialong a similar line to lift. Here however we are presenting just a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniplain version, mapping Haskell types in the corresponding unlifted HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. All variables belong to the class type. Recursive and mutually
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive data-types declarations are translated to HOL datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Function definitions}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNon-recursive definitions and let expressions are treated similarly as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin the translation to HOLCF. Recursive defitions is the topic that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireally sets HOL and HOLCF apart. In HOL a distinction has to be drawn
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibetween primitive recursive functions and generic recursive ones. In
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe former, termination is guaranteed by the fact that recursive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions are strictly associated with the datatype structure of a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniparameter. In the latter, termination needs to be proved. This must be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidone, in a \emph{recdef} definition, by providing a measure for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction parameter that can be proved to be strictly decreasing for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieach occurrence of a recursive call in the definition. This requires a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidegree of ingenuity that cannot be generally associated with an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniautomated translation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFor this reason, the translation of recursive functions to HOL is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestricted to primitive recursive ones. Mutually recursive functions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare allowed under additional restrictions. These are: all the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions should be recursive in the first argument; this should be of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe same type for each of them; the constructors should be listed in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe same order in each of the case expressions; the variable names in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe case patterns are expected to be maintained.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation of mutually recursive functions $a \rightarrow b, \ldots a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefined, for each case pattern, as the product of the values
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorrespondingly taken by the original functions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Pattern matching}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSupport of pattern-matching in Isabelle is more restricted than in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. Nested patterns are disallowed; case expressions are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisensitive to the order of the constructors, which should be the same
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias in the datatype declaration. In particular, the case variable si
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequired to be a variable. Translation of pattern-matching is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipotentially laborious. For this reason guarded expressions, list
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomprehension and nested pattern-matching have been left out; they
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishould be replaced by the programmer, using conditional expressions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand map functions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFunction definition by top level pattern matching is not allowed in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle with ordinary definitions, but it is with those that are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexplicitly declared to be recursive ones. However, particularly in HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprimitive recursive definitions patterns are allowed in one parameter
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinionly. In order to translate function definitions with patterns in more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithan one parameter, without resorting to using tuples and more complex
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions (\emph{recdef} instead of \emph{primrec}), our
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslations turn a multiple definition by top level pattern matching
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto a definition by case construct.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Classes}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell classes and instances are translated to Isabelle,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirespectively, as classes with empty axiomatisation and as instances
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith trivial instantiation proof. The translation supports only
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisingle-parameter classes --- in principle, more than one parameter
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicould be handled using tuples.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever here is not provided !!!
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFunctions declarations associated to classes are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle as independent function declarations with appropriate class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation. Function definitions associated to instances are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated as overloaded function definitions, relying on class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation of typed variables.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section*{Haskell2Isabelle}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe tool is designed to support the translation of simple but
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirealistic Haskell programs to HOLCF and, with some restriction, to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL. Not all the syntactical features of Haskell are covered yet,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialthough most of those used in the Prelude are. The most noticeable
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilimitations are related to built-in types, pattern-matching and local
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions. There are additional and more substantial restrictions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin the case of HOL, related to termination and to recursion.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe application can be installed as part of Hets. It requires Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniGHC and Programatica. It is run by the command \emph{hets -t ...
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini [h|hc] file.hs} where the options stand for HOL and HOLCF,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFor the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimodule that contains the main translation function, carried out as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomposition of a signature morphism and a theory morphism.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{IsaSign.hs} contains the Hets representation of the Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibase logic and extensions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe general design of the translation functions, and particularly the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitwo-layered recursion adopted for them, is similar to that used for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe translation Haskell to Agda in Programatica.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Monads}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle does not allow for classes of type constructors, hence a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproblem in representing monads. We can deal with this problem,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever, relying on an axiomatisation of monads that allows for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipresentation of monadic types as an axiomatic class, as provided in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{}. Therefore, monadic types can be translated to newly defined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes that are constrained to satisfy the monadic axioms. This
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstraining, carried out as an instantiation of type variables in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory of monads, takes the form of a theory morphism, and can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicarried out automatically by AWE, an implementation of parametrisation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand theory morphism on top of Isabelle basic logic, that may also be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniused to extend HOL and HOLCF. The do notation can then be translated
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby unpacking it into monadic operators. Attempting to translate
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonadic notation without support AWE support will result in an error
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section*{Conclusion}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following is a list of constructs that are covered by all the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{itemize}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined types: boolean, integer.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predifed type constructors: funtion, cartesian product, list.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item declaration of recursive datatype, including mutually recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined functions: equality, booelan constructors,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini connectives, list constructors, head and tail list functions,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini arithmetic operations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item non-recursive functions, including conditional,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilet and case expressions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item use of incomplete patterns (HOLCF) and of wildcards in case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item total primitive recursive functions (HOL)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand partial recursive ones (HOLCF), including mutual ones (with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestrictions in the HOL case).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item class and instance declarations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item monad declarations and do notation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe shallow embedding approach used by our translations should allow
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito take as much advantage as possible of the automation currently
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavailable on Isabelle, particularly in HOL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFurther work should include extending the translation to cover the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhole of the Haskell Prelude. We hope that this will make it possible
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito support the verification of functional robotics programs.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA further extension, in line with the work on Programtica, would be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe translation of P-logic. This translation, due to the character of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe P-logic typing system, could be more easily carried out relying on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisome form of universal quantification on type variables, or else
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifurther relying on parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliographystyle{alpha}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliography{case}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{document}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation of types is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOur general strategy for translating signatures is to map Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes to Isabelle defined types.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini the fact that Haskell expressions are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinievaluated lazily, however it does not preserve The translation to HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidoes not, and moreover requires that all the functions defined in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell program are total ones...
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll types have a sort in Isabelle, defined by the set of the classes
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof which it is a member. In HOL, all types belong to the class type;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin HOLCF, they belong to class pcpo (pointed complete poset).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll Haskell function declarations are translated to Isabelle ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniType variables are assigned default sort type in HOL and pcpo in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF. Names get translated by a function that preserves them, up to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavoidance of clashes with Isabelle keywords.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe only built-in types that are properly covered are booleans,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniunbounded integers and rationals. These get translated, in the case of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL, to Isabelle booleans, integers and rationals, respectively. Bound
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintegers and floating point numbers would require low-level modelling,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand have not been dealt with; anyway, bounded integers are accepted
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand simply treated as unbounded by the application.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the HOLCF translation, all built-in types get lifted to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorresponding domains (pcpos), which by definion include the undefined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinivalue, by using the lift HOLCF type constructor. In particular, type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniboolean get translated to type tr (short for bool lift), and similarly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor types integer and rational.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRecursive data-types declarations can be translated to datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations in HOL. In HOLCF they can be translated to domain
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations. The two structure are quite similar, except that in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidomains, which are pcpo, all the parameters are required to be pcpos
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well. Morevover, Isabelle domain declarations require to introduce
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininames for destructors. Mutually recursive Haskell datatypes can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated to both logics, relying on the specific Isabelle syntax for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA type class in Isabelle is conceptually quite different from one in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. The former is associated to a set of axioms, whereas the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilatter is associated to a set of function declarations. Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininot allow for type constructor classes. The last limitation is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimost serious of the three, since it makes quite hard to cope with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonads. We can get around this obstacle relying on a method for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \emph{lift} type constructor, in particular, lifts each HOL type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito a flat domain, by adding a bottom element to them. We are going to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniuse it to lift the basic types. For the product we are going to use
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininon-strict product.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformalisation on Isabele relies on axiomatic type classes \cite{},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith \emph{pcpo} (pointed complete partial order) as the default
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclass, in which the type of continuous functions can be represented as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction spaces, allowing for an elegant interpretation of recursion
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby fixpoint operator. HOL types may be lifted to \emph{pcpo} by simply
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniadding a bottom element to them. This is what the type constructor
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{lift} does, thus providing also a way of handling partiality ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniundefined cases can be mapped to the bottom element. HOLCF has also a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype constructor \emph{u} that allows to deal with laziness, by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniguaranteeing $\bot \neq \smath{up} \$ (\bot)$.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the case of HOLCF, the logic provides a computational
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinterpretation of function types as domains. In HOL there is no such
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifacility, therefore either appropriate types for the translation are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintroduced --- as in \cite{}, or considerable semantical restrictions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimust be accepted --- this is also the case for one of the translation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito FOL proposed in \cite{}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDepending on the expressiveness of the logic, the translation of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprogramming language may be carried out at different levels of depth.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn general, the deeper is the embedding, the less it relies on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimeta-level features of the target language. This may be a plus, either
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifrom the point of view of semantic clarity, or from that of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressiveness. Taking advantage of meta-level feaures, on the other
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihand, may be useful in order to make the theorem proving less tedious,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby allowing more constant use of generic proof methods. It may also
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniultimately affect positively the theorem prover economy, by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireinforcing the bias toward the development of proof methods that,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever specific, can be more easily integrated with generic ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% a point made in \cite{}. for example by allowing a straightforward
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% operational interpretation ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations of Haskell to HOLCF and HOL that we are presenting in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe following justify themselves in terms of denotational semantics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOLCF differs from that proposed in \cite{} in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitreatment of types. We translate Haskell types directly into HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniones, whereas they use HOLCF terms to embed Haskell types. We assume
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat the HOLCF types are similar enough to the those of Haskell, in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniorder to guarantee the semantical correctness of our translations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMoreover, we rely on axiomatic classes to translate Haskell types
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOur approach has the advantage of giving a shallower embedding,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever it has the drawback of not bein complete --- notably, type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructor classes are missing. We plan to handle in future this
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproblem (see section~\ref{sec:Monads}) by relying on an extension of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle based on morphism between theories. The translation into HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis essentialy only a first experiment, it handles types very
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimplistically, relying on drastic semantical restrictions for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorrecteness. Under those restrictions, however, it gives expressions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat are comparatively quite simple to work with.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA type class in Isabelle is conceptually quite different from one in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. The former is associated to a set of axioms, whereas the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilatter is associated to a set of function declarations. Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininot allow for type constructor classes. The last limitation is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimost serious of the three, since it makes quite hard to cope with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonads. We can get around this obstacle relying on a method for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Types}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF allows has types for computable functions --- defined as sets of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicontinuous functions of a type (!! fixpoints!!). It has a type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructor \emph{lift} that lifts HOL types to \emph{pcpo}s, thus
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproviding a way of handling partiality --- undefined cases can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimapped to the bottom element. It has also a type constructor \emph{u}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat allows to deal with laziness, by guaranteeing $\bot \neq
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\smath{u}(\bot)$.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat can be used to embed Haskell function types.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOLCF differs from that to HOL insofar as only the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifirst one relies on a denotational semantics for the full language,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinikeeping into account partiality and lazy evaluation, and associating
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions to corresponding fixed points, using on the Fixrec
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniextension of HOLCF. The translation to HOL is more restrictive; it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidoes not keep into account any form of partiality, and it restricts
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation of recursive functions to the primitive recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIt would have been possible to give an account of partiality in HOL by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniusing option types. However, we chose to keep the HOL translation as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimple as possible for didactic purpose.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{maybe}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations of Haskell that we are presenting in the following,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe present translations of Haskell into some of the Isabelle logics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThese translations are implemented as part of Hets, and are based on a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishallow embedding approach quite different from that used in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProgramatica. In our translations Haskell types are mapped to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. We are assuming that the type systems of HOL and HOLCF are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimilar enough to the type system of Haskell, in order to guarantee
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe semantical correctness of our translations. Moreover, we rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic classes to translate Haskell types classes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA type class in Isabelle is conceptually quite different from one in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. The former is associated to a set of axioms, whereas the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilatter is associated to a set of function declarations. Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininot allow for type constructor classes. The last limitation is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimost serious of the three, since it makes quite hard to cope with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonads. We can get around this obstacle relying on a method for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOLCF differs from that to HOL insofar as only the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifirst one relies on a denotational semantics for the full language,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinikeeping into account partiality and lazy evaluation, and associating
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions to corresponding fixed points, using on the Fixrec
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniextension of HOLCF. The translation to HOL is more restrictive; it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidoes not keep into account any form of partiality, and it restricts
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation of recursive functions to the primitive recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIt would have been possible to give an account of partiality in HOL by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniusing option types. However, we chose to keep the HOL translation as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimple as possible for didactic purpose.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Type signature}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOur general strategy for translating signatures is to map Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes to Isabelle defined types. The translation to HOLCF keeps into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaccount the fact that Haskell expressions are evaluated lazily. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation to HOL does not, and moreover requires that all the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions defined in the Haskell program are total ones...
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll types have a sort in Isabelle, defined by the set of the classes
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof which it is a member. In HOL, all types belong to the class type;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin HOLCF, they belong to class pcpo (pointed complete poset).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll Haskell function declarations are translated to Isabelle ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniType variables are assigned default sort type in HOL and pcpo in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF. Names get translated by a function that preserves them, up to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavoidance of clashes with Isabelle keywords.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe only built-in types that are properly covered are booleans,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniunbounded integers and rationals. These get translated, in the case of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL, to Isabelle booleans, integers and rationals, respectively. Bound
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintegers and floating point numbers would require low-level modelling,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand have not been dealt with; anyway, bounded integers are accepted
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand simply treated as unbounded by the application.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the HOLCF translation, all built-in types get lifted to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorresponding domains (pcpos), which by definion include the undefined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinivalue, by using the lift HOLCF type constructor. In particular, type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniboolean get translated to type tr (short for bool lift), and similarly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor types integer and rational.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRecursive data-types declarations can be translated to datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations in HOL. In HOLCF they can be translated to domain
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations. The two structure are quite similar, except that in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidomains, which are pcpo, all the parameters are required to be pcpos
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well. Morevover, Isabelle domain declarations require to introduce
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininames for destructors. Mutually recursive Haskell datatypes can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated to both logics, relying on the specific Isabelle syntax for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe present translations of Haskell into some of the Isabelle logics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThese translations are implemented as part of Hets, and are based on a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishallow embedding approach quite different from that used in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProgramatica. In our translations Haskell types are mapped to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. We are assuming that the type systems of HOL and HOLCF are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimilar enough to the type system of Haskell, in order to guarantee
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe semantical correctness of our translations. Moreover, we rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic classes to translate Haskell types classes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the following, we present translations of Haskell into some of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle logics. These translations are implemented as part of Hets,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand are based on a shallow embedding approach quite different from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat used in Programatica. In our translations Haskell types are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimapped to Isabelle types. We are assuming that the type systems of HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand HOLCF are similar enough to the type system of Haskell, in order
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito guarantee the semantical correctness of our translations. Moreover,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe rely on axiomatic classes to translate Haskell types classes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini are those presented in \cite{}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well as in \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation of Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto FOL \cite{} and that into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn \cite{} Haskell is embedded in Martin-Loef
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype theory, implemented on Agda.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini is indeed a general difference between a lower level
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniapproach based on operational semantics, followed in \cite{agda} and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{miranda}, and a higher-level one, based essentially on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotational semantics, followed in \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe correctness of such embeddings
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialways rests, ultimately, on the denotational semantics of Haskell,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand on the possibility to encode it in a logic under consideration.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Thompson95}. Indeed, Haskell --- a strongly typed, purely
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctional language with lazy evaluation, based on a system of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipolymorphic types extended with type constructor classes, where monads
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniallow for side effects and pseudo-imperative code \cite{Hudak} --- has
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialready been considered several times as a target for verification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll the above-mentioned works provide embeddings of Haskell, either
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipartial or total, into programming logic implemented on theorem
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprovers. The correctness of such embeddings always rests, ultimately,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinion the denotational semantics of Haskell, and on the possibility to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniencode it in a logic under consideration.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe tools, the logic and the ways in which the encoding can be done
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimay differ quite deeply. In \cite{} Haskell is embedded in Martin-Loef
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype theory, implemented on Agda. All the other examples rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle, a generic theorem-prover written in SML that allows for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformalisation of a variety of logics, including FOL, HOL and HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Paulson94isa}. The embedding in \cite{} rely on FOL, the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle implementation of classical first-order logic.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll the other examples \cite{...} rely on higher-order logic. HOL is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe implementation of classical higher-order logic based on simply
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinityped lambda calculus, extended with axiomatic type classes. HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{holcf} is the extension of HOL with a formalisation of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory of computable functions (LCF) based on axiomatic type classes.
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
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses. Isabelle-HOLCF \cite{holcf} is the extension of HOL 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.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations of Haskell that we are presenting in the following,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe present translations of Haskell into some of the Isabelle logics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThese translations are implemented as part of Hets, and are based on a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishallow embedding approach quite different from that used in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProgramatica. In our translations Haskell types are mapped to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. We are assuming that the type systems of HOL and HOLCF are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimilar enough to the type system of Haskell, in order to guarantee
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe semantical correctness of our translations. Moreover, we rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic 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
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Monads}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec: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}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Moreover, being such languages
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%as Haskell, ML and Miranda closely modelled on typed lambda-calculus,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%their translations to specification formalisms, particularly to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%higher-order logics, turn out to be comparatively straighforward to be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%defined in the main lines --- although not so to be carried out in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%, due to the richness in syntax, the specific way evaluation is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%implemented, as well as to issues associated with classes (Haskell),
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%overloading and side effects.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%All functions are total in HOL. Partiality may be dealt with by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%lifting types through the \emph{option} type constructor. HOL has an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%implementation of recursive functions based on Tarski fixed-point
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%theorem. Defining a recursive function requires giving a specific
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%measure and proving monotonicity about it.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% HOL has an implementation of recursive functions, based on Tarski
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% fixed-point theorem. Their definition in general requires specific
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% measure to be given each time, for monotonicity to be proved.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% Moreover, partial functions are needed to programs that might not
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% terminate, but in HOL all functions are total. Partiality may be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% dealt with by lifting types through \emph{option}, a type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% constructor in HOL. This inevitably complicates case expressions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%There are different general approaches depending on the style of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%semantics. The expressiveness of the logical language may also make a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%big difference.
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).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini as well as an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperational, but is quite deep.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniit builds into HOL a specific domain class for the interpretation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHigher-level approaches relying on denotational
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini propose level
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniapproaches based on large-step operational semantics, even if with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisome complication when dealing with higher-order programming languages
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisuch as those presented in \cite{} --- Miranda in FOL; \cite{} ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell in FOL; \cite{} --- Haskell in the Agda implementation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMartin-Loef type theory. More expressiveness is usually required by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihigh-level approaches based on denotational semantics, such as those
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipresented in \cite{} --- Haskell in HOLCF and HOL; \cite{} --- ML in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe main one, is which Depending on the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressiveness of the logic, the translation of the programming
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilanguage may be carried out at different levels of depth. In general,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe deeper is the embedding, the less it relies on meta-level features
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the target language. This may be a plus, either from the point of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniview of semantic clarity, or from that of expressiveness. Taking
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniadvantage of meta-level feaures, on the other hand, may be useful in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniorder to make the theorem proving less tedious, by allowing more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstant use of generic proof methods. It may also ultimately affect
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipositively the theorem prover economy, by reinforcing the bias toward
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe development of proof methods that, however specific, can be more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieasily integrated with generic ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSome significantly different examples of functional programming
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilanguages embedded into the logic of a theorem prover can be found in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{} (Miranda on Isabelle), \cite{} (ML on Isabelle), \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(Haskell on Isabelle), \cite{} (Haskell on Agda). Example of lower
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilevel approaches are given in \cite{}, where Haskell is translated
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto the Agda implementation of Martin-Loef theory based on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperational rules and relies on operational semantics for correctness,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis followed in \cite{}, where Haskell is embedded into the Agda
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimplementation of Martin-Loef theory, as well as in the embeddings of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMiranda \cite{} and Haskell \cite{} into FOL (classical first-order
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilogic, until the middle of the nineties still probably the best
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisupported logic on Isabelle). Higher-level approaches, such as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipresented in \cite{} (embedding ML into HOL), and in \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(embedding Haskell into HOLCF and into HOL), rely ultimately on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotational semantics for correctenss. This, together with the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressiveness allowed by higher-order logic for the formulation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequirements, gives the considerable advantage of enabling proofs that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare more abstract and closer to mathematical intuition.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimethod for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniit is not complete, and cannot be trivially completed ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininotably, type constructor classes have not been considered, since
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle does not have them. However, we are expecting to deal with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithis problem by relying on an extension of Isabelle based on theory
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimorphism (see section \ref{}) .