hs2isa.tex revision 12138d113e5e25fc91b7e8ba0a179a3da00b9a91
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Author: Paolo Torrini <paolot@helios.dai.ed.ac.uk>
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Created: Mon Feb 15 1999
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\documentclass[a4paper,12pt]{article}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage[dvips]{graphics}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{amsfonts}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{amssymb}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%\usepackage{psfig}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{fancybox}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{epsfig}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{graphicx}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{color}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%\usepackage{semrot}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\input{newmacros}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Use \includegraphics{*.eps} for pictures
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% Enlarge printing area a bit:
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\textwidth}{16cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\oddsidemargin}{0cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\evensidemargin}{0cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\topmargin}{-0.94cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\setlength{\textheight}{23cm}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\begin{document}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\title{Translating Haskell to Isabelle logics in Hets}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\author{Paolo Torrini, Till Mossakowski, Christian Maeder}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% \\ Fachbereich Mathematik und Informatik, Universitaet Bremen}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\abstract{\scriptsize \bf Automated, partial translations of Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini into Isabelle higher-order logic (with or without computable
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini functions) have been implemented as functions of Hets, a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Haskell-based proof-management and program development system that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini allows for integration with other tools. The application, built on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini top of Programatica-style static analysis, can translate simple
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Haskell programs to HOLCF and, under stronger restrictions, to HOL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Both translations are based on shallow embedding and rely
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini informally on denotational semantics.}\\
984e73d7bd9693bb0f113d956969b7d1483f5925Paolo Torrini% The translation of monads uses the AWE extension of Isabelle.}\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWork on the integration of compilers, analyzers and theorem-provers,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well as translations between programming and specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilanguages, may help on the way to making formal development and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniverification of programs more viable. In order to verify formally a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprogram, we need to formulate the requirements in a logic that also
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniallows for the program to be represented; to translate the program to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe logic; finally, to carry out a proof of the correctness statement.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAlthough specifications and proofs require normally the biggest amount
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof work, translations can also be a significant source of potential
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproblems. For the verification to be reliable and efficient, the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation should rest on the definition of a formal semantics of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprogramming language in the specification logic; it should be carried
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniout safely, at best automatically; it should also give program
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirepresentations that do not make proofs more complex than necessary.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIt has long been argued that functional languages, based on notions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicloser to general, mathematical ones, can make the task of proving
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniassertions about them easier, owing to the clarity and relative
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimplicity of their semantics \cite{Thompson92}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn this report we are presenting automated translations based on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotational semantics of Haskell programs into Isabelle higher-order
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilogic. Haskell is a strongly typed, purely functional language with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilazy evaluation. It relies on a system of polymorphic types extended
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith type constructor classes, and has a syntax for side effects and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipseudo-imperative code based on monadic operators \cite{HaskellRep}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations are implemented as functions of Hets \cite{Hets}, an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell-based application designed to support integration of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecification formalisms for the development of Haskell programs. Hets
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisupplies with parsing, static analysis, proof management and interface
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito various language-specific tools. From the point of view of generic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheorem proving, Hets relies on an interface with Isabelle, a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistate-of-the-art interactive theorem-prover, written in SML, allowing
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor the formalization of a variety of logics \cite{Paulson94isa}. Hets
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirelies on Programatica \cite{Prog04} for the parsing and static
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinianalysis of Haskell programs. Programatica is a Haskell-specific
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformal development system built at OGI, envisioned to provide more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithan analysis. Its own proof management includes a specification logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand translations to different proof tools, notably to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Huff}. In section~\ref{sec:Translations} it is going to be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclarified how our work differs from theirs.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Isabelle}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle-HOL (hereafter simply HOL) is the implementation in Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof classical higher-order logic based on simply typed lambda calculus,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniextended with axiomatic type classes. It provides considerable support
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor reasoning about programming functions, both in terms of libraries
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand automation. Since the late nineties, it has essentially superseded
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFOL (classical first-order logic) as the logic of standard use in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle. HOL has an implementation of recursive functions based on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniKnaster-Tarski fixed-point theorem. All functions are total;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipartiality may be dealt with by lifting types through the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{option} type constructor.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF \cite{holcf} is HOL conservatively extended with the logic of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomputable functions --- a formalization of domain theory. In HOL,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes are just sets; functions may not be computable, and a recursive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction may require discharging proof obligations already at the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinition stage --- in fact, a specific measure has to be given for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe function to be proved monotonic. In contrast, domain theory has
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieach type interpreted as a \emph{pcpo} (pointed complete partially
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniordered set) that is, as a set with a partial order which is closed
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniw.r.t. $\omega$-chains and has a bottom. All functions defined over
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidomains, including partial ones, are continuous, therefore computable.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRecursion can be expressed in terms of least fixed-point operator, and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniso, in contrast with HOL, function definition is never dependant on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe Isabelle formalization of HOLCF is based on axiomatic type classes
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Wenzel}, following an approach that makes it possible to deal
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith complete partial orders while abstracting away from any specific
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirelation. The class of types is \emph{pcpo} --- whereas in HOL it is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{type}. Domain theory offers a good basis for the semantical
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinianalysis of programming languages; however, it may make proofs
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomparatively hard. After being spared the need to discharge proof
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniobligations at the defining stage, one has to bear with assumptions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniover the continuity of functions while proving theorems. A standard
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistrategy to get the best out of the two systems is to define as much
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias possible in HOL language, using HOLCF type constructors to lift
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes to domains only when this is needed.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Translations}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:Translations}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA translation may be carried out relying on different semantical
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniapproaches and at different levels of depth, depending mainly on the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressiveness of the target logic. Different formalisms may make the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniembedding of certain features more or less hard. Translations into FOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisuch as those based on large-step operational semantics of Miranda
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Thompson95,Thompson89,Thompson95b} and Haskell \cite{Thompson92}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicannot deal straightforwardly at first order with higher-order
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifeatures such as currying. The translation of Haskell to the Agda
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimplementation of Martin-Loef type theory in \cite{Abel} gets
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomplicated dealing with Haskell polymorphism. The expressiveness of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihigher-order logic help overcome more plainly most of these obstacles,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand makes it possible to adopt a higher-level approach based on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotational semantics, as proposed in \cite{Huff} to translate
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell to HOLCF, and used in \cite{Pollack} to translate ML to HOL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThis approach allows for representations of programs that are closer
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito their specification as well as for proofs that are relatively more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabstract and general.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniExpressiveness plays an important role in the ``depth'' issue, as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwell. A shallow embedding is one that relies as much as possible on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibuilt-in features and packages provided with the implementation of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitarget language, especially with respect to general features such as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes, classes, and recursion. The deeper the embedding, the less it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirelies on such features. This independence may be a plus from the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipoint of view of semantic clarity and logical generality ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniobject-logical, ``deep'' translation can be used to overcome
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{ad-hoc} limitations imposed by the built-in, meta-level
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifeatures. Taking advantage of those features, on the other hand, may
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihelp make the theorem proving less tedious and make it easier to rely
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinion common proof methods.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation of ML in \cite{Pollack} gives an example on the deep
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniside --- a class of types with bottom elements is defined in HOL for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe sake of the embedding. On the other hand, the translation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell to HOLCF proposed in \cite{Huff} relies on a generic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformalization of domain theory, particularly on the \emph{fixrec}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipackage for recursive functions (part of HOLCF in Isabelle 2006)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideveloped in order to provide with a friendly syntax that covers
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimutually recursive definitions, too. Not even this translation is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishallow as far as types are concerned, though. In order to capture an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimportant feature of the Haskell type system, notably type constructor
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses, Haskell types are not translated to HOLCF types, rather they
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare to terms, relying on a modelling of the Haskell type system at the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniobject level. In this way it is possible to give a complete account
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the type system. The practical drawback is that plenty of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniautomation built into the Isabelle type checking is lost, unless one
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis prepared to reimplement a lot.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations of Haskell to HOLCF and HOL that we are presenting
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihere are based on denotational semantics keeping to a shallow
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniapproach. The translation to HOLCF relies on the \emph{fixrec}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipackage, along similar lines to those in \cite{Huff}. In contrast with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithem, we translate Haskell types to HOLCF types, quite directly, and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell classes to Isabelle axiomatic classes, wishing to take
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieffectively advantage of Isabelle type checking. We rely on the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniassumption that types in HOLCF are similar enough to those in Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito allow for embedding, save for possible implementation subtleties
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat we are not going to consider. We expect that operational
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniequivalence between Haskell programs and their translation to HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniholds up to the level of typeable output. The translation covers a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisignificant part of the syntax used in the Prelude, although it is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistill incomplete in one important respect --- it does not include type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructor classes; we have plans, however, for an extention that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishould address this aspect as well.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniConceptually, type classes in Isabelle are quite different from those
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin Haskell. The formers are associated with sets of axioms, whereas
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe latters come with sets of function declarations. Isabelle classes
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimay have at most a single type parameter. Most importantly, Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidoes not allow for type constructor classes. The last limitation is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniserious, since it makes hard to cope with essential Haskell features
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisuch as monads and \emph{do} notation. In alternative to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitreatment of types proposed in \cite{Huff}, we would like to get
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaround the obstacle by relying on an extension of Isabelle based on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory morphism (see section~ \ref{sec:Monads}). The AWE system \cite{AWE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis in fact an implementation of such an extension.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOur translation to HOL, shallow as well, is much more limited. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimost important restriction is related to recursion --- only primitive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions are covered. This limitation appears relatively
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihard to overcome, given the way syntax for full recursion works in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL. Operational equivalence up to typeable output for the remaining
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifragment would require using option types, but we do not pursue it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihere, rather we rely on a restriction to terminating programs for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisemantical correctness. Under such restrictions, however drastic,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithis translation gives expressions that are particularly simple and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitherefore potentially useful to verify some properties.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Haskell2Isabelle}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe Hets function \emph{Haskell2Isabelle} supports the translation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimple Haskell programs to HOLCF and, with more restriction, to HOL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNot all the syntactical features used in the Prelude and main
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilibraries are covered. Some of the most noticeable limitations are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithose related to built-in types, pattern-matching, local definitions,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimport and export. There are additional and more substantial
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestrictions in the case of HOL, related to termination and recursion.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniEach of the translations relies on a \emph{base theory}. These are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle theory files, respectively \emph{HsHOLCF}, extending HOLCF,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand \emph{HsHOL}, extending HOL, which are included in the Hets
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidistribution. Each of them provides definitions and axiomatizations of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininotions that are used in the corresponding translation --- notably
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniInformation for the use of Hets may be found in \cite{HetsUG} and a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinigeneral outlook in \cite{HetsUG}. The Haskell-to-Isabelle translation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequires essentially GHC, Isabelle 2006 and Programatica --- with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirespect to the latter, both analysis and translation functions in Hets
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimake use of its modules. The command to run the application is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{hets -v[1--5] -t Haskell2Isabelle[HOLCF | HOL] -o thy filename}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent where options set verbosity, target logic and name of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioutput file. The input file (last argument) must be a GHC source
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(\emph{hs} extension). The Haskell program gets analyzed and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated. The result of a successful execution is an Isabelle theory
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifile (\emph{thy} extension) depending on the corresponding base
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%The application requires essentially Haskell GHC and Programatica. It
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%is run by the command \emph{hets -t ... [h|hc] file.hs} where the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%options stand for HOL and HOLCF, respectively.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe internal representation of Haskell in Hets (module
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{Logic\_Haskell} and particularly \emph{HatAna}) is essentially
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe same as in Programatica, whereas the internal representation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle (module \emph{Logic\_Isabelle} and particularly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{IsaSign}) is a Haskell reworking of the ML definition of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle own base logic, extended in order to allow for a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistraightforward representation of HOL and HOLCF.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell programs as well as Isabelle theories are internally
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirepresented as Hets theories --- each of them a data-structures formed
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby a signature and a set of sentences, fitting a theoretical framework
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidescribed in \cite{MossaTh}. Each translation, defined as composition
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the signature translation with the translation of all sentences,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihas the structure of a morphism from theories in the internal
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirepresentation of the source language to those in the representation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the target language. The distribution module
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{Haskell2IsabelleHOLCF} contains the main function, dependent on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe target logic. The module \emph{IsaPrint} provides the essential
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions for the pretty-printing of Isabelle theories.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following gives a list of reserved names, i.e. the names that are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniused in order to either rename or name automatically variables and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstants in the translations. 1) Type variables, in the translation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito HOL: \emph{'vX}; any name terminating with \emph{'XXn} where $n$ is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinian integer. 2) Term variables, in both translations: \emph{pXn},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{qXn}, with $n$ integer. 3) Constants, in the translation to HOL:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistrings obtained by joining together names of defined functions, using
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{\_X} as end sequence and separator.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Correspondingly, the translation function is defined as the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%composition of signature translation with the translation of all
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%structure of a morphism from Hets theories written in the language of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%the source internal representation to those in the language
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%representation of the target language. Internally, the information
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%about types is collected into a signature, whereas datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%declarations and definitions are associated with sentences.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% For the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% module that contains the main translation function, carried out as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% composition of a signature morphism and a theory morphism.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \emph{IsaSign.hs} contains the Hets representation of the Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% base logic and extensions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% The general design of the translation functions, and particularly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% the two-layered recursion adopted for them, is similar to that used
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% for the translation Haskell to Agda in Programatica.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOLCF: Type signature}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOLCF keeps into account partiality, i.e. the fact
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat a function might be undefined for certain values, either because
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinition is missing, or because the program does not terminate. It
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialso keeps into account laziness, i. e. the fact that by default
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction values in Haskell are passed by name and evaluated only when
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinineeded. Essentially, we are following the main lines of the ``crude''
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotational semantics for lazy evaluation in \cite{winskel}, pp.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini216--217. Raising an exception is different from running forever, and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniboth are different from stopping short of evaluation. However, from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe point of view of the printable output, these behaviours are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimilar and can be treated semantically as such, i.e. using one and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe same bottom element.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% In order to ease the translation of some notions, the Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% theory \emph{HsHOLCF.thy}, that extends HOLCF has been defined and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% included in the Hets distribution.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% It is often convenient to define in Isabelle notions that match the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% translation of some itmes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% Haskell datatype and function declarations are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% declarations in HOLCF. Names are translated by a function that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% preserves them, up to avoidance of clashes with HOLCF keywords.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniEach type in Isabelle has a sort, defined by the set of the classes of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhich it is member. Haskell type variables are translated to HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniones, of class \emph{pcpo}. Each built-in type is translated to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilifting of its corresponding HOL type. Properly covered are Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibooleans and unbounded integers, associated respectively to HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibooleans and integers.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Rationals need to be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%imported in order to be used in Haskell, so they are not covered by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%the translation at the present stage (import has not been dealt with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%and rationals.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBound integers and floating point numbers would need low-level
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimodelling, and have not been covered. Bounded integers in particular
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare simply treated as unbounded in the translation. The HOLCF type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructor \emph{lift} is used to lift HOL types to flat domains. In
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe case of booleans, we can use type \emph{tr}, defined as equal to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$bool \ lift$ in HOLCF. In the case of integers, we use \emph{dInt},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefined in \emph{HsHOLCF} to equal $int \ lift$. The types of Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions and product are translated, respectively, to HOLCF function
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispaces and lazy product --- i.e. such that $\bot = (\bot * \bot) \neq
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(\bot*'a) \neq ('a * \bot)$, consistently with lazy evaluation. Type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructors are translated to corresponding HOLCF ones (noticeably,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniparameters precede type constructors in Isabelle syntax). In
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniparticular, lists are translated to the domain \emph{llist} defined in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{HsHOLCF}. Function declarations are translated to HOLCF ones
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(keyword \emph{consts}). Names (for types as well as for terms) are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated by a function ($t$ here) that preserves them, up to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavoidance of clashes with HOLCF keywords. Translation of types (minus
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimutual recursion) may be summed up as follows:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% Haskell datatype and function declarations are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% declarations in HOLCF.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lcl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \rceil & = & 'a_{t}::pcpo \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil Bool \rceil & = & tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil Integer \rceil & = & dInt \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \to b \rceil & = & \lceil a \rceil \to \lceil b \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil [a] \rceil & = & \lceil a \rceil \ llist \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent In HOL, datatype declarations define types of class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{type} by keyword \emph{datatype}; in contrast, in HOLCF, they
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefine types of class \emph{pcpo} (i.e. domains) by keyword
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{domain} (so we also may call them \emph{domain declarations}).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniEach recursive datatype declaration in Haskell is translated to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorresponding one in HOLCF. The translation of mutually recursive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidatatypes relies on specific Isabelle syntax (keyword
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{and}), as in the next example.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$data \ AType \ a \ b \ = \ ABase \ a \ | \ AStep \ (AType \ a \ b) \ (BType \ a \ b) $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$data \ BType \ a \ b \ = \ BBase \ b \ | \ BStep \ (BType \ a \ b) \ (AType \ a \ b) $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini and & \ ('a::pcpo, 'b::pcpo) \ AType \ = \ ABase \ (ABase\_1::'a) \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ (AStep\_1::('a, 'b) \ AType) \ (AStep\_2::('a, 'b) \ BType) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Notably, domain declarations require an explicit
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintroduction of destructors. Both translations (to HOL as well as to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF) take care automatically of the order of datatype declarations
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini--- this is needed, insofar as, differently from Haskell, Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequires them to be listed according to their order of dependency.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOLCF: Sentences}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniEach Haskell function definition is translated to a corresponding one.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNon-recursive definitions are translated to standard ones (keyword
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{defs}), whereas the translation of recursive definitions relies
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinion the \emph{fixrec} package. Lambda abstraction is translated as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicontinuous abstraction (\emph{LAM}), and function application as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicontinuous application (the \emph{dot} operator) --- these notions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicoincide with the corresponding, HOL-defined ones, whenever their
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniarguments are continuous.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% As to the translation of terms containing either values or operators
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% of built-in type, it is often the case that we translate them to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% lifted HOL operators. The lifting function is \emph{Def}; $\bot$ is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% used for the undefined case.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTerms of built-in type (boolean and integers) are translated to lifted
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL values, using the HOLCF-defined lifting function \emph{Def}. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibottom element $\bot$ is used for all undefined terms. The following
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperator, defined in \emph{HsHOLCF}, is used to map binary arithmetic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions to lifted functions over
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilifted integers.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$fliftbin :: ('a \Rightarrow \ 'b \Rightarrow \ 'c)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \Rightarrow ('a \ lift \to \ 'b \ lift \to \ 'c \ lift) $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$fliftbin \ f \ == \ LAM \ y x. \ (flift1 \ (\%u. \ flift2 \ (\%v. \ f \ v \ u))) \cdot x \ \cdot y $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Booleans are translated to values of \emph{tr} ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{TT}, \emph{FF} and $\bot$, and boolean connectives are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated to the corresponding HOLCF-defined lifted operators.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF-defined \emph{If then else fi} and \emph{case} syntax are used
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito translate, respectively, conditional and case expressions. There
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare some restrictions, however, on the latters, due to limitations in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe translation of patterns (see section~\ref{sec:Patterns}); in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniparticular, the case term should always be a variable, and no nested
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipatterns are allowed.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation of lists and list constructors relies on the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifollowing \emph{HsHOLCF}-defined datatype.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$domain \ 'a\ llist \ = \ lNil \ | \ lCons \ (lazy \ lHd ::'a) \ (lazy \ lTl ::'a \ llist) $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Under the given interpretation, a stream as well as an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniundefined list function take value $\bot$. This may be regarded as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisemantical weakness.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell allows for local definitions by means of \emph{let} and
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini\emph{where} expressions. The \emph{let} expressions where the
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrinileft-hand side is a variable are translated to similar Isabelle ones;
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torriniother \emph{let} expressions (i.e. those containing patterns on the
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrinileft hand-side) and the \emph{where} expressions are not covered. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation of terms (minus mutual recursion) may be summed up,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniessentially, as follows:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lcl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil c \rceil & = & c_{t} \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil \backslash x \ \to \ f \rceil & = & LAM \ x_{t}. \ \lceil f \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil f \ a_{1} \ldots a_{n} \rceil & = & FIX \ f_{t}. \ f_{t} \ \cdot \
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \rceil \ldots \cdot \ \lceil a_{n} \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini & let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \ldots \lceil a_{n} \rceil \ TyCons_{t}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%In HOLCF, where every type is a domain and every function is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent In HOLCF all recursive functions can be defined by fixpoint
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperator --- a function that, given as argument the defining term
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabstracted of the recursive call name, returns the corresponding
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive function. Coding this directly turns out to be rather
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicumbersome, particularly in the case of mutually recursive functions,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhere tuples of defining terms and tupled abstraction would be needed.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn contrast, the \emph{fixrec} package allows us to handle fixpoint
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions in a way much more similar to ordinary Isabelle recursive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions, providing with friendly syntax for mutual recursion,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well. Continuing the example,\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ fun1 \ :: \ (a \to c) \ \to \ (b \to d) \
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\to \ AType \ a \ b \ \to \ AType \ c \ d $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1 & f \ g \ k & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ x & \to \ ABase \ (f \ x) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ x \ y & \to \ AStep \ (fun1 \ f \ g \ x) \ (fun2 \ f \ g \
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{array} $$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ fun2 \ :: \ (a \to c) \ \to \ (b \to d) \ \to \ BType \ a \ b \ \to \ BType \ c \ d $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun2 & f \ g \ k & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & BBase \ x & \to \ BBase \ (g \ x) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & BStep \ x \ y & \to \ BStep \ (fun2 \ f \ g \ x) \ (fun1 \ f \ g \ y)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{array} $$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent this code translates to HOLCF as follows:\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll} fun1 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to 'd::pcpo) \ \to \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('a::pcpo, 'b::pcpo) \ AType \ \to \ ('c::pcpo, 'd::pcpo) \ AType \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun2 \ :: & ('a::pcpo \to 'c::pcpo) \ \to \ ('b::pcpo \to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini 'd::pcpo) \ \to \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('a::pcpo, 'b::pcpo) \ BType \ \to \ ('c::pcpo,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini 'd::pcpo) \ BType
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rccl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fixrec & fun1 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & ABase \cdot pX1 \ => \ ABase \cdot (f \cdot pX1) \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & AStep \cdot pX1 \cdot pX2 \ => \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & \ AStep \cdot (fun1 \cdot f \cdot g \cdot pX1) \cdot (fun2 \cdot f \cdot g \cdot pX2)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini and & fun2 & = & (LAM f. \ LAM g. \ LAM k. \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & BBase \cdot pX1 \ => \ BBase \cdot (g \cdot pX1) \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & BStep \cdot pX1 \cdot pX2 \ => \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & \ BStep \cdot (fun2 \cdot f \cdot g \cdot pX1) \cdot (fun1 \cdot f \cdot g \cdot pX2)) \end{array}$$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent The translations take care automatically of the fact that,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin contrast with Haskell, Isabelle requires patterns in case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressions to follow the order of datatype declarations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the Programatica representation of Haskell, class information about
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype parameters is given by adding dictionary parameters to normal
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniones. These are eliminated by the translation, as class information in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle may be given by annotating arguments. In particular, each
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinition includes the type of the defined function complete with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclass annotation, in order to allow for overloading (a detail we
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniomitted to show for the sake of readability in some of the examples
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Type signature}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOL is semantically rather crude, it takes into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaccount neither partiality nor laziness, and so, for soundness, it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequires all functions in the program to be total ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAn account of partiality could be obtained using the \emph{option}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype constructor to lift types, along lines similar to those followed
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin HOLCF with \emph{lift}. Here instead we are just mapping Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes to corresponding, unlifted HOL ones --- so for booleans and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintegers. Type variables are of class \emph{type}. HOL function type,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproduct and list are used to translate the corresponding Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructors. The translation of types (minus mutual recursion) may be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisummed up as follows.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% Haskell datatype and function declarations are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% declarations in HOLCF.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lcl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \rceil & = & 'a_{t}::type \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil Bool \rceil & = & bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil Integer \rceil & = & int \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil a \to b \rceil & = & \lceil a \rceil \Rightarrow \lceil b \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil (a,b) \rceil & = & \lceil a \rceil * \lceil b \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil [a] \rceil & = & \lceil a \rceil \ list \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil \ldots \lceil a_{n} \rceil \ TyCons_{t}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Recursive and mutually recursive data-types declarations are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated to HOL as datatype declaration.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rll} datatype & \ ('a, 'b) \ BType & = \ BBase \ 'b \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & BStep \ (('a, 'b) \ BType) \ (('a, 'b) \ AType) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini and & \ ('a, 'b) \ AType & = \ ABase \ 'a \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & AStep \ (('a, 'b) \ AType) \ (('a, 'b) \ BType) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Metalevel features are essentially shared with the HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Sentences}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNon-recursive definitions are treated in an analogous way to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation into HOLCF. Standard lambda-abstraction ($\%$) and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction application are used here instead of continuous ones. Partial
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions, and particularly case expressions with incomplete patterns,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare not allowed. The translation of terms (minus recursion and case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressions) may be summed up as follows:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lcl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil x::a \rceil & = & x_{t}::\lceil a \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil c \rceil & = & c_{t} \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil \backslash x \ \to \ f \rceil & = & \% \ x_{t}. \ \lceil f \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil (a,b) \rceil & = & (\lceil a \rceil, \lceil b \rceil) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \lceil f \ a_{1} \ldots a_{n} \rceil & = & f_{t} \ \lceil a \rceil \ldots \ \lceil a_{n} \rceil \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & \mbox{where } f::\tau, \ f_{t}::\lceil \tau \rceil \\
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini \lceil let \ x_{1} \ \dots \ x_{n} \ in \ exp \rceil & =
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini & let \ \lceil x_{1} \rceil \ \dots \ \lceil x_{n} \rceil \ in \ \lceil exp \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \lceil TyCons \ a_{1} \ldots a_{n} \rceil & = & \lceil a_{1} \rceil
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \ldots \lceil a_{n} \rceil \ TyCons_{t}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Recursive definitions set HOL and HOLCF apart. In HOL a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidistinction is drawn, and syntactically highlighted, between primitive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions (introduced by keyword \emph{primrec}) and generic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive ones (by keyword \emph{recdef}). Termination is guaranteed
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor each of the formers, by the fact that recursion is based on the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidatatype structure of one of the parameters. In contrast, termination
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis not a trivial matter for the latters. A strictly decreasing measure
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimust be provided, associated to the parameters of the defined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction. This requires a degree of ingenuity that cannot be easily
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidealt with automatically. For this reason, the translation to HOL is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestricted to primitive recursive functions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMutual recursion is allowed for under additional restrictions --- more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprecisely: 1) all the functions involved are recursive in the first
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniargument; 2) recursive arguments are of the same type in each
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction. The translation of mutually recursive functions $a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\rightarrow b, \ldots a \rightarrow d$ introduces a new function $a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\rightarrow (b * \ldots * d)$ recursively defined, for each case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipattern, as the product of the values
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorrespondingly taken by the original, non-recursively defined ones. \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ fun3 \ :: \ AType \ a \ b \to (a \to a) \to AType \ a \ b $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3 \ k \ f & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ a \to ABase \ (f \ a) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ a \ b \to AStep \ (fun4 \ a) \ b \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ fun4 \ :: \ AType \ a \ b \to AType \ a \ b $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun4 \ k & = \ case \ k \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ x \ y \to AStep \ (fun3 \ x \ (\backslash z \to z)) \ y \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ x \to ABase \ x \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent These functions, satisfying the restrictions, will translate
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito the following.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3 \ :: & ('a::type, 'b::type) AType \Rightarrow ('a::type \Rightarrow 'a::type) \Rightarrow \\ & ('a::type, 'b::type) AType \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun4 \ :: & ('a::type, 'b::type) AType \Rightarrow ('a::type \Rightarrow 'a::type) \Rightarrow\\ & ('a::type, 'b::type) AType \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3\_Xfun4\_X :: & ('a::type, 'b::type) AType \Rightarrow \\ & (('aXX1::type \Rightarrow 'aXX1::type) \Rightarrow \\ & ('aXX1::type, 'bXX1::type) AType) * \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (('aXX2::type \Rightarrow 'aXX2::type) \Rightarrow \\ & ('aXX2::type, 'bXX2::type) AType) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3\_def : & fun3 \ == \ \% k \ f. \ fst \ (( fun3\_Xfun4\_X :: \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & \ ('a::type, 'b::type) AType \Rightarrow (('a::type \Rightarrow 'a::type) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini& \Rightarrow ('a::type, 'b::type) AType) * ((unit \Rightarrow unit) \Rightarrow \\ & (unit, unit) AType) ) \ k) \ f \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun4\_def : & fun4 \ == \ \% k \ f. \ snd \ (( fun3\_Xfun4\_X :: \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('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 \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $primrec$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{lll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3\_Xfun4\_X & (ABase \ pX1) \ = & (\% f. \ ABase \ (f \ pX1), \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & \% f. \ ABase \ pX1) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun3\_Xfun4\_X & (AStep \ pX1 \ pX2) & = \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (\% f. \ AStep \ (snd & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2, \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & \% f. \ AStep \ (fst & (fun3\_Xfun4\_X \ pX1) \ f) \ pX2) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Calls of the recursive functions in the non-recursive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions are annotated with type where exceeding type variables are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinstantiated with the unit type, as required by Isabelle in order to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavoid definitions from which inconsistencies are derivable.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Patterns}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:Patterns}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSupport of patterns in definitions and case expressions is more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestricted in Isabelle than in Haskell. Nested patterns are overall
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidisallowed. In case expressions, the case term is required to be a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinivariable. Both of these restrictions apply to our translations. A
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifurther Isabelle limitation concerning case expressions ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisensitiveness to pattern order --- is dealt with automatically.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSimilarly, wildcards --- something unknown to Isabelle --- are dealt
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith, as well as, in HOLCF, incomplete patterns. The exclusion of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininested patterns complicate the translation of some specific ones ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin fact, guarded expressions and list comprehension are not covered;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheir use should be avoided here, using conditional expressions and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{map} instead.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% not allowed in Isabelle with ordinary definitions (keyword
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \emph{Defs}), but it is allowed with the syntax for recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMultiple function definitions using top level pattern matching are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated as definitions based on a single case expression; this is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidue to HOL more than to HOLCF. In fact, multiple definitions in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle are only allowed with the syntax of recursive ones. However,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin HOL primitive recursive definitions, patterns are allowed for only
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin one parameter. In order to translate definitions with more patterns
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias arguments, without resorting to tuples and to more complex syntax
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(\emph{recdef} instead of \emph{primrec}) we translate multiple
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions by top level pattern matching
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias definitions by case construct.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ctl \ :: \ Bool \to Bool \to Bool \to Bool$ \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ False \ a \ False \ = \ a $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ True \ a \ False \ = \ False $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ False \ a \ True = \ True $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctl \ True \ a \ True \ = \ a $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent This translates to HOL as the following.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts \ ctl :: \ bool \Rightarrow bool \Rightarrow bool \Rightarrow bool$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{llll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinictl\_def : & ctl \ == & \% qX1. \% qX2. \% qX3. & case \ qX1 \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & False \Rightarrow case \ qX3 & of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & False \Rightarrow qX2 \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & True \Rightarrow True \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & True \Rightarrow case \ qX3 & of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & False \Rightarrow False \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo 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
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis not a recursive datatype. The following gives an alternative that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinican be handled (a new datatype is used instead of booleans).\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $data \ Two \ = Fx \ | \ Tx $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $ctlx :: \ Two \to Two \to Two \to Two $ \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctlx \ Fx \ a \ Fx \ = \ a $ \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctlx \ Tx \ a \ Fx \ = \ Fx $ \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctlx \ Fx \ a \ Tx \ = \ Tx $ \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ctlx \ Tx \ a \ Tx \ = \ a $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent This translates to HOLCF as follows.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $domain \ Two \ = \ Fx \ | \ Tx $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts \ ctlx :: \ Two \to Two \to Two \to Two$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{llll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinictlx\_def : & map5 \ == & LAM \ qX1 \ qX2 \ qX3. & case \ qX1 \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & Fx \Rightarrow case \ qX3 & of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & Fx \Rightarrow qX2 \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & Tx \Rightarrow Tx \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & Tx \Rightarrow case \ qX3 & of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & Fx \Rightarrow Fx \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & & & Tx \Rightarrow qX2 \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent In case expressions as well as in top level pattern matching
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions, wildcards may be used --- though not in nested position.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIncomplete patterns are translated to HOLCF using $\bot$ as default
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Classes}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell defined classes are translated to Isabelle as classes with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniempty axiomatization. Isabelle allows classes with no more than one
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype parameter, therefore our translations can support only them ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniit might be possible to handle more than one parameter using tuples,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibut this would surely involve considerable complications dealing with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconditional instances.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniInstance declarations are translated to corresponding ones in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle. Isabelle instances in general require proofs that class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxioms are satisfied by the types, but as long as there are no axioms
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe proofs are trivial and can be handled automatically. Function
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations associated with Haskell classes are translated as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniindependent function declarations with appropriate class annotation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFunction definitions associated with instance declarations are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated as overloaded function definitions,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirelying on class annotation of the typed variables.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $class ClassA \ a \ where$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$abase :: \ a \to Bool $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$ astep :: \ a \to Bool $\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $instance \ (ClassA \ a, \ ClassA \ b) \Rightarrow ClassA \ (AType \ a \ b) \ where $
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabase \ x \ = & case \ x \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ u \ \to \ True \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & \_ \ \to \ False \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent This code translates to HOLCF as follows.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $axclass \ ClassA < pcpo$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $instance \ AType::({pcpo, ClassA}, {pcpo, ClassA}) \ ClassA$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$by \ intro\_classes$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabase :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniastep :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_abase :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_astep :: & 'a::\{ClassA, pcpo\} \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAType\_abase\_def : & \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini abase :: & ('a::\{ClassA, pcpo\}, 'b::\{ClassA, pcpo\}) \ AType \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini == & LAM x. \ case \ x \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \cdot pX1 \Rightarrow TT \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \cdot pX2 \cdot pX1 \Rightarrow FF \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAType\_astep\_def : & \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini astep :: & ('a::\{ClassA, pcpo\}, 'b::\{ClassA, pcpo\}) \ AType \to tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & == default\_astep \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent Similarly, it translates to HOL.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $axclass \ ClassA < type$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $instance \ AType::(\{type, ClassA\}, \{type, ClassA\}) \ ClassA$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$by \ intro\_classes$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniastep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_abase :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefault\_astep :: & 'a::\{ClassA, type\} \Rightarrow bool\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{rl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAType\_abase\_def : & \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini abase :: & ('a::\{ClassA, type\}, 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini == & \% x. \ case \ x \ of \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ABase \ pX1 \Rightarrow True \ | \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & AStep \ pX2 \ pX1 \Rightarrow False \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAType\_astep\_def : & \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini astep :: & ('a::\{ClassA, type\}, 'b::\{ClassA, type\}) \ AType \Rightarrow bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini == & default\_astep\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Equality}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAt the moment equality is the only covered built-in class. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatizations provided, respectively, in \emph{HsHOLCF} and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{HsHOL} are based on the abstract definition of the equality and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinequality functions \cite{HaskellRep}. In both theories, \emph{Eq} is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclared as a subclass of \emph{type} --- in \emph{HsHOLCF} this is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidone in order to instantiate it with lifted types.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorrinihEq :: & ('a::Eq) lift \ \to \ 'a \ lift \ \to \ tr \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorrinihNEq :: & ('a::Eq) lift \ \to \ 'a \ lift \ \to \ tr\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $axioms$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniaxEq: & ALL x. (hEq \cdot p \cdot q \ = \ Def x) \ = \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (hNEq \cdot p \cdot q \ = \ Def (\sim x)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent The instantiation of equality (consequently, of inequality) for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniboolean (and similarly for integer) is obtained by lifting HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniequality so that $\bot$ is returned whenever one of the argument is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $tr\_hEq\_def: \ hEq \ == \ fliftbin \ (\% (a::bool) \ b. \ a \ = \ b)$\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%ax1: & hEq \cdot p \cdot p \ == \ Def \ true \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%ax2: & [| \ hEq \cdot q \cdot r \ = \ Def \ true; \ hEq \cdot p \cdot q \ = \ Def \ true \ |] \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% & ==> \ hEq \cdot p \cdot r \ = \ Def \ true \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent In \emph{HsHOL} the axiomatization reflects the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestriction to terminating programs.\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorrinihEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorrinihNEq :: & ('a::Eq) \ \Rightarrow \ 'a \ \Rightarrow \ bool \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $axioms$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$\begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini axEq: & hEq \ p \ q \ == \ \sim hNEq \ p \ q \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent The instantiation of \emph{hEq} for boolean and integer is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimply taken to be HOL equality.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% ax1: & hEq \ p \ p \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% ax2: & [| \ hEq \ q \ r; \ hEq \ p \ q \ |] ==> hEq \ p \ r \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Monads}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:Monads}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle does not allow for classes of type constructors, hence a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproblem in representing monads. We could deal with this problem
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirelying on an axiomatization of monads that allows for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirepresentation of monadic types as an axiomatic class, as presented in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Lueth}. Monadic types should be translated to newly defined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes that satisfy monadic axioms. This would involve defining a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory morphism, as an instantiation of type variables in the theory
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof monads. We are planning to rely on AWE \cite{AWE}, an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimplementation of theory morphism on top of Isabelle base logic that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimay be used to extend HOL as well.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Conclusion}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following is a list of features that are covered by our
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{itemize}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined types: boolean, integer.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined type constructors: function, cartesian product, list.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item declaration of recursive datatype, including mutually recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined functions: equality, booelan constructors,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini connectives, list constructors, head and tail list functions,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini arithmetic operators.
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini\item non-recursive functions, including conditional, \emph{case} and
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini \emph{let} and expressions (with restriction related to use of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item use of incomplete patterns (in HOLCF) and of wildcards in case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item total primitive recursive functions (in HOL)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand partial recursive ones (in HOLCF), including mutual ones (with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestrictions in the HOL case).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item single-parameter class and instance declarations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \item monad declarations and do notation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe shallow embedding approach makes it possible to take the most out
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the automation currently available on Isabelle, especially in HOL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFurther work should include extending the translation to cover the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhole of the Haskell Prelude. We would also be interested in carrying
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniout an extension to cover P-logic \cite{KiebPl}, a specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformalism for Haskell programs included in the Programatica toolset.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%This translation, due to the character of the P-logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%typing system, could be more easily carried out relying on some form
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%of universal quantification on type variables, or else further relying
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%on parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliographystyle{alpha}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliography{case}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{document}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn our example,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation gives the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $consts$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun1 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('a::type, 'b::type) \ Prelude\_AType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_AType \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun1\_Xfun2\_X & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (('bXX1::type \Rightarrow 'dXX1::type) \ \Rightarrow \\ & ('aXX1::type, 'bXX1::type) \ Prelude\_AType \ \Rightarrow \\ & ('cXX1::type, 'dXX1::type) \ Prelude\_AType) * \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (('bXX2::type \Rightarrow 'dXX2::type) \ \Rightarrow \\ & ('aXX2::type, 'bXX2::type) \ Prelude\_BType \ \Rightarrow \\ & ('cXX2::type, 'dXX2::type) \ Prelude\_BType) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun2 & :: \ ('a::type \Rightarrow 'c::type) \ \Rightarrow \ ('b::type \Rightarrow 'd::type) \ \Rightarrow \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & ('a::type, 'b::type) \ Prelude\_BType \ \Rightarrow \\ & ('c::type, 'd::type) \ Prelude\_BType \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $defs$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun1\_def : & fun1 \ == \ \% f. \% g. \% k. \ fst (fun1\_Xfun2\_X \ f) \ g \ k \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifun2\_def : & fun2 \ == \ \% f. \% g. \% k. \ snd (fun1\_Xfun2\_X \ f) \ g \ k
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\noindent $primrec$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$$ \begin{array}{ll}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (ABase \ pX1) & = \ (\% g. \% k. \ ABase \ (f \ pX1)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (BBase \ pX1) & = \ (\% g. \% k. \ BBase \ (g \ pX1)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (AStep \ pX1 \ pX2) & = \ (\% g. \% k. \ AStep \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini fun1\_Xfun2\_X \ (BStep \ pX1 \ pX2) & = \ (\% g. \% k. \ BStep \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (snd \ (fun1\_Xfun2\_X \ f) \ g \ pX1) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini & (fst \ (fun1\_Xfun2\_X \ f) \ g \ pX2)) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Equality: HOLCF}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Equality: HOL}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell classes and instances are translated to Isabelle,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirespectively, as classes with empty axiomatisation and as instances
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith trivial instantiation proof. The translation supports only
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisingle-parameter classes --- in principle, more than one parameter
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicould be handled using tuples.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever here is not provided !!!
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFunctions declarations associated to classes are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle as independent function declarations with appropriate class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation. Function definitions associated to instances are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated as overloaded function definitions, relying on class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation of typed variables.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% ...xxx...!!! check out for stuff to include in Classes ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNon-recursive definitions are translated to ordinary definitions (keyword
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{defs}), whereas recursive ones require specific keywords. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype of the function, inclusive of class annotation, is included in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinievery definitions in order to allow for overloading.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%For values of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%built-in type, the lifting function is \emph{Def}; the undefined case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%collapses on $\bot$.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn HOLCF, where every type is a domain and every function is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicontinuous, all recursive functions can be defined by fixpoint
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperator. This is essentially a function that, given as argument the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction definition body abstracted of the recursive call name,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireturns the corresponding recursive function. Coding this directly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwould be rather cumbersome, particularly in the case of mutually
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions, where tuples of definition bodies and tupled
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniabstraction are needed. We can instead rely on the \emph{recdef}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipackage, which allows to handle fixpoint definitions like ordinary
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive ones, offering nice syntax to deal with mutual recursion as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Type signature}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe present translation to HOL is very basic, and does take into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaccount neither partiality nor laziness. Essentially, it left to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell programmer to check that all the functions are total ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAn account of partiality -- although possibly not aof laziness ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicould be obtained using the option type constructor to lift types,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialong a similar line to lift. Here however we are presenting just a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniplain version, mapping Haskell types in the corresponding unlifted HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. All variables belong to the class type. Recursive and mutually
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive data-types declarations are translated to HOL datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{HOL: Function definitions}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNon-recursive definitions and let expressions are treated similarly as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin the translation to HOLCF. Recursive defitions is the topic that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireally sets HOL and HOLCF apart. In HOL a distinction has to be drawn
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibetween primitive recursive functions and generic recursive ones. In
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe former, termination is guaranteed by the fact that recursive
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions are strictly associated with the datatype structure of a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniparameter. In the latter, termination needs to be proved. This must be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidone, in a \emph{recdef} definition, by providing a measure for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction parameter that can be proved to be strictly decreasing for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieach occurrence of a recursive call in the definition. This requires a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidegree of ingenuity that cannot be generally associated with an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniautomated translation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFor this reason, the translation of recursive functions to HOL is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestricted to primitive recursive ones. Mutually recursive functions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare allowed under additional restrictions. These are: all the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions should be recursive in the first argument; this should be of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe same type for each of them; the constructors should be listed in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe same order in each of the case expressions; the variable names in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe case patterns are expected to be maintained.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation of mutually recursive functions $a \rightarrow b, \ldots a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefined, for each case pattern, as the product of the values
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorrespondingly taken by the original functions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Pattern matching}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSupport of pattern-matching in Isabelle is more restricted than in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. Nested patterns are disallowed; case expressions are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisensitive to the order of the constructors, which should be the same
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias in the datatype declaration. In particular, the case variable si
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequired to be a variable. Translation of pattern-matching is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipotentially laborious. For this reason guarded expressions, list
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomprehension and nested pattern-matching have been left out; they
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishould be replaced by the programmer, using conditional expressions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand map functions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFunction definition by top level pattern matching is not allowed in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle with ordinary definitions, but it is with those that are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexplicitly declared to be recursive ones. However, particularly in HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprimitive recursive definitions patterns are allowed in one parameter
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinionly. In order to translate function definitions with patterns in more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithan one parameter, without resorting to using tuples and more complex
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions (\emph{recdef} instead of \emph{primrec}), our
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslations turn a multiple definition by top level pattern matching
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto a definition by case construct.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Classes}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell classes and instances are translated to Isabelle,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirespectively, as classes with empty axiomatisation and as instances
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith trivial instantiation proof. The translation supports only
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisingle-parameter classes --- in principle, more than one parameter
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicould be handled using tuples.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever here is not provided !!!
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFunctions declarations associated to classes are translated to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle as independent function declarations with appropriate class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation. Function definitions associated to instances are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated as overloaded function definitions, relying on class
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniannotation of typed variables.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section*{Haskell2Isabelle}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe tool is designed to support the translation of simple but
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirealistic Haskell programs to HOLCF and, with some restriction, to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL. Not all the syntactical features of Haskell are covered yet,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialthough most of those used in the Prelude are. The most noticeable
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilimitations are related to built-in types, pattern-matching and local
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidefinitions. There are additional and more substantial restrictions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin the case of HOL, related to termination and to recursion.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe application can be installed as part of Hets. It requires Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniGHC and Programatica. It is run by the command \emph{hets -t ...
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini [h|hc] file.hs} where the options stand for HOL and HOLCF,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFor the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimodule that contains the main translation function, carried out as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomposition of a signature morphism and a theory morphism.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{IsaSign.hs} contains the Hets representation of the Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibase logic and extensions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe general design of the translation functions, and particularly the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitwo-layered recursion adopted for them, is similar to that used for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe translation Haskell to Agda in Programatica.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Monads}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle does not allow for classes of type constructors, hence a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproblem in representing monads. We can deal with this problem,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever, relying on an axiomatisation of monads that allows for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipresentation of monadic types as an axiomatic class, as provided in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{}. Therefore, monadic types can be translated to newly defined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes that are constrained to satisfy the monadic axioms. This
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstraining, carried out as an instantiation of type variables in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory of monads, takes the form of a theory morphism, and can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicarried out automatically by AWE, an implementation of parametrisation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand theory morphism on top of Isabelle basic logic, that may also be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniused to extend HOL and HOLCF. The do notation can then be translated
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby unpacking it into monadic operators. Attempting to translate
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonadic notation without support AWE support will result in an error
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section*{Conclusion}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following is a list of constructs that are covered by all the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{itemize}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined types: boolean, integer.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predifed type constructors: funtion, cartesian product, list.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item declaration of recursive datatype, including mutually recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item predefined functions: equality, booelan constructors,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini connectives, list constructors, head and tail list functions,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini arithmetic operations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item non-recursive functions, including conditional,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilet and case expressions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item use of incomplete patterns (HOLCF) and of wildcards in case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item total primitive recursive functions (HOL)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand partial recursive ones (HOLCF), including mutual ones (with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirestrictions in the HOL case).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item class and instance declarations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item monad declarations and do notation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe shallow embedding approach used by our translations should allow
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito take as much advantage as possible of the automation currently
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavailable on Isabelle, particularly in HOL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFurther work should include extending the translation to cover the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhole of the Haskell Prelude. We hope that this will make it possible
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito support the verification of functional robotics programs.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA further extension, in line with the work on Programtica, would be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe translation of P-logic. This translation, due to the character of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe P-logic typing system, could be more easily carried out relying on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisome form of universal quantification on type variables, or else
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifurther relying on parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliographystyle{alpha}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\bibliography{case}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{document}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation of types is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOur general strategy for translating signatures is to map Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes to Isabelle defined types.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini the fact that Haskell expressions are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinievaluated lazily, however it does not preserve The translation to HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidoes not, and moreover requires that all the functions defined in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell program are total ones...
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll types have a sort in Isabelle, defined by the set of the classes
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof which it is a member. In HOL, all types belong to the class type;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin HOLCF, they belong to class pcpo (pointed complete poset).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll Haskell function declarations are translated to Isabelle ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniType variables are assigned default sort type in HOL and pcpo in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF. Names get translated by a function that preserves them, up to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavoidance of clashes with Isabelle keywords.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe only built-in types that are properly covered are booleans,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniunbounded integers and rationals. These get translated, in the case of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL, to Isabelle booleans, integers and rationals, respectively. Bound
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintegers and floating point numbers would require low-level modelling,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand have not been dealt with; anyway, bounded integers are accepted
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand simply treated as unbounded by the application.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the HOLCF translation, all built-in types get lifted to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorresponding domains (pcpos), which by definion include the undefined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinivalue, by using the lift HOLCF type constructor. In particular, type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniboolean get translated to type tr (short for bool lift), and similarly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor types integer and rational.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRecursive data-types declarations can be translated to datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations in HOL. In HOLCF they can be translated to domain
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations. The two structure are quite similar, except that in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidomains, which are pcpo, all the parameters are required to be pcpos
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well. Morevover, Isabelle domain declarations require to introduce
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininames for destructors. Mutually recursive Haskell datatypes can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated to both logics, relying on the specific Isabelle syntax for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA type class in Isabelle is conceptually quite different from one in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. The former is associated to a set of axioms, whereas the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilatter is associated to a set of function declarations. Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininot allow for type constructor classes. The last limitation is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimost serious of the three, since it makes quite hard to cope with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonads. We can get around this obstacle relying on a method for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \emph{lift} type constructor, in particular, lifts each HOL type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito a flat domain, by adding a bottom element to them. We are going to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniuse it to lift the basic types. For the product we are going to use
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininon-strict product.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformalisation on Isabele relies on axiomatic type classes \cite{},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith \emph{pcpo} (pointed complete partial order) as the default
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclass, in which the type of continuous functions can be represented as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunction spaces, allowing for an elegant interpretation of recursion
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby fixpoint operator. HOL types may be lifted to \emph{pcpo} by simply
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniadding a bottom element to them. This is what the type constructor
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{lift} does, thus providing also a way of handling partiality ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniundefined cases can be mapped to the bottom element. HOLCF has also a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype constructor \emph{u} that allows to deal with laziness, by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniguaranteeing $\bot \neq \smath{up} \$ (\bot)$.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the case of HOLCF, the logic provides a computational
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinterpretation of function types as domains. In HOL there is no such
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifacility, therefore either appropriate types for the translation are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintroduced --- as in \cite{}, or considerable semantical restrictions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimust be accepted --- this is also the case for one of the translation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito FOL proposed in \cite{}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDepending on the expressiveness of the logic, the translation of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprogramming language may be carried out at different levels of depth.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn general, the deeper is the embedding, the less it relies on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimeta-level features of the target language. This may be a plus, either
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifrom the point of view of semantic clarity, or from that of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressiveness. Taking advantage of meta-level feaures, on the other
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihand, may be useful in order to make the theorem proving less tedious,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby allowing more constant use of generic proof methods. It may also
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniultimately affect positively the theorem prover economy, by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireinforcing the bias toward the development of proof methods that,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever specific, can be more easily integrated with generic ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% a point made in \cite{}. for example by allowing a straightforward
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% operational interpretation ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations of Haskell to HOLCF and HOL that we are presenting in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe following justify themselves in terms of denotational semantics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOLCF differs from that proposed in \cite{} in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitreatment of types. We translate Haskell types directly into HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniones, whereas they use HOLCF terms to embed Haskell types. We assume
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat the HOLCF types are similar enough to the those of Haskell, in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniorder to guarantee the semantical correctness of our translations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMoreover, we rely on axiomatic classes to translate Haskell types
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOur approach has the advantage of giving a shallower embedding,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihowever it has the drawback of not bein complete --- notably, type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructor classes are missing. We plan to handle in future this
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproblem (see section~\ref{sec:Monads}) by relying on an extension of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle based on morphism between theories. The translation into HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis essentialy only a first experiment, it handles types very
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimplistically, relying on drastic semantical restrictions for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorrecteness. Under those restrictions, however, it gives expressions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat are comparatively quite simple to work with.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA type class in Isabelle is conceptually quite different from one in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. The former is associated to a set of axioms, whereas the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilatter is associated to a set of function declarations. Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininot allow for type constructor classes. The last limitation is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimost serious of the three, since it makes quite hard to cope with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonads. We can get around this obstacle relying on a method for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Types}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF allows has types for computable functions --- defined as sets of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicontinuous functions of a type (!! fixpoints!!). It has a type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstructor \emph{lift} that lifts HOL types to \emph{pcpo}s, thus
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproviding a way of handling partiality --- undefined cases can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimapped to the bottom element. It has also a type constructor \emph{u}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat allows to deal with laziness, by guaranteeing $\bot \neq
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\smath{u}(\bot)$.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat can be used to embed Haskell function types.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOLCF differs from that to HOL insofar as only the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifirst one relies on a denotational semantics for the full language,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinikeeping into account partiality and lazy evaluation, and associating
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions to corresponding fixed points, using on the Fixrec
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniextension of HOLCF. The translation to HOL is more restrictive; it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidoes not keep into account any form of partiality, and it restricts
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation of recursive functions to the primitive recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIt would have been possible to give an account of partiality in HOL by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniusing option types. However, we chose to keep the HOL translation as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimple as possible for didactic purpose.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{maybe}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations of Haskell that we are presenting in the following,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe present translations of Haskell into some of the Isabelle logics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThese translations are implemented as part of Hets, and are based on a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishallow embedding approach quite different from that used in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProgramatica. In our translations Haskell types are mapped to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. We are assuming that the type systems of HOL and HOLCF are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimilar enough to the type system of Haskell, in order to guarantee
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe semantical correctness of our translations. Moreover, we rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic classes to translate Haskell types classes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA type class in Isabelle is conceptually quite different from one in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell. The former is associated to a set of axioms, whereas the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilatter is associated to a set of function declarations. Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininot allow for type constructor classes. The last limitation is the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimost serious of the three, since it makes quite hard to cope with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimonads. We can get around this obstacle relying on a method for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translation to HOLCF differs from that to HOL insofar as only the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifirst one relies on a denotational semantics for the full language,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinikeeping into account partiality and lazy evaluation, and associating
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirecursive functions to corresponding fixed points, using on the Fixrec
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniextension of HOLCF. The translation to HOL is more restrictive; it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidoes not keep into account any form of partiality, and it restricts
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation of recursive functions to the primitive recursive ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIt would have been possible to give an account of partiality in HOL by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniusing option types. However, we chose to keep the HOL translation as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimple as possible for didactic purpose.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Type signature}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOur general strategy for translating signatures is to map Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes to Isabelle defined types. The translation to HOLCF keeps into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaccount the fact that Haskell expressions are evaluated lazily. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation to HOL does not, and moreover requires that all the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctions defined in the Haskell program are total ones...
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll types have a sort in Isabelle, defined by the set of the classes
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof which it is a member. In HOL, all types belong to the class type;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin HOLCF, they belong to class pcpo (pointed complete poset).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll Haskell function declarations are translated to Isabelle ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniType variables are assigned default sort type in HOL and pcpo in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOLCF. Names get translated by a function that preserves them, up to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavoidance of clashes with Isabelle keywords.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe only built-in types that are properly covered are booleans,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniunbounded integers and rationals. These get translated, in the case of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHOL, to Isabelle booleans, integers and rationals, respectively. Bound
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintegers and floating point numbers would require low-level modelling,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand have not been dealt with; anyway, bounded integers are accepted
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand simply treated as unbounded by the application.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the HOLCF translation, all built-in types get lifted to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicorresponding domains (pcpos), which by definion include the undefined
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinivalue, by using the lift HOLCF type constructor. In particular, type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniboolean get translated to type tr (short for bool lift), and similarly
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor types integer and rational.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRecursive data-types declarations can be translated to datatype
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations in HOL. In HOLCF they can be translated to domain
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations. The two structure are quite similar, except that in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidomains, which are pcpo, all the parameters are required to be pcpos
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well. Morevover, Isabelle domain declarations require to introduce
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininames for destructors. Mutually recursive Haskell datatypes can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslated to both logics, relying on the specific Isabelle syntax for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe present translations of Haskell into some of the Isabelle logics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThese translations are implemented as part of Hets, and are based on a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishallow embedding approach quite different from that used in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProgramatica. In our translations Haskell types are mapped to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. We are assuming that the type systems of HOL and HOLCF are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimilar enough to the type system of Haskell, in order to guarantee
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe semantical correctness of our translations. Moreover, we rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic classes to translate Haskell types classes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the following, we present translations of Haskell into some of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle logics. These translations are implemented as part of Hets,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand are based on a shallow embedding approach quite different from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat used in Programatica. In our translations Haskell types are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimapped to Isabelle types. We are assuming that the type systems of HOL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand HOLCF are similar enough to the type system of Haskell, in order
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito guarantee the semantical correctness of our translations. Moreover,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe rely on axiomatic classes to translate Haskell types classes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini are those presented in \cite{}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias well as in \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation of Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto FOL \cite{} and that into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn \cite{} Haskell is embedded in Martin-Loef
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype theory, implemented on Agda.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini is indeed a general difference between a lower level
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniapproach based on operational semantics, followed in \cite{agda} and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{miranda}, and a higher-level one, based essentially on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotational semantics, followed in \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe correctness of such embeddings
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialways rests, ultimately, on the denotational semantics of Haskell,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand on the possibility to encode it in a logic under consideration.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Thompson95}. Indeed, Haskell --- a strongly typed, purely
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifunctional language with lazy evaluation, based on a system of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipolymorphic types extended with type constructor classes, where monads
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniallow for side effects and pseudo-imperative code \cite{Hudak} --- has
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialready been considered several times as a target for verification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll the above-mentioned works provide embeddings of Haskell, either
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipartial or total, into programming logic implemented on theorem
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprovers. The correctness of such embeddings always rests, ultimately,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinion the denotational semantics of Haskell, and on the possibility to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniencode it in a logic under consideration.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe tools, the logic and the ways in which the encoding can be done
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimay differ quite deeply. In \cite{} Haskell is embedded in Martin-Loef
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitype theory, implemented on Agda. All the other examples rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle, a generic theorem-prover written in SML that allows for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformalisation of a variety of logics, including FOL, HOL and HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Paulson94isa}. The embedding in \cite{} rely on FOL, the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle implementation of classical first-order logic.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll the other examples \cite{...} rely on higher-order logic. HOL is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe implementation of classical higher-order logic based on simply
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinityped lambda calculus, extended with axiomatic type classes. HOLCF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{holcf} is the extension of HOL with a formalisation of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory of computable functions (LCF) based on axiomatic type classes.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% other words, we need to represent the program in a mechanised logic in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% which the requirements can be expressed, as well.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% The representation can take different forms. It is possible to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% associate the state-machine behavioural description to models in a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% logic. Another possibility is to represent the program in terms of a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% computational logic based on the operational semantics of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% In both cases however, a significant part of the work has to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini% be carried out before the actual verification may take place.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn order to verify a program, we need to associate its code to a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilogical representation that allows for requirements to be expressed
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand for proofs to be carried out. There are different ways to do this.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe way we carry this out here is to embed Haskell into an expressive
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinihigher-order logic, together with providing an implementation of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniembedding that allows for an automated translation of Haskell. From
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe theoretical point of view, the correctness of the embdedding
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidepends on the denotational semantics of the language. From the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipractical point of view, once the program code can be translated
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniautomatically to the logic, all the burden of the verification can
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirest on the theorem proving.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniDepending on the expressiveness of the logic, the translation of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprogrmaming language may be carried out at different levels of depth.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn general, the deeper is the embedding, the less it relies on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimeta-level features of the target language. This may be a plus from
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe point of view of semantic clarity. Taking advantage of meta-level
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifeaures, on the other hand, may be useful in order to make the theorem
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniproving less tedious.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle is a generic theorem-prover written in SML that allows for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe formalisation of a variety of logics \cite{Paulson94isa}.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle-HOL is the implementation of classical higher-order logic
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibased on simply typed lambda calculus, extended with axiomatic type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclasses. Isabelle-HOLCF \cite{holcf} is the extension of HOL with a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniformalisation of the theory of computable functions (LCF) based on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaxiomatic type classes.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHets \cite{Hets} is a parsing, static analysis and proof management
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitool designed to interface with various language specific tools, in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniorder to support heterogeneous specification. In particular, for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniparsing and static analysis of Haskell programs Hets relies on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniProgramatica \cite{PTeam}, a tool that has its own proof management,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniincluding a translation of Haskell to Isabelle-HOLCF.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe translations of Haskell that we are presenting in the following,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwe present translations of Haskell into some of the Isabelle logics.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThese translations are implemented as part of Hets, and are based on a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishallow embedding approach quite different from that used in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProgramatica. In our translations Haskell types are mapped to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes. We are assuming that the type systems of HOL and HOLCF are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimilar enough to the type system of Haskell, in order to guarantee
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe semantical correctness of our translations. Moreover, we rely on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic classes to translate Haskell types classes.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniA type class in Isabelle is conceptually quite different from one in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell. The former is associated to a set of axioms, whereas the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilatter is associated to a set of function declarations. Isabelle
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniclasses may have at most a type parameter. Moreover, Isabelle does
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininot allow for type constructor classes. The last limitation is the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimost serious of the three, since it makes quite hard to cope with
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimonads. We can get around this obstacle relying on a method for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniParametrisation based on theory morphism has been implemented, as a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidesigned to support proof reuse \cite{AWE}.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe translation to HOLCF differs from that to HOL insofar as only the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifirst one relies on a denotational semantics for the full language,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinikeeping into account partiality and lazy evaluation, and associating
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirecursive functions to corresponding fixed points, using on the Fixrec
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniextension of HOLCF. The translation to HOL is more restrictive; it
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidoes not keep into account any form of partiality, and it restricts
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslation of recursive functions to the primitive recursive ones.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIt would have been possible to give an account of partiality in HOL by
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniusing option types. However, we chose to keep the HOL translation as
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisimple as possible for didactic purpose.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThese translations are on the overall quite different from other ones
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibased on deep embeddings, particularly from the Programatica
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslation of Haskell into HOLCF \cite{Huff}, where the type system
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniis modelled at the logical level, as well as from translations of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniMiranda and Haskell into FOL (Isabelle classical first-order logic)
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwhere higher-order features have to be dealt with less directly
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\cite{Thompson95,Thompson92}.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\section*{The hs2thy tool}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini(suggested change: from h2hf to hs2thy)
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe tool is designed to support the translation of simple but
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirealistic Haskell programs to HOLCF and, with some restriction, to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOL. Not all the syntactical features of Haskell are covered yet,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinialthough most of those used in the Prelude are. The most noticeable
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilimitations are related to built-in types, pattern-matching and local
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefinitions. There are additional and more substantial restrictions
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniin the case of HOL, related to termination and to recursion.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe application can be installed as part of Hets. It requires Haskell
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniGHC and Programatica. It is run by the command \emph{h2hf
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini [h|hc|mh|mhc] file.hs} where the options stand, respectively, for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOL, HOLCF, HOL extended with AWE and HOLCF extended with AWE.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFor the sake of maintainance, \emph{Haskell2IsabelleHOLCF.hs} is the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimodule that contains the main translation function, carried out as
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitheory translation after a preliminary step of signature translation,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand \emph{IsaSign.hs} contains the internal representation of Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Type signature}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniOur general strategy for translating signatures is to map Haskell
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitypes to Isabelle defined types. The translation to HOLCF keeps into
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaccount the fact that Haskell expressions are evaluated lazily. The
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslation to HOL does not, and moreover requires that all the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunctions defined in the Haskell program are total ones...
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniAll types have a sort in Isabelle, defined by the set of the classes
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniof which it is a member. In HOL, all types belong to the class type;
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniin HOLCF, they belong to class pcpo (pointed complete poset).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniAll Haskell function declarations are translated to Isabelle ones.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniType variables are assigned default sort type in HOL and pcpo in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOLCF. Names get translated by a function that preserves them, up to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniavoidance of clashes with Isabelle keywords.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe only built-in types that are properly covered are booleans,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniunbounded integers and rationals. These get translated, in the case of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHOL, to Isabelle booleans, integers and rationals, respectively. Bound
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniintegers and floating point numbers would require low-level modelling,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand have not been dealt with; anyway, bounded integers are accepted
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand simply treated as unbounded by the application.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn the HOLCF translation, all built-in types get lifted to the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicorresponding domains (pcpos), which by definion include the undefined
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinivalue, by using the lift HOLCF type constructor. In particular, type
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniboolean get translated to type tr (short for bool lift), and similarly
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifor types integer and rational.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniRecursive data-types declarations can be translated to datatype
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclarations in HOL. In HOLCF they can be translated to domain
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclarations. The two structure are quite similar, except that in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidomains, which are pcpo, all the parameters are required to be pcpos
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinias well. Morevover, Isabelle domain declarations require to introduce
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininames for destructors. Mutually recursive Haskell datatypes can be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslated to both logics, relying on the specific Isabelle syntax for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Function definitions}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell function definitions are translated to corresponding Isabelle
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniones. Non-recursive definitions are translated to ordinary definitions
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini(keyword \emph{defs}), whereas recursive ones require specific
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinikeywords. The type of the function, inclusive of class annotation, is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniincluded in each of its definitions in order to allow for overloading.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn the translation to HOLCF, when the Haskell value is of built-in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitype, the translated value has the lifted corresponding type --- this
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniis either the case of a lifted value (where \emph{Def} is the lifting
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunction) or the case of the undefined value (\emph{UU}).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniAs to local definitions, they can be introduced in Haskell by let and
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwhere expressions. Let expressions are translated to Isabelle let
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniexpressions, whereas where expressions are not covered.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Recursive definitions}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniRecursive defitions is the topic that really sets HOL and HOLCF apart.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn HOLCF, where every type is a domain and every function is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicontinuous, all recursive functions can be defined by fixpoint
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinioperator. This is essentially a function that, given as argument the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunction definition body abstracted of the recursive call name,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinireturns the corresponding recursive function. Coding this directly
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwould be rather cumbersome, particularly in the case of mutually
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirecursive functions, where tuples of definition bodies and tupled
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniabstraction are needed. We can instead rely on the \emph{recdef}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipackage, which allows to handle fixpoint definitions like ordinary
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirecursive ones, offering nice syntax to deal with mutual recursion as
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe case of HOL is more compplex. There a distinction must be drawn
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibetween primitive recursive functions and generic recursive ones. In
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe formers, termination is guaranteed by the fact that recursive
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefinitions are strictly associated with the datatype structure of a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniparameter. In the latters, termination needs to be proved. This can be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidone, in a \emph{recdef} definition, by providing a measure for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunction parameter that can be proved to be strictly decreasing for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinieach occurrence of a recursive call in the definition. This requires a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinigenerally unbounded amount of ingenuity and cannot be carried out by a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisimple translation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFor this reason, the translation of recursive functions to HOL is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestricted to primitive recursive ones. Mutually recursive functions
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniare allowed under additional restrictions. These are: all the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunctions should be recursive in the first argument, this should be of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe same type for each of them, the constructors should be listed in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe same order in each of the case expressions, and also the variable
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininames in the case patterns are expected to be maintained.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe translation of mutually recursive functions $a \rightarrow b, \ldots a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefined, for each case pattern, as the product of the values
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicorrespondingly taken by the original functions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Pattern matching}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniSupport of pattern-matching in Isabelle is more restricted than in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell. Nested patterns are disallowed; case expressions are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisensitive to the order of the constructors, which should be the same
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinias in the datatype declaration. In particular, the case variable si
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirequired to be a variable. Translation of pattern-matching is
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipotentially laborious. For this reason guarded expressions, list
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicomprehension and nested pattern-matching have been left out; they can
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibe replaced without loss, anyway, using conditional expressions and
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimap functions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFunction definition by top level pattern matching is not allowed in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle with ordinary definitions, but it is with those that are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniexplicitly declared to be recursive ones. However, particularly in HOL
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprimitive recursive definitions patterns are allowed in one parameter
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinionly. In order to translate function definitions with patterns in more
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithan one parameter, without resorting to using tuples and more complex
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefinitions (\emph{recdef} instead of \emph{primrec}), our
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslations turn a multiple definition by top level pattern matching
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniinto a definition by case construct.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Classes}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHaskell classes and instances are translated to Isabelle,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirespectively, as classes with empty axiomatisation and as instances
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwith trivial instantiation proof. The translation supports only
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisingle-parameter classes --- in principle, more than one parameter
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicould be handled using tuples.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniBuilt-in classes --- Eq and Ord in particular --- are translated to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininewly defined classes in Isabelle; the corresponding axiomatisation
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinihowever here is not provided.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFunctions declarations associated to classes are translated to
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle as independent function declarations with appropriate class
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniannotation. Function definitions associated to instances are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslated as overloaded function definitions, relying on class
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniannotation of typed variables.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Monads}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:Monads}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle does not allow for classes of type constructors, hence a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniproblem in representing monads. We can deal with this problem,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinihowever, relying on an axiomatisation of monads that allows for the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipresentation of monadic types as an axiomatic class, as provided in
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\cite{}. Therefore, monadic types can be translated to newly defined
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitypes that are constrained to satisfy the monadic axioms. This
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniconstraining, carried out as an instantiation of type variables in the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitheory of monads, takes the form of a theory morphism, and can be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicarried out automatically by AWE, an implementation of parametrisation
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand theory morphism on top of Isabelle basic logic, that may also be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniused to extend HOL and HOLCF. The do notation can then be translated
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniby unpacking it into monadic operators. Attempting to translate
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimonadic notation without support AWE support will result in an error
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\section*{Conclusion}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe following is a list of constructs that are covered by all the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\begin{itemize}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item predefined types: boolean, integer.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item predifed type constructors: funtion, cartesian product, list.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item declaration of recursive datatype, including mutually recursive ones.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item predefined functions: equality, booelan constructors,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini connectives, list constructors, head and tail list functions,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini arithmetic operations.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item non-recursive functions, including conditional,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinilet and case expressions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item use of incomplete patterns (HOLCF) and of wildcards in case
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item total primitive recursive functions (HOL)
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniand partial recursive ones (HOLCF), including mutual ones (with
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestrictions in the HOL case).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item class and instance declarations.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\item monad declarations and do notation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe shallow embedding approach used by our translations should allow
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinito take as much advantage as possible of the automation currently
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniavailable on Isabelle, particularly in HOL.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniFurther work should include extending the translation to cover the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniwhole of the Haskell Prelude. We hope that this will make it possible
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinito support the verification of functional robotics programs.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniA further extension, in line with the work on Programtica, would be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe translation of P-logic. This translation, due to the character of
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe P-logic typing system, could be more easily carried out relying on
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisome form of universal quantification on type variables, or else
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifurther relying on parametrisation.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\bibliographystyle{alpha}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\bibliography{case}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\end{document}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Moreover, being such languages
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%as Haskell, ML and Miranda closely modelled on typed lambda-calculus,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%their translations to specification formalisms, particularly to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%higher-order logics, turn out to be comparatively straighforward to be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%defined in the main lines --- although not so to be carried out in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%, due to the richness in syntax, the specific way evaluation is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%implemented, as well as to issues associated with classes (Haskell),
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%overloading and side effects.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%All functions are total in HOL. Partiality may be dealt with by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%lifting types through the \emph{option} type constructor. HOL has an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%implementation of recursive functions based on Tarski fixed-point
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%theorem. Defining a recursive function requires giving a specific
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%measure and proving monotonicity about it.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% HOL has an implementation of recursive functions, based on Tarski
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% fixed-point theorem. Their definition in general requires specific
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% measure to be given each time, for monotonicity to be proved.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% Moreover, partial functions are needed to programs that might not
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% terminate, but in HOL all functions are total. Partiality may be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% dealt with by lifting types through \emph{option}, a type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% constructor in HOL. This inevitably complicates case expressions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%There are different general approaches depending on the style of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%semantics. The expressiveness of the logical language may also make a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%big difference.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe Haskell classes Eq and Ord are translated to corresponding classes
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclared, respectively, in HsHOL.thy and HsHOLCF.thy. These classes
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifor the moment are taken to be absolutely generic ones (with empty
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniaxiomatisation).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Isabelle-HOL}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle-HOL as an implementation of classical higher-order logic
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinisupports the definition of datatypes and recursive functions.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniHowever, it distinguishes between primitive recursion (keyword
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniemph{primrec}), in which termination is trivially guaranteed by
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidecrease in the complexity of a parameter, and recursion (keyword
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniemph{recdef}) for which an appropriate specific measure must be
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprovided in order to get the termination proof to go through.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniMoreover, HOL does not have a notion of undefined suitable for
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicomputations --- therefore all functions have to be total.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThis translation of recursive functions is restricted to total
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniprimitive recursive functions that are recursive in their first
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidatatype argument. The Haskell definition should be a case expression
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniin which all the constructors are considered in their datatype
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinideclaration order, save for the use of a wildcard.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%Wildcards cannot be used for constructor arguments.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%Moreover, the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%case variable should not be used in the specific case expression (just
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%replace it with the specific case pattern).
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniMutually recursive functions are allowed under additional
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestrictions. All the functions should be recursive in the same type,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinithe constructors should be listed in the same order in each of the
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicase expressions, and also the variable names in the case patterns are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torriniexpected to be maintained.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe translation of mutually recursive functions $a \rightarrow b, \ldots a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\rightarrow d$ introduces a new function $a \rightarrow (b * \ldots * d)$
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinidefined, for each case pattern, as the product of the values
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinicorrespondingly taken by the original functions.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Isabelle-HOLCF}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIsabelle-HOLCF is the implementation of the theory of computable
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinifunctions on top of higher-order logic, relying on axiomatic classes.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn comparison with HOL, the handling of partial functions is more
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrininatural, and the presence of the fixpoint operator allows for a
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinigeneral treatment of recursive functions. However, types in HOLCF can
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinibe interpreted as pointed complete partial orders (pcpo), and this
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirequires all standard types to be lifted.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniIn the present translation, the type constructor \emph{lift} is used
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinito lift types, in association with the corresponding lifting function
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\emph{Def} and with the undefined value \emph{UU}. Datatypes are
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinitranslated to domains --- complete with destructors from declaration.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniThe class \emph{pcpo} is added to the sort of each type variable.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo TorriniPartial recursive functions (defined by case expressions), including
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinimutually recursive ones, are covered without any essential
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinirestrictions, relying on the recdef package.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\end{document}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini as well as an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperational, but is quite deep.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniit builds into HOL a specific domain class for the interpretation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHigher-level approaches relying on denotational
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini propose level
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniapproaches based on large-step operational semantics, even if with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisome complication when dealing with higher-order programming languages
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisuch as those presented in \cite{} --- Miranda in FOL; \cite{} ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell in FOL; \cite{} --- Haskell in the Agda implementation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMartin-Loef type theory. More expressiveness is usually required by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihigh-level approaches based on denotational semantics, such as those
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipresented in \cite{} --- Haskell in HOLCF and HOL; \cite{} --- ML in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe main one, is which Depending on the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressiveness of the logic, the translation of the programming
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilanguage may be carried out at different levels of depth. In general,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe deeper is the embedding, the less it relies on meta-level features
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the target language. This may be a plus, either from the point of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniview of semantic clarity, or from that of expressiveness. Taking
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniadvantage of meta-level feaures, on the other hand, may be useful in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniorder to make the theorem proving less tedious, by allowing more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconstant use of generic proof methods. It may also ultimately affect
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipositively the theorem prover economy, by reinforcing the bias toward
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe development of proof methods that, however specific, can be more
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieasily integrated with generic ones.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSome significantly different examples of functional programming
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilanguages embedded into the logic of a theorem prover can be found in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{} (Miranda on Isabelle), \cite{} (ML on Isabelle), \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(Haskell on Isabelle), \cite{} (Haskell on Agda). Example of lower
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilevel approaches are given in \cite{}, where Haskell is translated
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto the Agda implementation of Martin-Loef theory based on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioperational rules and relies on operational semantics for correctness,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis followed in \cite{}, where Haskell is embedded into the Agda
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimplementation of Martin-Loef theory, as well as in the embeddings of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMiranda \cite{} and Haskell \cite{} into FOL (classical first-order
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilogic, until the middle of the nineties still probably the best
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisupported logic on Isabelle). Higher-level approaches, such as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipresented in \cite{} (embedding ML into HOL), and in \cite{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(embedding Haskell into HOLCF and into HOL), rely ultimately on
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotational semantics for correctenss. This, together with the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexpressiveness allowed by higher-order logic for the formulation of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirequirements, gives the considerable advantage of enabling proofs that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare more abstract and closer to mathematical intuition.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimethod for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxiomatic encoding of monads in HOL that uses parametrisation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniParametrisation based on theory morphism has been implemented, as a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconservative extension of various Isabelle logics, in AWE, a tool
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidesigned to support proof reuse \cite{AWE}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniit is not complete, and cannot be trivially completed ---
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininotably, type constructor classes have not been considered, since
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIsabelle does not have them. However, we are expecting to deal with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithis problem by relying on an extension of Isabelle based on theory
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimorphism (see section \ref{}) .