hs2isa.tex revision 278efe81d7d9f2e475e76c74c0db8622ccef99eb
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% Author: Paolo Torrini <paolot@helios.dai.ed.ac.uk>
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski% Created: Mon Feb 15 1999
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\documentclass[a4paper,12pt]{article}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage[dvips]{graphics}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{amsfonts}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{amssymb}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%\usepackage{psfig}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{fancybox}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\usepackage{epsfig}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{graphicx}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{color}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski%\usepackage{semrot}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\input{newmacros}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski% Use \includegraphics{*.eps} for pictures
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Enlarge printing area a bit:
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\textwidth}{16cm}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\setlength{\oddsidemargin}{0cm}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\setlength{\evensidemargin}{0cm}
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski\setlength{\topmargin}{-0.94cm}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\setlength{\textheight}{23cm}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{document}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\title{Translating Haskell to Isabelle logics in Hets}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\author{Paolo Torrini, Till Mossakowski, Christian Maeder}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \\ Fachbereich Mathematik und Informatik, Universitaet Bremen}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\abstract{\scriptsize \bf Automated, partial translations of Haskell
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini into Isabelle higher-order logic (with or without computable
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini functions) have been implemented as functions of Hets, a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Haskell-based proof-management and program development system that
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini allows for integration with other tools. The application, built on
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini top of Programatica-style static analysis, can translate simple
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Haskell programs to HOLCF and, under stronger restrictions, to HOL.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Both translations are based on shallow embedding and rely
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini informally on denotational semantics.}\\
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini% The translation of monads uses the AWE extension of Isabelle.}\\
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo TorriniWork on the integration of compilers, analyzers and theorem-provers,
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinias well as translations between programming and specification
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilanguages, may help on the way to making formal development and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniverification of programs more viable. In order to verify formally a
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiprogram, we need to formulate the requirements in a logic that also
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiallows for the program to be represented; to translate the program to
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithe logic; finally, to carry out a proof of the correctness statement.
5b465790447d54472837f1084ed3e751c745d0dcTill MossakowskiAlthough specifications and proofs require normally the biggest amount
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiof work, translations can also be a significant source of potential
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiproblems. For the verification to be reliable and efficient, the
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskitranslation should rest on the definition of a formal semantics of the
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiprogramming language in the specification logic; it should be carried
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiout safely, at best automatically; it should also give program
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskirepresentations that do not make proofs more complex than necessary.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIt has long been argued that functional languages, based on notions
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskicloser to general, mathematical ones, can make the task of proving
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiassertions about them easier, owing to the clarity and relative
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisimplicity of their semantics \cite{Thompson92}.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiIn this report we are presenting automated translations based on
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskidenotational semantics of Haskell programs into Isabelle higher-order
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskilogic. Haskell is a strongly typed, purely functional language with
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskilazy evaluation. It relies on a system of polymorphic types extended
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiwith type constructor classes, and has a syntax for side effects and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskipseudo-imperative code based on monadic operators \cite{HaskellRep}.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe translations are implemented as functions of Hets \cite{Hets}, an
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiHaskell-based application designed to support integration of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskispecification formalisms for the development of Haskell programs. Hets
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisupplies with parsing, static analysis, proof management and interface
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskito various language-specific tools. From the point of view of generic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitheorem proving, Hets relies on an interface with Isabelle, a
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskistate-of-the-art interactive theorem-prover, written in SML, allowing
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifor the formalization of a variety of logics \cite{Paulson94isa}. Hets
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirelies on Programatica \cite{Prog04} for the parsing and static
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinianalysis of Haskell programs. Programatica is a Haskell-specific
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniformal development system built at OGI, envisioned to provide more
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithan analysis. Its own proof management includes a specification logic
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiand translations to different proof tools, notably to Isabelle
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\cite{Huff}. In section~\ref{sec:Translations} it is going to be
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiclarified how our work differs from theirs.
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini\section{Isabelle}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle-HOL (hereafter simply HOL) is the implementation in Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof classical higher-order logic based on simply typed lambda calculus,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniextended with axiomatic type classes. It provides considerable support
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifor reasoning about programming functions, both in terms of libraries
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand automation. Since the late nineties, it has essentially superseded
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiFOL (classical first-order logic) as the logic of standard use in
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiIsabelle. HOL has an implementation of recursive functions based on
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiKnaster-Tarski fixed-point theorem. All functions are total;
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskipartiality may be dealt with by lifting types through the
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\emph{option} type constructor.
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till MossakowskiHOLCF \cite{holcf} is HOL conservatively extended with the logic of
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskicomputable functions --- a formalization of domain theory. In HOL,
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskitypes are just sets; functions may not be computable, and a recursive
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskifunction may require discharging proof obligations already at the
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskidefinition stage --- in fact, a specific measure has to be given for
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskithe function to be proved monotonic. In contrast, domain theory has
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskieach type interpreted as a \emph{pcpo} (pointed complete partially
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiordered set) that is, as a set with a partial order which is closed
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiw.r.t. $\omega$-chains and has a bottom. All functions defined over
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidomains, including partial ones, are continuous, therefore computable.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiRecursion can be expressed in terms of least fixed-point operator, and
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiso, in contrast with HOL, function definition is never dependant on
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe Isabelle formalization of HOLCF is based on axiomatic type classes
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\cite{Wenzel}, following an approach that makes it possible to deal
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiwith complete partial orders while abstracting away from any specific
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskirelation. The class of types is \emph{pcpo} --- whereas in HOL it is
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\emph{type}. Domain theory offers a good basis for the semantical
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskianalysis of programming languages; however, it may make proofs
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicomparatively hard. After being spared the need to discharge proof
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiobligations at the defining stage, one has to bear with assumptions
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiover the continuity of functions while proving theorems. A standard
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskistrategy to get the best out of the two systems is to define as much
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskias possible in HOL language, using HOLCF type constructors to lift
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitypes to domains only when this is needed.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\section{Translations}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\label{sec:Translations}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiA translation may be carried out relying on different semantical
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiapproaches and at different levels of depth, depending mainly on the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiexpressiveness of the target logic. Different formalisms may make the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiembedding of certain features more or less hard. Translations into FOL
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskisuch as those based on large-step operational semantics of Miranda
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\cite{Thompson95,Thompson89,Thompson95b} and Haskell \cite{Thompson92}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicannot deal straightforwardly at first order with higher-order
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifeatures such as currying. The translation of Haskell to the Agda
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiimplementation of Martin-Loef type theory in \cite{Abel} gets
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicomplicated dealing with Haskell polymorphism. The expressiveness of
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskihigher-order logic help overcome more plainly most of these obstacles,
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiand makes it possible to adopt a higher-level approach based on
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskidenotational semantics, as proposed in \cite{Huff} to translate
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiHaskell to HOLCF, and used in \cite{Pollack} to translate ML to HOL.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThis approach allows for representations of programs that are closer
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskito their specification as well as for proofs that are relatively more
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiabstract and general.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiExpressiveness plays an important role in the ``depth'' issue, as
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiwell. A shallow embedding is one that relies as much as possible on
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskibuilt-in features and packages provided with the implementation of the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitarget language, especially with respect to general features such as
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitypes, classes, and recursion. The deeper the embedding, the less it
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskirelies on such features. This independence may be a plus from the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskipoint of view of semantic clarity and logical generality ---
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiobject-logical, ``deep'' translation can be used to overcome
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\emph{ad-hoc} limitations imposed by the built-in, meta-level
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifeatures. Taking advantage of those features, on the other hand, may
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskihelp make the theorem proving less tedious and make it easier to rely
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskion common proof methods.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe translation of ML in \cite{Pollack} gives an example on the deep
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiside --- a class of types with bottom elements is defined in HOL for
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe sake of the embedding. On the other hand, the translation of
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiHaskell to HOLCF proposed in \cite{Huff} relies on a generic
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torriniformalization of domain theory, particularly on the \emph{fixrec}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskipackage for recursive functions (part of HOLCF in Isabelle 2006)
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskideveloped in order to provide with a friendly syntax that covers
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskimutually recursive definitions, too. Not even this translation is
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskishallow as far as types are concerned, though. In order to capture an
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiimportant feature of the Haskell type system, notably type constructor
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiclasses, Haskell types are not translated to HOLCF types, rather they
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiare to terms, relying on a modelling of the Haskell type system at the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiobject level. In this way it is possible to give a complete account
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiof the type system. The practical drawback is that plenty of the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiautomation built into the Isabelle type checking is lost, unless one
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiis prepared to reimplement a lot.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe translations of Haskell to HOLCF and HOL that we are presenting
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskihere are based on denotational semantics keeping to a shallow
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiapproach. The translation to HOLCF relies on the \emph{fixrec}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskipackage, along similar lines to those in \cite{Huff}. In contrast with
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithem, we translate Haskell types to HOLCF types, quite directly, and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiHaskell classes to Isabelle axiomatic classes, wishing to take
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskieffectively advantage of Isabelle type checking. We rely on the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiassumption that types in HOLCF are similar enough to those in Haskell
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskito allow for embedding, save for possible implementation subtleties
413201905fc2c50c77555aea8f73444d2841126cPaolo Torrinithat we are not going to consider. We expect that operational
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniequivalence between Haskell programs and their translation to HOLCF
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiholds up to the level of typeable output. The translation covers a
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskisignificant part of the syntax used in the Prelude, although it is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinistill incomplete in one important respect --- it does not include type
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiconstructor classes; we have plans, however, for an extention that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinishould address this aspect as well.
5b465790447d54472837f1084ed3e751c745d0dcTill MossakowskiConceptually, type classes in Isabelle are quite different from those
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiin Haskell. The formers are associated with sets of axioms, whereas
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe latters come with sets of function declarations. Isabelle classes
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskimay have at most a single type parameter. Most importantly, Isabelle
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidoes not allow for type constructor classes. The last limitation is
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiserious, since it makes hard to cope with essential Haskell features
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskisuch as monads and \emph{do} notation. In alternative to the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitreatment of types proposed in \cite{Huff}, we would like to get
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiaround the obstacle by relying on an extension of Isabelle based on
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitheory morphism (see section~ \ref{sec:Monads}). The AWE system \cite{AWE}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiis in fact an implementation of such an extension.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiOur translation to HOL, shallow as well, is much more limited. The
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimost important restriction is related to recursion --- only primitive
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskirecursive functions are covered. This limitation appears relatively
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskihard to overcome, given the way syntax for full recursion works in
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiHOL. Operational equivalence up to typeable output for the remaining
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifragment would require using option types, but we do not pursue it
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskihere, rather we rely on a restriction to terminating programs for
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisemantical correctness. Under such restrictions, however drastic,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithis translation gives expressions that are particularly simple and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitherefore potentially useful to verify some properties.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\section{Haskell2Isabelle}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe Hets function \emph{Haskell2Isabelle} supports the translation of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisimple Haskell programs to HOLCF and, with more restriction, to HOL.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiNot all the syntactical features used in the Prelude and main
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskilibraries are covered. Some of the most noticeable limitations are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithose related to built-in types, pattern-matching, local definitions,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiimport and export. There are additional and more substantial
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskirestrictions in the case of HOL, related to termination and recursion.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiEach of the translations relies on a \emph{base theory}. These are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIsabelle theory files, respectively \emph{HsHOLCF}, extending HOLCF,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiand \emph{HsHOL}, extending HOL, which are included in the Hets
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskidistribution. Each of them provides definitions and axiomatizations of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskinotions that are used in the corresponding translation --- notably
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo TorriniInformation for the use of Hets may be found in \cite{HetsUG} and a
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskigeneral outlook in \cite{HetsUG}. The Haskell-to-Isabelle translation
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskirequires essentially GHC, Isabelle 2006 and Programatica --- with
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskirespect to the latter, both analysis and translation functions in Hets
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskimake use of its modules. The command to run the application is
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\emph{hets -v[1--5] -t Haskell2Isabelle[HOLCF | HOL] -o thy filename}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\noindent where options set verbosity, target logic and name of the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskioutput file. The input file (last argument) must be a GHC source
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski(\emph{hs} extension). The Haskell program gets analyzed and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskitranslated. The result of a successful execution is an Isabelle theory
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifile (\emph{thy} extension) depending on the corresponding base
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%The application requires essentially Haskell GHC and Programatica. It
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%is run by the command \emph{hets -t ... [h|hc] file.hs} where the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%options stand for HOL and HOLCF, respectively.
eee2119f1e850ad533252f43212664b25d83e7adPaolo TorriniThe internal representation of Haskell in Hets (module
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrini\emph{Logic\_Haskell} and particularly \emph{HatAna}) is essentially
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrinithe same as in Programatica, whereas the internal representation of
eee2119f1e850ad533252f43212664b25d83e7adPaolo TorriniIsabelle (module \emph{Logic\_Isabelle} and particularly
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\emph{IsaSign}) is a Haskell reworking of the ML definition of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIsabelle own base logic, extended in order to allow for a
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskistraightforward representation of HOL and HOLCF.
5b465790447d54472837f1084ed3e751c745d0dcTill MossakowskiHaskell programs as well as Isabelle theories are internally
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskirepresented as Hets theories --- each of them a data-structures formed
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiby a signature and a set of sentences, fitting a theoretical framework
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskidescribed in \cite{MossaTh}. Each translation, defined as composition
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiof the signature translation with the translation of all sentences,
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskihas the structure of a morphism from theories in the internal
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskirepresentation of the source language to those in the representation
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiof the target language. The distribution module
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowski\emph{Haskell2IsabelleHOLCF} contains the main function, dependent on
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskithe target logic. The module \emph{IsaPrint} provides the essential
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskifunctions for the pretty-printing of Isabelle theories.
5b465790447d54472837f1084ed3e751c745d0dcTill MossakowskiThe following gives a list of reserved names, i.e. the names that are
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiused in order to either rename or name automatically variables and
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskiconstants in the translations. 1) Type variables, in the translation
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowskito HOL: \emph{'vX}; any name terminating with \emph{'XXn} where $n$ is
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskian integer. 2) Term variables, in both translations: \emph{pXn},
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\emph{qXn}, with $n$ integer. 3) Constants, in the translation to HOL:
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskistrings obtained by joining together names of defined functions, using
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\emph{\_X} as end sequence and separator.
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski%Correspondingly, the translation function is defined as the
413201905fc2c50c77555aea8f73444d2841126cPaolo Torrini%composition of signature translation with the translation of all
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski%structure of a morphism from Hets theories written in the language of
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski%the source internal representation to those in the language
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski%representation of the target language. Internally, the information
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski%about types is collected into a signature, whereas datatype
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski%declarations and definitions are associated with sentences.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% module that contains the main translation function, carried out as
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% composition of a signature morphism and a theory morphism.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% \emph{IsaSign.hs} contains the Hets representation of the Isabelle
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski% base logic and extensions.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% The general design of the translation functions, and particularly
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% the two-layered recursion adopted for them, is similar to that used
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% for the translation Haskell to Agda in Programatica.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\subsection{HOLCF: Type signature}
eee2119f1e850ad533252f43212664b25d83e7adPaolo TorriniThe translation to HOLCF keeps into account partiality, i.e. the fact
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrinithat a function might be undefined for certain values, either because
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskidefinition is missing, or because the program does not terminate. It
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinialso keeps into account laziness, i. e. the fact that by default
0078e2f9b2d9ad3ceec2b68817ab1cc31ee50813Till Mossakowskifunction values in Haskell are passed by name and evaluated only when
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskineeded. Essentially, we are following the main lines of the ``crude''
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskidenotational semantics for lazy evaluation in \cite{winskel}, pp.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski216--217. Raising an exception is different from running forever, and
0078e2f9b2d9ad3ceec2b68817ab1cc31ee50813Till Mossakowskiboth are different from stopping short of evaluation. However, from
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithe point of view of the printable output, these behaviours are
0078e2f9b2d9ad3ceec2b68817ab1cc31ee50813Till Mossakowskisimilar and can be treated semantically as such, i.e. using one and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithe same bottom element.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% In order to ease the translation of some notions, the Isabelle
0078e2f9b2d9ad3ceec2b68817ab1cc31ee50813Till Mossakowski% theory \emph{HsHOLCF.thy}, that extends HOLCF has been defined and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% included in the Hets distribution.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% It is often convenient to define in Isabelle notions that match the
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% translation of some itmes.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% Haskell datatype and function declarations are translated to
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% declarations in HOLCF. Names are translated by a function that
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini% preserves them, up to avoidance of clashes with HOLCF keywords.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill MossakowskiEach type in Isabelle has a sort, defined by the set of the classes of
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiwhich it is member. Haskell type variables are translated to HOLCF
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torriniones, of class \emph{pcpo}. Each built-in type is translated to the
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinilifting of its corresponding HOL type. Properly covered are Haskell
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrinibooleans and unbounded integers, associated respectively to HOL
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskibooleans and integers.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski%Rationals need to be
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%imported in order to be used in Haskell, so they are not covered by
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%the translation at the present stage (import has not been dealt with
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski%and rationals.
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till MossakowskiBound integers and floating point numbers would need low-level
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskimodelling, and have not been covered. Bounded integers in particular
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiare simply treated as unbounded in the translation. The HOLCF type
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiconstructor \emph{lift} is used to lift HOL types to flat domains. In
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskithe case of booleans, we can use type \emph{tr}, defined as equal to
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski$bool \ lift$ in HOLCF. In the case of integers, we use \emph{dInt},
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskidefined in \emph{HsHOLCF} to equal $int \ lift$. The types of Haskell
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskifunctions and product are translated, respectively, to HOLCF function
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskispaces and lazy product --- i.e. such that $\bot = (\bot * \bot) \neq
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski(\bot*'a) \neq ('a * \bot)$, consistently with lazy evaluation. Type
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiconstructors are translated to corresponding HOLCF ones (noticeably,
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiparameters precede type constructors in Isabelle syntax). In
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiparticular, lists are translated to the domain \emph{llist} defined in
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski\emph{HsHOLCF}. Function declarations are translated to HOLCF ones
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski(keyword \emph{consts}). Names (for types as well as for terms) are
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskitranslated by a function ($t$ here) that preserves them, up to
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiavoidance of clashes with HOLCF keywords. Translation of types (minus
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskimutual recursion) may be summed up as follows:
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski% Haskell datatype and function declarations are translated to
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski% declarations in HOLCF.
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski$$\begin{array}{lcl}
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski \lceil a \rceil & = & 'a_{t}::pcpo \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \lceil Bool \rceil & = & tr \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \lceil Integer \rceil & = & dInt \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \lceil a \to b \rceil & = & \lceil a \rceil \to \lceil b \rceil \\
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \lceil [a] \rceil & = & \lceil a \rceil \ llist \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\noindent In HOL, datatype declarations define types of class
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\emph{type} by keyword \emph{datatype}; in contrast, in HOLCF, they
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskidefine types of class \emph{pcpo} (i.e. domains) by keyword
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\emph{domain} (so we also may call them \emph{domain declarations}).
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiEach recursive datatype declaration in Haskell is translated to the
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskicorresponding one in HOLCF. The translation of mutually recursive
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskidatatypes relies on specific Isabelle syntax (keyword
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowski\emph{and}), as in the next example.\\
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowski$data \ AType \ a \ b \ = \ ABase \ a \ | \ AStep \ (AType \ a \ b) \ (BType \ a \ b) $
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski$data \ BType \ a \ b \ = \ BBase \ b \ | \ BStep \ (BType \ a \ b) \ (AType \ a \ b) $\\
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini\noindent This translates to HOLCF as the following.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rr} domain & \ ('a::pcpo, 'b::pcpo) \ BType \ = \ BBase \ (BBase\_1::'b) \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & BStep \ (BStep\_1::('a, 'b) \ BType) \ (BStep\_2::('a, 'b) \ AType) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini and & \ ('a::pcpo, 'b::pcpo) \ AType \ = \ ABase \ (ABase\_1::'a) \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & AStep \ (AStep\_1::('a, 'b) \ AType) \ (AStep\_2::('a, 'b) \ BType) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Notably, domain declarations require an explicit
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torriniintroduction of destructors. Both translations (to HOL as well as to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHOLCF) take care automatically of the order of datatype declarations
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini--- this is needed, insofar as, differently from Haskell, Isabelle
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskirequires them to be listed according to their order of dependency.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\subsection{HOLCF: Sentences}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiEach Haskell function definition is translated to a corresponding one.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniNon-recursive definitions are translated to standard ones (keyword
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{defs}), whereas the translation of recursive definitions relies
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinion the \emph{fixrec} package. Lambda abstraction is translated as
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicontinuous abstraction (\emph{LAM}), and function application as
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicontinuous application (the \emph{dot} operator) --- these notions
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskicoincide with the corresponding, HOL-defined ones, whenever their
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiarguments are continuous.
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini% As to the translation of terms containing either values or operators
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini% of built-in type, it is often the case that we translate them to
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini% lifted HOL operators. The lifting function is \emph{Def}; $\bot$ is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% used for the undefined case.
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo TorriniTerms of built-in type (boolean and integers) are translated to lifted
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo TorriniHOL values, using the HOLCF-defined lifting function \emph{Def}. The
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibottom element $\bot$ is used for all undefined terms. The following
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinioperator, defined in \emph{HsHOLCF}, is used to map binary arithmetic
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinifunctions to lifted functions over
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinilifted integers.\\
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo 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 $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Booleans are translated to values of \emph{tr} ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{TT}, \emph{FF} and $\bot$, and boolean connectives are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskitranslated to the corresponding HOLCF-defined lifted operators.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiHOLCF-defined \emph{If then else fi} and \emph{case} syntax are used
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskito translate, respectively, conditional and case expressions. There
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiare some restrictions, however, on the latters, due to limitations in
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskithe translation of patterns (see section~\ref{sec:Patterns}); in
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiparticular, the case term should always be a variable, and no nested
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinipatterns are allowed.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe translation of lists and list constructors relies on the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifollowing \emph{HsHOLCF}-defined datatype.\\
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski$domain \ 'a\ llist \ = \ lNil \ | \ lCons \ (lazy \ lHd ::'a) \ (lazy \ lTl ::'a \ llist) $\\
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski\noindent Under the given interpretation, a stream as well as an
413201905fc2c50c77555aea8f73444d2841126cPaolo Torriniundefined list function take value $\bot$. This may be regarded as a
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisemantical weakness.
eee2119f1e850ad533252f43212664b25d83e7adPaolo TorriniHaskell allows for local definitions by means of \emph{let} and
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrini\emph{where} expressions. The \emph{let} expressions are translated to
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrinisimilar Isabelle ones; \emph{where} expressions are not covered. The
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinitranslation of terms (minus mutual recursion) may be summed up,
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torriniessentially, as follows:
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski$$\begin{array}{lcl}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \lceil c \rceil & = & c_{t} \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \lceil \backslash x \ \to \ f \rceil & = & LAM \ x_{t}. \ \lceil f \rceil \\
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrini \lceil f \ a_{1} \ldots a_{n} \rceil & = & FIX \ f_{t}. \ f_{t} \ \cdot \
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrini \lceil a \rceil \ldots \cdot \ \lceil a_{n} \rceil \\
eee2119f1e850ad533252f43212664b25d83e7adPaolo Torrini & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \lceil let \ exp_{1} \ \dots \ exp_{n} \ in \ exp \rceil & =
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & let \ \lceil exp_{1} \rceil \ \dots \ \lceil exp_{n} \rceil \ in \ \lceil exp \rceil
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski% \ldots \lceil a_{n} \rceil \ TyCons_{t}
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini%In HOLCF, where every type is a domain and every function is
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\noindent In HOLCF all recursive functions can be defined by fixpoint
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinioperator --- a function that, given as argument the defining term
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiabstracted of the recursive call name, returns the corresponding
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskirecursive function. Coding this directly turns out to be rather
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskicumbersome, particularly in the case of mutually recursive functions,
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torriniwhere tuples of defining terms and tupled abstraction would be needed.
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo TorriniIn contrast, the \emph{fixrec} package allows us to handle fixpoint
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinidefinitions in a way much more similar to ordinary Isabelle recursive
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskidefinitions, providing with friendly syntax for mutual recursion,
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrinias well. Continuing the example,\\
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini\noindent $ fun1 \ :: \ (a \to c) \ \to \ (b \to d) \
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\to \ AType \ a \ b \ \to \ AType \ c \ d $
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini$$\begin{array}{lll}
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini fun1 & f \ g \ k & = \ case \ k \ of \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & ABase \ x & \to \ ABase \ (f \ x) \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski & AStep \ x \ y & \to \ AStep \ (fun1 \ f \ g \ x) \ (fun2 \ f \ g \
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\end{array} $$
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski$ fun2 \ :: \ (a \to c) \ \to \ (b \to d) \ \to \ BType \ a \ b \ \to \ BType \ c \ d $
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski$$\begin{array}{lll}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski fun2 & f \ g \ k & = \ case \ k \ of \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski & BBase \ x & \to \ BBase \ (g \ x) \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski & BStep \ x \ y & \to \ BStep \ (fun2 \ f \ g \ x) \ (fun1 \ f \ g \ y)
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\end{array} $$
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\noindent this code translates to HOLCF as follows:\\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\noindent $consts $
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski$$ \begin{array}{ll} fun1 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to 'd::pcpo) \ \to \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski & ('a::pcpo, 'b::pcpo) \ AType \ \to \ ('c::pcpo, 'd::pcpo) \ AType \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski fun2 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski 'd::pcpo) \ \to \\
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski & ('a::pcpo, 'b::pcpo) \ BType \ \to \ ('c::pcpo,
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski 'd::pcpo) \ BType
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski$$\begin{array}{rccl}
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski fixrec & fun1 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & & ABase \cdot pX1 \ => \ ABase \cdot (f \cdot pX1) \ | \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & & AStep \cdot pX1 \cdot pX2 \ => \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & & \ AStep \cdot (fun1 \cdot f \cdot g \cdot pX1) \cdot (fun2 \cdot f \cdot g \cdot pX2)) \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski and & fun2 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & & BBase \cdot pX1 \ => \ BBase \cdot (g \cdot pX1) \ | \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & & BStep \cdot pX1 \cdot pX2 \ => \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & & \ BStep \cdot (fun2 \cdot f \cdot g \cdot pX1) \cdot (fun1 \cdot f \cdot g \cdot pX2)) \end{array}$$
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski\noindent The translations take care automatically of the fact that,
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiin contrast with Haskell, Isabelle requires patterns in case
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiexpressions to follow the order of datatype declarations.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill MossakowskiIn the Programatica representation of Haskell, class information about
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskitype parameters is given by adding dictionary parameters to normal
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiones. These are eliminated by the translation, as class information in
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill MossakowskiIsabelle may be given by annotating arguments. In particular, each
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskidefinition includes the type of the defined function complete with
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiclass annotation, in order to allow for overloading (a detail we
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiomitted to show for the sake of readability in some of the examples
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski\subsection{HOL: Type signature}
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill MossakowskiThe translation to HOL is semantically rather crude, it takes into
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiaccount neither partiality nor laziness, and so, for soundness, it
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskirequires all functions in the program to be total ones.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill MossakowskiAn account of partiality could be obtained using the \emph{option}
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskitype constructor to lift types, along lines similar to those followed
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiin HOLCF with \emph{lift}. Here instead we are just mapping Haskell
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskitypes to corresponding, unlifted HOL ones --- so for booleans and
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiintegers. Type variables are of class \emph{type}. HOL function type,
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiproduct and list are used to translate the corresponding Haskell
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiconstructors. The translation of types (minus mutual recursion) may be
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskisummed up as follows.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% Haskell datatype and function declarations are translated to
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski% declarations in HOLCF.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski$$\begin{array}{lcl}
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil a \rceil & = & 'a_{t}::type \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil Bool \rceil & = & bool \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil Integer \rceil & = & int \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil a \to b \rceil & = & \lceil a \rceil \Rightarrow \lceil b \rceil \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski \lceil [a] \rceil & = & \lceil a \rceil \ list \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski\noindent Recursive and mutually recursive data-types declarations are
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskitranslated to HOL as datatype declaration.
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski$$\begin{array}{rll} datatype & \ ('a, 'b) \ BType & = \ BBase \ 'b \ | \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & BStep \ (('a, 'b) \ BType) \ (('a, 'b) \ AType) \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski and & \ ('a, 'b) \ AType & = \ ABase \ 'a \ | \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & AStep \ (('a, 'b) \ AType) \ (('a, 'b) \ BType) \\
4d8cfbb65324759c9ca537ff7a364c5fa5372693Paolo Torrini\noindent Metalevel features are essentially shared with the HOLCF
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski\subsection{HOL: Sentences}
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill MossakowskiNon-recursive definitions are treated in an analogous way to the
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskitranslation into HOLCF. Standard lambda-abstraction ($\%$) and
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskifunction application are used here instead of continuous ones. Partial
5d222a875fe9457bbc61140ba06b85cde53b4a62Till Mossakowskifunctions, and particularly case expressions with incomplete patterns,
5d222a875fe9457bbc61140ba06b85cde53b4a62Till Mossakowskiare not allowed. The translation of terms (minus recursion and case
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowskiexpressions) may be summed up as follows:
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski$$\begin{array}{lcl}
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil c \rceil & = & c_{t} \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil \backslash x \ \to \ f \rceil & = & \% \ x_{t}. \ \lceil f \rceil \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil f \ a_{1} \ldots a_{n} \rceil & = & f_{t} \ \lceil a \rceil \ldots \ \lceil a_{n} \rceil \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
d4dc8e8f329453ad4756c92de860d3c1833abf6eTill Mossakowski \lceil let \ exp_{1} \ \dots \ exp_{n} \ in \ exp \rceil & =
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski & let \ \lceil exp_{1} \rceil \ \dots \ \lceil exp_{n} \rceil \ in \ \lceil exp \rceil
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski% \ldots \lceil a_{n} \rceil \ TyCons_{t}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\noindent Recursive definitions set HOL and HOLCF apart. In HOL a
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskidistinction is drawn, and syntactically highlighted, between primitive
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskirecursive functions (introduced by keyword \emph{primrec}) and generic
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskirecursive ones (by keyword \emph{recdef}). Termination is guaranteed
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskifor each of the formers, by the fact that recursion is based on the
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskidatatype structure of one of the parameters. In contrast, termination
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskiis not a trivial matter for the latters. A strictly decreasing measure
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskimust be provided, associated to the parameters of the defined
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskifunction. This requires a degree of ingenuity that cannot be easily
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskidealt with automatically. For this reason, the translation to HOL is
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskirestricted to primitive recursive functions.
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiMutual recursion is allowed for under additional restrictions --- more
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskiprecisely: 1) all the functions involved are recursive in the first
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskiargument; 2) recursive arguments are of the same type in each
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskifunction. The translation of mutually recursive functions $a
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\rightarrow b, \ldots a \rightarrow d$ introduces a new function $a
e1201831787ad2919649a57f359006f30a8fedb0Till Mossakowski\rightarrow (b * \ldots * d)$ recursively defined, for each case
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskipattern, as the product of the values
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskicorrespondingly taken by the original, non-recursively defined ones. \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\noindent $ fun3 \ :: \ AType \ a \ b \to (a \to a) \to AType \ a \ b $
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski$$\begin{array}{ll}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifun3 \ k \ f & = \ case \ k \ of \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & ABase \ a \to ABase \ (f \ a) \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & AStep \ a \ b \to AStep \ (fun4 \ a) \ b \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\noindent $ fun4 \ :: \ AType \ a \ b \to AType \ a \ b $
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski$$\begin{array}{ll}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifun4 \ k & = \ case \ k \ of \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & AStep \ x \ y \to AStep \ (fun3 \ x \ (\backslash z \to z)) \ y \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & ABase \ x \to ABase \ x \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\noindent These functions, satisfying the restrictions, will translate
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskito the following.\\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\noindent $consts$
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski$$\begin{array}{ll}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskifun3 \ :: & ('a::type, 'b::type) AType \Rightarrow ('a::type \Rightarrow 'a::type) \Rightarrow \\ & ('a::type, 'b::type) AType \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskifun4 \ :: & ('a::type, 'b::type) AType \Rightarrow ('a::type \Rightarrow 'a::type) \Rightarrow\\ & ('a::type, 'b::type) AType \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskifun3\_Xfun4\_X :: & ('a::type, 'b::type) AType \Rightarrow \\ & (('aXX1::type \Rightarrow 'aXX1::type) \Rightarrow \\ & ('aXX1::type, 'bXX1::type) AType) * \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski & (('aXX2::type \Rightarrow 'aXX2::type) \Rightarrow \\ & ('aXX2::type, 'bXX2::type) AType) \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\noindent $defs$
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski$$\begin{array}{lll}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskifun3\_def : & fun3 \ == \ \% k \ f. \ fst \ (( fun3\_Xfun4\_X :: \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski & \ ('a::type, 'b::type) AType \Rightarrow (('a::type \Rightarrow 'a::type) \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski& \Rightarrow ('a::type, 'b::type) AType) * ((unit \Rightarrow unit) \Rightarrow \\ & (unit, unit) AType) ) \ k) \ f \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifun4\_def : & fun4 \ == \ \% k \ f. \ snd \ (( fun3\_Xfun4\_X :: \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & ('a::type, 'b::type) AType \Rightarrow ((unit \Rightarrow unit) \Rightarrow (unit, unit) AType) * \\ & (('a::type \Rightarrow 'a::type) \Rightarrow ('a::type, 'b::type) AType) ) \ k) \ f \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\noindent $primrec$
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski$$\begin{array}{lll}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifun3\_Xfun4\_X & (ABase \ pX1) \ = & (\% f. \ ABase \ (f \ pX1), \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & & \% f. \ ABase \ pX1) \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifun3\_Xfun4\_X & (AStep \ pX1 \ pX2) & = \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski & (\% f. \ AStep \ (snd & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2, \\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski & \% f. \ AStep \ (fst & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2) \\
5b465790447d54472837f1084ed3e751c745d0dcTill Mossakowski\noindent Calls of the recursive functions in the non-recursive
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskidefinitions are annotated with type where exceeding type variables are
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskiinstantiated with the unit type, as required by Isabelle in order to
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowskiavoid definitions from which inconsistencies are derivable.
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\subsection{Patterns}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\label{sec:Patterns}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiSupport of patterns in definitions and case expressions is more
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskirestricted in Isabelle than in Haskell. Nested patterns are overall
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskidisallowed. In case expressions, the case term is required to be a
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskivariable. Both of these restrictions apply to our translations. A
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifurther Isabelle limitation concerning case expressions ---
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisensitiveness to pattern order --- is dealt with automatically.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiSimilarly, wildcards --- something unknown to Isabelle --- are dealt
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiwith, as well as, in HOLCF, incomplete patterns. The exclusion of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskinested patterns complicate the translation of some specific ones ---
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiin fact, guarded expressions and list comprehension are not covered;
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskitheir use should be avoided here, using conditional expressions and
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\emph{map} instead.
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski% not allowed in Isabelle with ordinary definitions (keyword
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski% \emph{Defs}), but it is allowed with the syntax for recursive ones.
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiMultiple function definitions using top level pattern matching are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskitranslated as definitions based on a single case expression; this is
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskidue to HOL more than to HOLCF. In fact, multiple definitions in
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIsabelle are only allowed with the syntax of recursive ones. However,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiin HOL primitive recursive definitions, patterns are allowed for only
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniin one parameter. In order to translate definitions with more patterns
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias arguments, without resorting to tuples and to more complex syntax
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(\emph{recdef} instead of \emph{primrec}) we translate multiple
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidefinitions by top level pattern matching
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinias definitions by case construct.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $ctl \ :: \ Bool \to Bool \to Bool \to Bool$ \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ctl \ False \ a \ False \ = \ a $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ctl \ True \ a \ False \ = \ False $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ctl \ False \ a \ True = \ True $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ctl \ True \ a \ True \ = \ a $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent This translates to HOL as the following.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts \ ctl :: \ bool \Rightarrow bool \Rightarrow bool \Rightarrow bool$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $defs$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{llll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinictl\_def : & ctl \ == & \% qX1. \% qX2. \% qX3. & case \ qX1 \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & False \Rightarrow case \ qX3 & of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & & False \Rightarrow qX2 \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & True \Rightarrow True \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & True \Rightarrow case \ qX3 & of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & & False \Rightarrow False \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & & True \Rightarrow qX2 \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent This example does not go through with the translation to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF, as booleans there are translated to values of \emph{tr}, which
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniis not a recursive datatype. The following gives an alternative that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinican be handled (a new datatype is used instead of booleans).\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $data \ Two \ = Fx \ | \ Tx $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $ctlx :: \ Two \to Two \to Two \to Two $ \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ctlx \ Fx \ a \ Fx \ = \ a $ \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ctlx \ Tx \ a \ Fx \ = \ Fx $ \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ctlx \ Fx \ a \ Tx \ = \ Tx $ \\
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski$ctlx \ Tx \ a \ Tx \ = \ a $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent This translates to HOLCF as follows.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $domain \ Two \ = \ Fx \ | \ Tx $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts \ ctlx :: \ Two \to Two \to Two \to Two$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $defs$
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski$$\begin{array}{llll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinictlx\_def : & map5 \ == & LAM \ qX1 \ qX2 \ qX3. & case \ qX1 \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & Fx \Rightarrow case \ qX3 & of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & & Fx \Rightarrow qX2 \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & & Tx \Rightarrow Tx \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & Tx \Rightarrow case \ qX3 & of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & & Fx \Rightarrow Fx \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & & & Tx \Rightarrow qX2 \\
c4e48c487e8797c2a101d15b2fc542d2de4b2246Till Mossakowski\noindent In case expressions as well as in top level pattern matching
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefinitions, wildcards may be used --- though not in nested position.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIncomplete patterns are translated to HOLCF using $\bot$ as default
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{Classes}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell defined classes are translated to Isabelle as classes with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniempty axiomatization. Isabelle allows classes with no more than one
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype parameter, therefore our translations can support only them ---
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniit might be possible to handle more than one parameter using tuples,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibut this would surely involve considerable complications dealing with
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniconditional instances.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniInstance declarations are translated to corresponding ones in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle. Isabelle instances in general require proofs that class
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniaxioms are satisfied by the types, but as long as there are no axioms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe proofs are trivial and can be handled automatically. Function
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideclarations associated with Haskell classes are translated as
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniindependent function declarations with appropriate class annotation.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFunction definitions associated with instance declarations are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslated as overloaded function definitions,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirelying on class annotation of the typed variables.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $class ClassA \ a \ where$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$abase :: \ a \to Bool $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$ astep :: \ a \to Bool $\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $instance \ (ClassA \ a, \ ClassA \ b) \Rightarrow ClassA \ (AType \ a \ b) \ where $
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniabase \ x \ = & case \ x \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ABase \ u \ \to \ True \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & \_ \ \to \ False \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent This code translates to HOLCF as follows.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $axclass \ ClassA < pcpo$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $instance \ AType::({pcpo, ClassA}, {pcpo, ClassA}) \ ClassA$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$by \ intro\_classes$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniabase :: & 'a::\{ClassA, pcpo\} \to tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniastep :: & 'a::\{ClassA, pcpo\} \to tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefault\_abase :: & 'a::\{ClassA, pcpo\} \to tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefault\_astep :: & 'a::\{ClassA, pcpo\} \to tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $defs$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{rl}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAType\_abase\_def : & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini abase :: & ('a::\{ClassA, pcpo\}, 'b::\{ClassA, pcpo\}) \ AType \to tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini == & LAM x. \ case \ x \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ABase \cdot pX1 \Rightarrow TT \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & AStep \cdot pX2 \cdot pX1 \Rightarrow FF \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAType\_astep\_def : & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini astep :: & ('a::\{ClassA, pcpo\}, 'b::\{ClassA, pcpo\}) \ AType \to tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & == default\_astep \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent Similarly, it translates to HOL.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $axclass \ ClassA < type$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $instance \ AType::(\{type, ClassA\}, \{type, ClassA\}) \ ClassA$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$by \ intro\_classes$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniabase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniastep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefault\_abase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefault\_astep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $defs$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{rl}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAType\_abase\_def : & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini abase :: & ('a::\{ClassA, type\}, 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini == & \% x. \ case \ x \ of \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ABase \ pX1 \Rightarrow True \ | \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & AStep \ pX2 \ pX1 \Rightarrow False \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAType\_astep\_def : & \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini astep :: & ('a::\{ClassA, type\}, 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini == & default\_astep\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{Equality}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAt the moment equality is the only covered built-in class. The
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniaxiomatizations provided, respectively, in \emph{HsHOLCF} and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{HsHOL} are based on the abstract definition of the equality and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinequality functions \cite{HaskellRep}. In both theories, \emph{Eq} is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideclared as a subclass of \emph{type} --- in \emph{HsHOLCF} this is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidone in order to instantiate it with lifted types.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$ \begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorrinihEq :: & ('a::Eq) lift \ \to \ 'a \ lift \ \to \ tr \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorrinihNEq :: & ('a::Eq) lift \ \to \ 'a \ lift \ \to \ tr\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $axioms$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniaxEq: & ALL x. (hEq \cdot p \cdot q \ = \ Def x) \ = \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (hNEq \cdot p \cdot q \ = \ Def (\sim x)) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent The instantiation of equality (consequently, of inequality) for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniboolean (and similarly for integer) is obtained by lifting HOL
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniequality so that $\bot$ is returned whenever one of the argument is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $tr\_hEq\_def: \ hEq \ == \ fliftbin \ (\% (a::bool) \ b. \ a \ = \ b)$\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%ax1: & hEq \cdot p \cdot p \ == \ Def \ true \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%ax2: & [| \ hEq \cdot q \cdot r \ = \ Def \ true; \ hEq \cdot p \cdot q \ = \ Def \ true \ |] \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% & ==> \ hEq \cdot p \cdot r \ = \ Def \ true \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent In \emph{HsHOL} the axiomatization reflects the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirestriction to terminating programs.\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorrinihEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorrinihNEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $axioms$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$\begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini axEq: & hEq \ p \ q \ == \ \sim hNEq \ p \ q \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent The instantiation of \emph{hEq} for boolean and integer is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisimply taken to be HOL equality.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% ax1: & hEq \ p \ p \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% ax2: & [| \ hEq \ q \ r; \ hEq \ p \ q \ |] ==> hEq \ p \ r \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{Monads}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\label{sec:Monads}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle does not allow for classes of type constructors, hence a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproblem in representing monads. We could deal with this problem
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirelying on an axiomatization of monads that allows for the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirepresentation of monadic types as an axiomatic class, as presented in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\cite{Lueth}. Monadic types should be translated to newly defined
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitypes that satisfy monadic axioms. This would involve defining a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitheory morphism, as an instantiation of type variables in the theory
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof monads. We are planning to rely on AWE \cite{AWE}, an
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniimplementation of theory morphism on top of Isabelle base logic that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimay be used to extend HOL as well.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Conclusion}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following is a list of features that are covered by our
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\begin{itemize}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item predefined types: boolean, integer.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined type constructors: function, cartesian product, list.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item declaration of recursive datatype, including mutually recursive ones.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item predefined functions: equality, booelan constructors,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini connectives, list constructors, head and tail list functions,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini arithmetic operators.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item non-recursive functions, including conditional, case and let and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item use of incomplete patterns (in HOLCF) and of wildcards in case
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item total primitive recursive functions (in HOL)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand partial recursive ones (in HOLCF), including mutual ones (with
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskirestrictions in the HOL case).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item single-parameter class and instance declarations.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% \item monad declarations and do notation.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe shallow embedding approach makes it possible to take the most out
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof the automation currently available on Isabelle, especially in HOL.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFurther work should include extending the translation to cover the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwhole of the Haskell Prelude. We would also be interested in carrying
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniout an extension to cover P-logic \cite{KiebPl}, a specification
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniformalism for Haskell programs included in the Programatica toolset.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%This translation, due to the character of the P-logic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%typing system, could be more easily carried out relying on some form
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%of universal quantification on type variables, or else further relying
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%on parametrisation.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\bibliographystyle{alpha}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\bibliography{case}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{document}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn our example,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslation gives the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $consts$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$ \begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifun1 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ('a::type, 'b::type) \ Prelude\_AType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_AType \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifun1\_Xfun2\_X & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (('bXX1::type \Rightarrow 'dXX1::type) \ \Rightarrow \\ & ('aXX1::type, 'bXX1::type) \ Prelude\_AType \ \Rightarrow \\ & ('cXX1::type, 'dXX1::type) \ Prelude\_AType) * \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (('bXX2::type \Rightarrow 'dXX2::type) \ \Rightarrow \\ & ('aXX2::type, 'bXX2::type) \ Prelude\_BType \ \Rightarrow \\ & ('cXX2::type, 'dXX2::type) \ Prelude\_BType) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifun2 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & ('a::type, 'b::type) \ Prelude\_BType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_BType \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\noindent $defs$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$$ \begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifun1\_def : & fun1 \ == \ \% f. \% g. \% k. \ fst (fun1\_Xfun2\_X \ f) \ g \ k \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifun2\_def : & fun2 \ == \ \% f. \% g. \% k. \ snd (fun1\_Xfun2\_X \ f) \ g \ k
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $primrec$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fun1\_Xfun2\_X \ (ABase \ pX1) & = \ (\% g. \% k. \ ABase \ (f \ pX1)) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fun1\_Xfun2\_X \ (BBase \ pX1) & = \ (\% g. \% k. \ BBase \ (g \ pX1)) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fun1\_Xfun2\_X \ (AStep \ pX1 \ pX2) & = \ (\% g. \% k. \ AStep \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini fun1\_Xfun2\_X \ (BStep \ pX1 \ pX2) & = \ (\% g. \% k. \ BStep \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{Equality: HOLCF}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{Equality: HOL}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell classes and instances are translated to Isabelle,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirespectively, as classes with empty axiomatisation and as instances
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwith trivial instantiation proof. The translation supports only
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisingle-parameter classes --- in principle, more than one parameter
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicould be handled using tuples.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinihowever here is not provided !!!
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFunctions declarations associated to classes are translated to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle as independent function declarations with appropriate class
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniannotation. Function definitions associated to instances are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslated as overloaded function definitions, relying on class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation of typed variables.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% ...xxx...!!! check out for stuff to include in Classes ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNon-recursive definitions are translated to ordinary definitions (keyword
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{defs}), whereas recursive ones require specific keywords. The
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitype of the function, inclusive of class annotation, is included in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinievery definitions in order to allow for overloading.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%For values of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%built-in type, the lifting function is \emph{Def}; the undefined case
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%collapses on $\bot$.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn HOLCF, where every type is a domain and every function is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicontinuous, all recursive functions can be defined by fixpoint
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinioperator. This is essentially a function that, given as argument the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunction definition body abstracted of the recursive call name,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo 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
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniabstraction are needed. We can instead rely on the \emph{recdef}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipackage, which allows to handle fixpoint definitions like ordinary
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirecursive ones, offering nice syntax to deal with mutual recursion as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Type signature}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo 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.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAn account of partiality -- although possibly not aof laziness ---
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo 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
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniplain version, mapping Haskell types in the corresponding unlifted HOL
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitypes. All variables belong to the class type. Recursive and mutually
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirecursive data-types declarations are translated to HOL datatype
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{HOL: Function definitions}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniNon-recursive definitions and let expressions are treated similarly as
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniin the translation to HOLCF. Recursive defitions is the topic that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinireally sets HOL and HOLCF apart. In HOL a distinction has to be drawn
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibetween primitive recursive functions and generic recursive ones. In
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe former, termination is guaranteed by the fact that recursive
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrinidefinitions are strictly associated with the datatype structure of a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniparameter. In the latter, termination needs to be proved. This must be
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidone, in a \emph{recdef} definition, by providing a measure for the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunction parameter that can be proved to be strictly decreasing for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinieach occurrence of a recursive call in the definition. This requires a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidegree of ingenuity that cannot be generally associated with an
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniautomated translation.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFor this reason, the translation of recursive functions to HOL is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirestricted to primitive recursive ones. Mutually recursive functions
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare allowed under additional restrictions. These are: all the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifunctions should be recursive in the first argument; this should be of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe same type for each of them; the constructors should be listed in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe same order in each of the case expressions; the variable names in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe case patterns are expected to be maintained.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe translation of mutually recursive functions $a \rightarrow b, \ldots a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefined, for each case pattern, as the product of the values
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicorrespondingly taken by the original functions.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{Pattern matching}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniSupport of pattern-matching in Isabelle is more restricted than in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell. Nested patterns are disallowed; case expressions are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisensitive to the order of the constructors, which should be the same
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinias in the datatype declaration. In particular, the case variable si
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequired to be a variable. Translation of pattern-matching is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipotentially laborious. For this reason guarded expressions, list
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicomprehension and nested pattern-matching have been left out; they
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinishould be replaced by the programmer, using conditional expressions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand map functions.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFunction definition by top level pattern matching is not allowed in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIsabelle with ordinary definitions, but it is with those that are
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniexplicitly declared to be recursive ones. However, particularly in HOL
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniprimitive recursive definitions patterns are allowed in one parameter
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinionly. In order to translate function definitions with patterns in more
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithan one parameter, without resorting to using tuples and more complex
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidefinitions (\emph{recdef} instead of \emph{primrec}), our
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslations turn a multiple definition by top level pattern matching
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto a definition by case construct.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Classes}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell classes and instances are translated to Isabelle,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirespectively, as classes with empty axiomatisation and as instances
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniwith trivial instantiation proof. The translation supports only
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisingle-parameter classes --- in principle, more than one parameter
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicould be handled using tuples.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinihowever here is not provided !!!
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo 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
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitranslated as overloaded function definitions, relying on class
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniannotation of typed variables.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section*{Haskell2Isabelle}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo 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
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilimitations are related to built-in types, pattern-matching and local
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidefinitions. There are additional and more substantial restrictions
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniin the case of HOL, related to termination and to recursion.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe application can be installed as part of Hets. It requires Haskell
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniGHC and Programatica. It is run by the command \emph{hets -t ...
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo 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.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{IsaSign.hs} contains the Hets representation of the Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibase logic and extensions.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe general design of the translation functions, and particularly the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitwo-layered recursion adopted for them, is similar to that used for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe translation Haskell to Agda in Programatica.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\subsection{Monads}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiIsabelle does not allow for classes of type constructors, hence a
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiproblem in representing monads. We can deal with this problem,
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskihowever, relying on an axiomatisation of monads that allows for the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskipresentation of monadic types as an axiomatic class, as provided in
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\cite{}. Therefore, monadic types can be translated to newly defined
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitypes that are constrained to satisfy the monadic axioms. This
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiconstraining, carried out as an instantiation of type variables in the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitheory of monads, takes the form of a theory morphism, and can be
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicarried out automatically by AWE, an implementation of parametrisation
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiand theory morphism on top of Isabelle basic logic, that may also be
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiused to extend HOL and HOLCF. The do notation can then be translated
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiby unpacking it into monadic operators. Attempting to translate
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskimonadic notation without support AWE support will result in an error
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\section*{Conclusion}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe following is a list of constructs that are covered by all the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{itemize}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item predefined types: boolean, integer.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item predifed type constructors: funtion, cartesian product, list.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item declaration of recursive datatype, including mutually recursive ones.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item predefined functions: equality, booelan constructors,
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski connectives, list constructors, head and tail list functions,
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski arithmetic operations.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item non-recursive functions, including conditional,
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskilet and case expressions.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item use of incomplete patterns (HOLCF) and of wildcards in case
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item total primitive recursive functions (HOL)
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiand partial recursive ones (HOLCF), including mutual ones (with
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskirestrictions in the HOL case).
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item class and instance declarations.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item monad declarations and do notation.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe shallow embedding approach used by our translations should allow
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskito take as much advantage as possible of the automation currently
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiavailable on Isabelle, particularly in HOL.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiFurther work should include extending the translation to cover the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiwhole of the Haskell Prelude. We hope that this will make it possible
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskito support the verification of functional robotics programs.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiA further extension, in line with the work on Programtica, would be
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe translation of P-logic. This translation, due to the character of
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe P-logic typing system, could be more easily carried out relying on
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskisome form of universal quantification on type variables, or else
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifurther relying on parametrisation.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\bibliographystyle{alpha}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\bibliography{case}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\end{document}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe translation of types is
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiOur general strategy for translating signatures is to map Haskell
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitypes to Isabelle defined types.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski the fact that Haskell expressions are
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskievaluated lazily, however it does not preserve The translation to HOL
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidoes not, and moreover requires that all the functions defined in the
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiHaskell program are total ones...
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiAll types have a sort in Isabelle, defined by the set of the classes
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiof which it is a member. In HOL, all types belong to the class type;
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiin HOLCF, they belong to class pcpo (pointed complete poset).
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiAll Haskell function declarations are translated to Isabelle ones.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiType variables are assigned default sort type in HOL and pcpo in
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiHOLCF. Names get translated by a function that preserves them, up to
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiavoidance of clashes with Isabelle keywords.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe only built-in types that are properly covered are booleans,
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiunbounded integers and rationals. These get translated, in the case of
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiHOL, to Isabelle booleans, integers and rationals, respectively. Bound
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiintegers and floating point numbers would require low-level modelling,
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiand have not been dealt with; anyway, bounded integers are accepted
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiand simply treated as unbounded by the application.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiIn the HOLCF translation, all built-in types get lifted to the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicorresponding domains (pcpos), which by definion include the undefined
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskivalue, by using the lift HOLCF type constructor. In particular, type
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiboolean get translated to type tr (short for bool lift), and similarly
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifor types integer and rational.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiRecursive data-types declarations can be translated to datatype
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskideclarations in HOL. In HOLCF they can be translated to domain
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskideclarations. The two structure are quite similar, except that in
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidomains, which are pcpo, all the parameters are required to be pcpos
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskias well. Morevover, Isabelle domain declarations require to introduce
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskinames for destructors. Mutually recursive Haskell datatypes can be
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitranslated to both logics, relying on the specific Isabelle syntax for
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiA type class in Isabelle is conceptually quite different from one in
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiHaskell. The former is associated to a set of axioms, whereas the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskilatter is associated to a set of function declarations. Isabelle
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiclasses may have at most a type parameter. Moreover, Isabelle does
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskinot allow for type constructor classes. The last limitation is the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskimost serious of the three, since it makes quite hard to cope with
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskimonads. We can get around this obstacle relying on a method for the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiaxiomatic encoding of monads in HOL that uses parametrisation.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiParametrisation based on theory morphism has been implemented, as a
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiconservative extension of various Isabelle logics, in AWE, a tool
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidesigned to support proof reuse \cite{AWE}.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe \emph{lift} type constructor, in particular, lifts each HOL type
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskito a flat domain, by adding a bottom element to them. We are going to
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiuse it to lift the basic types. For the product we are going to use
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskinon-strict product.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiformalisation on Isabele relies on axiomatic type classes \cite{},
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiwith \emph{pcpo} (pointed complete partial order) as the default
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiclass, in which the type of continuous functions can be represented as
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifunction spaces, allowing for an elegant interpretation of recursion
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiby fixpoint operator. HOL types may be lifted to \emph{pcpo} by simply
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiadding a bottom element to them. This is what the type constructor
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\emph{lift} does, thus providing also a way of handling partiality ---
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiundefined cases can be mapped to the bottom element. HOLCF has also a
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitype constructor \emph{u} that allows to deal with laziness, by
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiguaranteeing $\bot \neq \smath{up} \$ (\bot)$.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIn the case of HOLCF, the logic provides a computational
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiinterpretation of function types as domains. In HOL there is no such
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifacility, therefore either appropriate types for the translation are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiintroduced --- as in \cite{}, or considerable semantical restrictions
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskimust be accepted --- this is also the case for one of the translation
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskito FOL proposed in \cite{}.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiDepending on the expressiveness of the logic, the translation of the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiprogramming language may be carried out at different levels of depth.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIn general, the deeper is the embedding, the less it relies on
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskimeta-level features of the target language. This may be a plus, either
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifrom the point of view of semantic clarity, or from that of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiexpressiveness. Taking advantage of meta-level feaures, on the other
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskihand, may be useful in order to make the theorem proving less tedious,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiby allowing more constant use of generic proof methods. It may also
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiultimately affect positively the theorem prover economy, by
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskireinforcing the bias toward the development of proof methods that,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskihowever specific, can be more easily integrated with generic ones.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% a point made in \cite{}. for example by allowing a straightforward
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% operational interpretation ---
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe translations of Haskell to HOLCF and HOL that we are presenting in
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithe following justify themselves in terms of denotational semantics.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe translation to HOLCF differs from that proposed in \cite{} in the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskitreatment of types. We translate Haskell types directly into HOLCF
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiones, whereas they use HOLCF terms to embed Haskell types. We assume
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithat the HOLCF types are similar enough to the those of Haskell, in
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiorder to guarantee the semantical correctness of our translations.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiMoreover, we rely on axiomatic classes to translate Haskell types
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiOur approach has the advantage of giving a shallower embedding,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskihowever it has the drawback of not bein complete --- notably, type
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiconstructor classes are missing. We plan to handle in future this
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiproblem (see section~\ref{sec:Monads}) by relying on an extension of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIsabelle based on morphism between theories. The translation into HOL
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiis essentialy only a first experiment, it handles types very
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisimplistically, relying on drastic semantical restrictions for
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskicorrecteness. Under those restrictions, however, it gives expressions
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithat are comparatively quite simple to work with.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiA type class in Isabelle is conceptually quite different from one in
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiHaskell. The former is associated to a set of axioms, whereas the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskilatter is associated to a set of function declarations. Isabelle
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiclasses may have at most a type parameter. Moreover, Isabelle does
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskinot allow for type constructor classes. The last limitation is the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskimost serious of the three, since it makes quite hard to cope with
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskimonads. We can get around this obstacle relying on a method for the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiaxiomatic encoding of monads in HOL that uses parametrisation.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiParametrisation based on theory morphism has been implemented, as a
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiconservative extension of various Isabelle logics, in AWE, a tool
[h|hc|mh|mhc] file.hs} where the options stand, respectively, for
For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
and \emph{IsaSign.hs} contains the internal representation of Isabelle