Proof Relevant Corecursive Resolution
Extracted source text · arXiv 1511.09394
\documentclass{llncs}
\usepackage{xcolor}
\usepackage{tikz-qtree}
\usepackage{etex}
%\usepackage{fullpage}
\usepackage{amsmath}
%\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{proof}
\usepackage{hyperref}
\usepackage{caption}
\usepackage{comment}
\usepackage{subcaption}
\usepackage{fancybox}
\usepackage{stmaryrd}
\usepackage{todonotes}
\newcommand{\knote}[1]{\todo[inline, color=blue!20]{#1}}
\newcommand{\tom}[1]{\todo[inline, color=red!30]{#1}}
\definecolor{light-gray}{gray}{0.86}
\newcommand{\nil}[0]{\mathsf{nil}}
\newcommand{\cons}[0]{\mathsf{cons}}
\newcommand{\vecc}[0]{\mathsf{vec}}
\newcommand{\suc}[0]{\mathsf{S}}
\newcommand{\nat}[0]{\mathsf{Nat}}
\newcommand{\ind}[0]{\mathsf{Ind}}
\newcommand{\app}[0]{\mathsf{app}}
\newcommand{\selfstar}[0]{$\mathsf{Selfstar}\ $}
\newcommand{\self}[0]{\mathbf{S}}
\newcommand{\fomega}[0]{\mathbf{F}_{\omega}}
\newcommand{\cc}[0]{\mathbf{CC}}
\newcommand{\gray}[1]{\colorbox{light-gray}{#1}}
\newcommand{\mgray}[1]{\colorbox{light-gray}{$#1$}}
\newcommand{\M}[3]{
\{#1_i \mapsto #2_i\}_{i \in #3}}
\newcommand{\Mb}[4]{
\{#1_i:#4_i \mapsto #2_i\}_{i \in #3}}
\newcommand{\interp}[1]{\llbracket #1 \rrbracket}
\newcommand{\mylet}[2]{\mathbf{let}\ #1 \ \mathbf{in} \ #2}
\newcommand{\fix}[1]{\mathbf{fix}(#1)}
\newcommand{\mycase}[2]{\mathbf{case}\ #1 \ \mathbf{of} \ \{ #2 \}_{i\in {N}}}
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}}
\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 ---F.P.]}}}
\newcommand{\remph}[1]{\textcolor{blue}{#1}}
%% \newarrowfiller{dasheq} {==}{==}{==}{==}
%% \newarrow {Mapsto} ||--->
%% \newarrow {Line} -----
%% \newarrow {Implies} ===={=>}
%% \newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
%% \newarrow {Onto} ----{>>}
%% \newarrow {DashInto} C{dash}{}{dash}{>}
%% \newarrow {Dashto}{}{dash}{}{dash}{>}
%% \newarrow {Dashtoo}{}{dash}{}{dash}{>>}
%% ODER: format == = "\mathrel{==}"
%% ODER: format /= = "\neq "
%
%
\makeatletter
\@ifundefined{lhs2tex.lhs2tex.sty.read}%
{\@namedef{lhs2tex.lhs2tex.sty.read}{}%
\newcommand\SkipToFmtEnd{}%
\newcommand\EndFmtInput{}%
\long\def\SkipToFmtEnd#1\EndFmtInput{}%
}\SkipToFmtEnd
\newcommand\ReadOnlyOnce[1]{\@ifundefined{#1}{\@namedef{#1}{}}\SkipToFmtEnd}
\usepackage{amstext}
\usepackage{amssymb}
\usepackage{stmaryrd}
\DeclareFontFamily{OT1}{cmtex}{}
\DeclareFontShape{OT1}{cmtex}{m}{n}
{<5><6><7><8>cmtex8
<9>cmtex9
<10><10.95><12><14.4><17.28><20.74><24.88>cmtex10}{}
\DeclareFontShape{OT1}{cmtex}{m}{it}
{<-> ssub * cmtt/m/it}{}
\newcommand{\texfamily}{\fontfamily{cmtex}\selectfont}
\DeclareFontShape{OT1}{cmtt}{bx}{n}
{<5><6><7><8>cmtt8
<9>cmbtt9
<10><10.95><12><14.4><17.28><20.74><24.88>cmbtt10}{}
\DeclareFontShape{OT1}{cmtex}{bx}{n}
{<-> ssub * cmtt/bx/n}{}
\newcommand{\tex}[1]{\text{\texfamily#1}} % NEU
\newcommand{\Sp}{\hskip.33334em\relax}
\newcommand{\Conid}[1]{\mathit{#1}}
\newcommand{\Varid}[1]{\mathit{#1}}
\newcommand{\anonymous}{\kern0.06em \vbox{\hrule\@width.5em}}
\newcommand{\plus}{\mathbin{+\!\!\!+}}
\newcommand{\bind}{\mathbin{>\!\!\!>\mkern-6.7mu=}}
\newcommand{\rbind}{\mathbin{=\mkern-6.7mu<\!\!\!<}}% suggested by Neil Mitchell
\newcommand{\sequ}{\mathbin{>\!\!\!>}}
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}
\usepackage{polytable}
%mathindent has to be defined
\@ifundefined{mathindent}%
{\newdimen\mathindent\mathindent\leftmargini}%
{}%
\def\resethooks{%
\global\let\SaveRestoreHook\empty
\global\let\ColumnHook\empty}
\newcommand*{\savecolumns}[1][default]%
{\g@addto@macro\SaveRestoreHook{\savecolumns[#1]}}
\newcommand*{\restorecolumns}[1][default]%
{\g@addto@macro\SaveRestoreHook{\restorecolumns[#1]}}
\newcommand*{\aligncolumn}[2]%
{\g@addto@macro\ColumnHook{\column{#1}{#2}}}
\resethooks
\newcommand{\onelinecommentchars}{\quad-{}- }
\newcommand{\commentbeginchars}{\enskip\{-}
\newcommand{\commentendchars}{-\}\enskip}
\newcommand{\visiblecomments}{%
\let\onelinecomment=\onelinecommentchars
\let\commentbegin=\commentbeginchars
\let\commentend=\commentendchars}
\newcommand{\invisiblecomments}{%
\let\onelinecomment=\empty
\let\commentbegin=\empty
\let\commentend=\empty}
\visiblecomments
\newlength{\blanklineskip}
\setlength{\blanklineskip}{0.66084ex}
\newcommand{\hsindent}[1]{\quad}% default is fixed indentation
\let\hspre\empty
\let\hspost\empty
\newcommand{\NB}{\textbf{NB}}
\newcommand{\Todo}[1]{$\langle$\textbf{To do:}~#1$\rangle$}
\EndFmtInput
\makeatother
%
%
%
%
%
%
% This package provides two environments suitable to take the place
% of hscode, called "plainhscode" and "arrayhscode".
%
% The plain environment surrounds each code block by vertical space,
% and it uses \abovedisplayskip and \belowdisplayskip to get spacing
% similar to formulas. Note that if these dimensions are changed,
% the spacing around displayed math formulas changes as well.
% All code is indented using \leftskip.
%
% Changed 19.08.2004 to reflect changes in colorcode. Should work with
% CodeGroup.sty.
%
\ReadOnlyOnce{polycode.fmt}%
\makeatletter
\newcommand{\hsnewpar}[1]%
{{\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
% can be used, for instance, to redefine the code size, by setting the
% command to \small or something alike
\newcommand{\hscodestyle}{}
% The command \sethscode can be used to switch the code formatting
% behaviour by mapping the hscode environment in the subst directive
% to a new LaTeX environment.
\newcommand{\sethscode}[1]%
{\expandafter\let\expandafter\hscode\csname #1\endcsname
\expandafter\let\expandafter\endhscode\csname end#1\endcsname}
% "compatibility" mode restores the non-polycode.fmt layout.
\newenvironment{compathscode}%
{\par\noindent
\advance\leftskip\mathindent
\hscodestyle
\let\\=\@normalcr
\(\pboxed}%
{\endpboxed\)%
\par\noindent
\ignorespacesafterend}
\newcommand{\compaths}{\sethscode{compathscode}}
% "plain" mode is the proposed default.
\newenvironment{plainhscode}%
{\hsnewpar\abovedisplayskip
\advance\leftskip\mathindent
\hscodestyle
\let\\=\@normalcr
\(\pboxed}%
{\endpboxed\)%
\hsnewpar\belowdisplayskip
\ignorespacesafterend}
% Here, we make plainhscode the default environment.
\newcommand{\plainhs}{\sethscode{plainhscode}}
\plainhs
% The arrayhscode is like plain, but makes use of polytable's
% parray environment which disallows page breaks in code blocks.
\newenvironment{arrayhscode}%
{\hsnewpar\abovedisplayskip
\advance\leftskip\mathindent
\hscodestyle
\let\\=\@normalcr
\(\parray}%
{\endparray\)%
\hsnewpar\belowdisplayskip
\ignorespacesafterend}
\newcommand{\arrayhs}{\sethscode{arrayhscode}}
% The mathhscode environment also makes use of polytable's parray
% environment. It is supposed to be used only inside math mode
% (I used it to typeset the type rules in my thesis).
\newenvironment{mathhscode}%
{\parray}{\endparray}
\newcommand{\mathhs}{\sethscode{mathhscode}}
% texths is similar to mathhs, but works in text mode.
\newenvironment{texthscode}%
{\(\parray}{\endparray\)}
\newcommand{\texths}{\sethscode{texthscode}}
% The framed environment places code in a framed box.
\def\codeframewidth{\arrayrulewidth}
\RequirePackage{calc}
\newenvironment{framedhscode}%
{\parskip=\abovedisplayskip\par\noindent
\hscodestyle
\arrayrulewidth=\codeframewidth
\tabular{@{}|p{\linewidth-2\arraycolsep-2\arrayrulewidth-2pt}|@{}}%
\hline\framedhslinecorrect\\{-1.5ex}%
\let\endoflinesave=\\
\let\\=\@normalcr
\(\pboxed}%
{\endpboxed\)%
\framedhslinecorrect\endoflinesave{.5ex}\hline
\endtabular
\parskip=\belowdisplayskip\par\noindent
\ignorespacesafterend}
\newcommand{\framedhslinecorrect}[2]%
{#1[#2]}
\newcommand{\framedhs}{\sethscode{framedhscode}}
% The inlinehscode environment is an experimental environment
% that can be used to typeset displayed code inline.
\newenvironment{inlinehscode}%
{\(\def\column##1##2{}%
\let\>\undefined\let\<\undefined\let\\\undefined
\newcommand\>[1][]{}\newcommand\<[1][]{}\newcommand\\[1][]{}%
\def\fromto##1##2##3{##3}%
\def\nextline{}}{\) }%
\newcommand{\inlinehs}{\sethscode{inlinehscode}}
% The joincode environment is a separate environment that
% can be used to surround and thereby connect multiple code
% blocks.
\newenvironment{joincode}%
{\let\orighscode=\hscode
\let\origendhscode=\endhscode
\def\endhscode{\def\hscode{\endgroup\def\@currenvir{hscode}\\}\begingroup}
%\let\SaveRestoreHook=\empty
%\let\ColumnHook=\empty
%\let\resethooks=\empty
\orighscode\def\hscode{\endgroup\def\@currenvir{hscode}}}%
{\origendhscode
\global\let\hscode=\orighscode
\global\let\endhscode=\origendhscode}%
\makeatother
\EndFmtInput
%
%REGENERATE:
%unlines ["%format " ++ l ++ num ++ ap | l <- map (:[]) (['a'..'z'] ++ ['A'..'Z']), num <- "" : map show [0..9], ap <- ["","'","''"], not (null (l ++ num ++ ap))]
%
%
% First, let's redefine the forall, and the dot.
%
%
% This is made in such a way that after a forall, the next
% dot will be printed as a period, otherwise the formatting
% of `comp_` is used. By redefining `comp_`, as suitable
% composition operator can be chosen. Similarly, period_
% is used for the period.
%
\ReadOnlyOnce{forall.fmt}%
\makeatletter
% The HaskellResetHook is a list to which things can
% be added that reset the Haskell state to the beginning.
% This is to recover from states where the hacked intelligence
% is not sufficient.
\let\HaskellResetHook\empty
\newcommand*{\AtHaskellReset}[1]{%
\g@addto@macro\HaskellResetHook{#1}}
\newcommand*{\HaskellReset}{\HaskellResetHook}
\global\let\hsforallread\empty
\newcommand\hsforall{\global\let\hsdot=\hsperiodonce}
\newcommand*\hsperiodonce[2]{#2\global\let\hsdot=\hscompose}
\newcommand*\hscompose[2]{#1}
\AtHaskellReset{\global\let\hsdot=\hscompose}
% In the beginning, we should reset Haskell once.
\HaskellReset
\makeatother
\EndFmtInput
%------------------------------------------------------------------------------
% LaTeX macros
% the `doubleequals' macro is due to Jeremy Gibbons
\def\doubleequals{\mathrel{\unitlength 0.01em
\begin{picture}(78,40)
\put(7,34){\line(1,0){25}} \put(45,34){\line(1,0){25}}
\put(7,14){\line(1,0){25}} \put(45,14){\line(1,0){25}}
\end{picture}}}
%------------------------------------------------------------------------------
%%% Haskell
%%% GHC's UnicodeSyntax
% operators
% format >>= = "\mathbin{\rhd}"
% \shortmid, \sslash
% format |> = "\mathbin{\rhd}"
% format |→ = "\mathbin{\mapsto}"
% format :→ = "\mathbin{\times}"
% format |→ = "\mathbin{\times}"
% format +> = "\mathbin{\triangleright}"
% format <: = "\preccurlyeq "
%%% set theory
%%% logic
%%% binders:
%%% functors:
%%% natural transformations:
%%% applicative functors:
%\newtheorem{conjecture}{Conjecture}
%% \newtheorem{lemma}{Lemma}
%% \newtheorem{theorem}{Theorem}
%% \newtheorem{definition}{Definition}
%\newtheorem{example}{Example}
%\newtheorem{procedure}{Procedure}
%\newtheorem{conjecture}{Conjecture}
% for page numbers:
\pagestyle{plain}
\begin{document}
\title{Proof Relevant Corecursive Resolution}
%\subtitle{with application to diverging type class resolution}
\author{Peng Fu\inst{1}\thanks{This author is supported by EPSRC grant EP/K031864/1.}, Ekaterina Komendantskaya\inst{1}, Tom Schrijvers\inst{2}, Andrew Pond\inst{1}\thanks{This author is supported by Carnegie Trust Scotland.}}
\institute{Computer Science, University of Dundee \and
Department of Computer Science, KU Leuven }
\maketitle
\begin{abstract}
Resolution lies at the foundation of both logic programming and type class
context reduction in functional languages.
Terminating derivations by resolution have well-defined inductive meaning,
whereas some non-terminating derivations can be understood coinductively.
%First-order resolution is not
%guaranteed to terminate and non-terminating derivations are often considered
%meaningless. Nevertheless many non-terminating derivations have coinductive meaning.
Cycle detection is a popular method to capture a small subset of such
derivations. We show that in fact cycle detection is a restricted form of
coinductive proof, in which the atomic formula forming the cycle plays the
r\^{o}le of coinductive hypothesis.
This paper introduces a heuristic method for obtaining richer coinductive
hypotheses in the form of Horn formulas. Our approach subsumes cycle detection
and gives coinductive meaning to a larger class of derivations. For this
purpose we extend resolution with Horn formula resolvents and corecursive
evidence generation. We illustrate our method on non-terminating type class
resolution problems.
%Type class is a mechanism to support ad hoc polymorphism, which originates in
%Haskell. They are typically implemented by passing dictionaries at
%compile time. These dictionaries are obtained as the proof evidence
% for a given type class constraint. The construction of these evidence
%can be viewed as a resolution process on a set of Horn formulas(in the form of instance
%declarations).
%Existing approaches require the resolution process to terminate modulo
%cycles. This is unfortunate because it rejects advanced applications in-
%volving nested datatypes and datatype-generic programming where res-
%olution easily diverges without forming cycles.
%This paper generalizes the resolution to support such applications. For
%this purpose we first identify an invariant formula that implicitly underlies
%the diverging resolution, and then resolve the invariant formula by means of
%\textit{corecursive resolution}. This allows us
%to derive a finite representation for a corecursive proof witness suitable for
%dictionary passing.
%Horn-clause logic is a fragment of first-order logic famous for its elegant semantics (i.e. least and greatest Herbrand model semantics) and
%efficient implementations (i.e. via (SLD-)resolution algorithm). It provides foundations for Logic programming (and Prolog),
%but equally gives rise to a variety of implementations in other programming languages. One such application -- the use of Horn clause resolution in Type class inference in Haskell
%is taken as a leading example application in this paper.
% Horn-clause logic lies in the foundations of both logic programming and type inference methods in functional languages.
% First-order resolution in Horn-clause logic is a semi-decidable procedure, i.e. not all derivations are guaranteed to terminate. %: i.e. only terminating derivations deliver sound answers.
% Some non-terminating derivations can be understood coinductively. The most popular method to implement coiductive reasoning
% in resolution is cycle detection. However, it is limited to cases in which infinite derivations exhibit cycles.
% There are, however, interesting examples of Horn-clause programs for which infinite derivations do not exhibit cycles, but nevertheless
% have meaningful coinductive semantics.
% In this paper, we show that cycle detection widely used in resolution is in fact an instance of a more general method of coinductive hypothesis formation, already known in the literature on
% induction and coinduction in (functional) interactive theorem provers. Moreover, cycle detection only allows to find coinductive hypotheses of patricular -- atomic -- shape.
% This new perspective allows us to see that the problem of extending coinductive methods of resolution can receive a new solution, -- via extensions to the shape of coinductive hypotheses found during the proof search.
% We introduce a new method for richer coinductive hypothesis formation for resolution, show its soundness, and illustrate its practical use in type class resolution problems.
\textbf{Keywords:} Horn Clause Logic, Resolution, Corecursion, Haskell Type Class Inference, Coinductive Proofs.
\end{abstract}
%===============================================================================
%\input{introK}
\section{Introduction}
\label{intro}
Horn clause logic is a fragment of first-order logic known for its simple syntax, well-defined models, and efficient algorithms for automated proof search.
It is used in a variety of applications, from program verification~\cite{BjornerGMR15} to type inference in object-oriented programming languages ~\cite{AnconaLagorio11}.
Similar syntax and proof methods underlie type inference in functional programming languages~\cite{wadler1989make,Lammel:2005}.
%We study its pontential application in functional
%programming languages in this paper.
%functional~\cite{wadler1989make,Lammel:2005} programming languages.
% lies in the foundations of logic programming and Prolog. %, but also
%gives rise to a variety of applications,
For example, the following declaration
specifies equality class instances for pairs and integers in Haskell:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{instance}\;\Conid{Eq}\;\Conid{Int}\;\mathbf{where}\mathbin{...}{}\<[E]%
\\
\>[3]{}\mathbf{instance}\;(\Conid{Eq}\;\Varid{x},\Conid{Eq}\;\Varid{y})\Rightarrow \Conid{Eq}\;(\Varid{x},\Varid{y})\;\mathbf{where}\mathbin{...}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
%The above syntax can be used to model the Haskell type-class setting as follows.
%Terms denote Haskell types like |Int| or |(x,y)|, and atomic formulas
%denote Haskell type class constraints on types like |Eq (Int,Int)|.
\noindent It corresponds to a Horn clause program $\Phi_{\ensuremath{\Conid{Pair}}}$ with two clauses $\kappa_{\ensuremath{\Conid{Int}}}$ and $\kappa_{\ensuremath{\Conid{Pair}}}$: % with the labels indicating the
%underlining evidence construction functions:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{17}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\Conid{Int}\mathbin{:}{}\<[17]%
\>[17]{}\Conid{Eq}\;\Conid{Int}{}\<[E]%
\\
\>[3]{}\kappa_\Conid{Pair}\mathbin{:}(\Conid{Eq}\;\Varid{x},\Conid{Eq}\;\Varid{y})\Rightarrow \Conid{Eq}\;(\Varid{x},\Varid{y}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
%\frank{We may need more smooth transition to cycle detection without giving too much details on model semantics. Also, I am not sure we want to talk too much about traditional logic program(and CoLP), since we do not deal with unification in the paper. Moreover, I suggest we use resolution instead of SLD-resolution in the intro.}
%\knote{If we want to talk about this paper making contributions to LP, we have to mention what coinduction means in LP/CoLP... I am not sure what ``smooth transition means here''}
Horn clause logic uses SLD-resolution as an inference engine.
%It is well-known that SLD-resolution is sound and complete for terminating queries:
If a derivation for a given formula $A$ and a Horn clause program $\Phi$ terminates successfully with substitution $\theta$,
then $\theta A$ is logically entailed by $\Phi$, or $\Phi \vdash \theta A$. The search for a suitable $\theta$ reflects the problem-solving nature of SLD-resolution.
When the unification algorithm underlying SLD-resolution is restricted to matching, resolution can be viewed as theorem proving:
the successful terminating derivations for $A$ using $\Phi$ will guarantee $\Phi \vdash A$.
For example, $ \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})} \leadsto \ensuremath{\Conid{Eq}\;\Conid{Int}}, \ensuremath{\Conid{Eq}\;\Conid{Int}} \leadsto \ensuremath{\Conid{Eq}\;\Conid{Int}} \leadsto \emptyset$.
Therefore, we have:
$\Phi_{\ensuremath{\Conid{Pair}}} \vdash \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})}$.
For the purposes of this paper, we always assume resolution by term-matching.
To emphasize the proof-theoretic meaning of resolution, we will record
proof evidence alongside the derivation steps. For instance, \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})} is proven by applying the clauses $\kappa_{\ensuremath{\Conid{Pair}}}$ and $\kappa_{\ensuremath{\Conid{Int}}}$.
We denote this by $\Phi_{\ensuremath{\Conid{Pair}}} \vdash \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})} \Downarrow
\kappa_{\ensuremath{\Conid{Pair}}}\ \kappa_{\ensuremath{\Conid{Int}}}\ \kappa_{\ensuremath{\Conid{Int}}}$. %% There is work by Fu and Komendantskaya \cite{FuK15} containing a detailed discussion of Horn formulas as types and proof evidence as terms.
%See also~\cite{FuK15} for a detailed discussion
Horn clause logic can have inductive and coinductive interpretation, via the least and greatest fixed points of the \emph{consequence operator} $F_{\Phi}$. % has received two kinds of fixed point semantics formulated using a fixpoint operator defined on sets of ground formulas of the given sigature.
Given a Horn clause program $\Phi$, and a set $S$ containing (ground) formulas formed from the signature of $\Phi$,
$F_{\Phi}(S) = \{\sigma A\ | \ \sigma B_1, \ldots , \sigma B_n \in S \textrm{ and } B_1, \ldots B_n \Rightarrow A \in \Phi \}$~\cite{Llo87}.
Through the Knaster-Tarski construction, the least fixed point of this operator gives the set of all finite ground formulas \emph{inductively entailed} by $\Phi$.
Extending $S$ to include infinite terms,
the greatest fixed point of $F_{\Phi}$ defines the set of all finite and infinite ground formulas \emph{coinductively entailed} by $\Phi$.
Inductively, SLD-resolution is sound: if $\Phi \vdash A$, then $A$ is inductively entailed by $\Phi$.
It is more difficult to characterise coinductive entailment computationally;
%obtain a similar soundness result for non-terminating derivations and coinductive entailment,
several alternative approaches %to relating infinite derivations and coinductive entailment
exist~\cite{SimonBMG07,Llo87,KJ15}.
% several soundness results exist in the literature, that relate
%Some derivations do not terminate. Yet, many of those non-terminating
%derivations do have corecursive interpretation.
%Unfortunately, it is not trivial to implement this intuition in practice.
So far the most
popular solution has been to use cycle detection~\cite{SimonBMG07}: if a cycle
is found in a derivation for a formula $A$ and a Horn clause program $\Phi$,
then $A$ is coinductively entailed by $\Phi$.
%the derivation is closed corecursively. \frank{I change coinductive to corecursive.}
Consider, as an example, the following Horn clause program $\Phi_{AB}$:
%\frank{I suggest we use the following notation, i.e. only variables are lower case, and use applicative syntax a la haskell to minimize parens.}
%\knote{I am leaving it to you, i have started changing it as you like,...}
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\Conid{A}\mathbin{:}\Conid{B}\;\Varid{x}\Rightarrow \Conid{A}\;\Varid{x}{}\<[E]%
\\
\>[3]{}\kappa_\Conid{B}\mathbin{:}\Conid{A}\;\Varid{x}\Rightarrow \Conid{B}\;\Varid{x}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
It gives rise to an infinite derivation $ A\ x \leadsto B\ x \leadsto A\ x \leadsto \ldots $.
By noticing the cycle, %coinductive dialect of Prolog CoLP~\cite{SimonBMG07}
%we can close the derivation corecursively \frank{I change coinductive to corecursive.},
we can conclude that (an instance) of $A\ x$ is coinductively entailed by $\Phi_{AB}$.
%The question is: how to realise this reasoning \emph{computationally}?
We are able to \emph{construct} a proof evidence that reflects the circular nature of this derivation: $\alpha = \kappa_A\ (\kappa_B \ \alpha)$.
This being a corecursive equation, we can represent it with the standard $\mu$ operator, $\mu \alpha. \kappa_A\ (\kappa_B \ \alpha)$. Now we have
$\Phi_{AB} \vdash A\ x \Downarrow \mu \alpha. \kappa_A\ (\kappa_B \ \alpha)$.
%\frank{I add a para here.}
%In terminology of~\cite{MD97}, recursion is defined by a function from a least fixed point and corecursion by a function into a greatest fixed point.
%This fits with the classical fixed-point semantics of Horn clause Logic:
%finite successful derivations are \emph{recursive} and infinite non-failing derivations are \emph{corecursive} in this sense. Now we see Horn clauses as types and proof evidence as terms,
%we can give an alternative meaning to the analogy of~\cite{MD97}, in a functional style of~\cite{GH05}, as follows.
According to Gibbons and Hutton~\cite{GH05} and inspired by Moss and Danner~\cite{MD97}, a corecursive program is defined to be a function whose range is a type defined recursively as the greatest solution of some equation (i.e. whose range is a coinductive type).
% In this paper, we use the terminology \textit{corecursive/corecursion} to describe situation that involves mu-term.
We can informally understand the Horn clause $\Phi_{AB}$ as the following Haskell data type declarations:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{20}{@{}>{\hspre}c<{\hspost}@{}}%
\column{20E}{@{}l@{}}%
\column{23}{@{}>{\hspre}l<{\hspost}@{}}%
\column{24}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{data}\;\Conid{B}\;\Varid{x}{}\<[20]%
\>[20]{}\mathrel{=}{}\<[20E]%
\>[23]{}\Conid{K_B}\;(\Conid{A}\;\Varid{x}){}\<[E]%
\\
\>[3]{}\mathbf{data}\;\Conid{A}\;\Varid{x}{}\<[20]%
\>[20]{}\mathrel{=}{}\<[20E]%
\>[24]{} \Conid{K_A}\;(\Conid{B}\;\Varid{x}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\noindent So the corecursive evidence $\mu \alpha. \kappa_A\ (\kappa_B \ \alpha)$ for $A\ x$ corresponds
to the corecursive program $(d\ :: A\ x) =\ K_A \ (K_B \ d)$.
In our case, the corecursive evidence $d$ is that function, and its range type $A \ x$ can be seen as a coinductive type. % (note that every type is coinductive in Haskell).
Corecursion also arises in type class inference.
Consider the following mutually recursive definitions of lists of even
and odd length in Haskell:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{20}{@{}>{\hspre}c<{\hspost}@{}}%
\column{20E}{@{}l@{}}%
\column{23}{@{}>{\hspre}l<{\hspost}@{}}%
\column{24}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{data}\;\Conid{OddList}\;\Varid{a}{}\<[20]%
\>[20]{}\mathrel{=}{}\<[20E]%
\>[23]{}\Conid{OCons}\;\Varid{a}\;(\Conid{EvenList}\;\Varid{a}){}\<[E]%
\\
\>[3]{}\mathbf{data}\;\Conid{EvenList}\;\Varid{a}{}\<[20]%
\>[20]{}\mathrel{=}{}\<[20E]%
\>[24]{}\Conid{Nil}\mid \Conid{ECons}\;\Varid{a}\;(\Conid{OddList}\;\Varid{a}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
They give rise to \ensuremath{\Conid{Eq}} type class instance declarations that can be expressed
using the following Horn clause program $\Phi_{EvenOdd}$:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\Conid{Odd}\mathbin{:}(\Conid{Eq}\;\Varid{a},\Conid{Eq}\;(\Conid{EvenList}\;\Varid{a}))\Rightarrow \Conid{Eq}\;(\Conid{OddList}\;\Varid{a}){}\<[E]%
\\
\>[3]{}\kappa_\Conid{Even}\mathbin{:}(\Conid{Eq}\;\Varid{a},\Conid{Eq}\;(\Conid{OddList}\;\Varid{a}))\Rightarrow \Conid{Eq}\;(\Conid{EvenList}\;\Varid{a}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
When resolving the type class constraint \ensuremath{\Conid{Eq}\;(\Conid{OddList}\;\Conid{Int})}, Haskell's standard type class resolution diverges.
The state-of-the-art is to use cycle detection~\cite{Lammel:2005} to terminate otherwise infinite
derivations.
Resolution for \ensuremath{\Conid{Eq}\;(\Conid{OddList}\;\Conid{Int})} exhibits a cycle on the atomic formula \ensuremath{\Conid{Eq}\;(\Conid{OddList}\;\Conid{Int})}, thus the derivation can be terminated,
%terminates and yields a
with corecursive evidence $\mu \alpha . \ensuremath{\kappa_\Conid{Odd}\;\kappa_\Conid{Int}\;(\kappa_\Conid{Even}\;\kappa_\Conid{Int}\;\alpha)}$.
%and
%output the answer ``True coinductively'' for |P x|.
The method of cycle detection is rather limited: there are many Horn clause
programs that have coinductive meaning, but do not give rise to
detectable cycles. For example, consider the program $\Phi_Q$:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{15}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\Conid{S}\mathbin{:}(\Conid{Q}\;(\Conid{S}\;(\Conid{G}\;\Varid{x})),\Conid{Q}\;\Varid{x})\Rightarrow \Conid{Q}\;(\Conid{S}\;\Varid{x}){}\<[E]%
\\
\>[3]{}\kappa_\Conid{G}\mathbin{:}\Conid{Q}\;\Varid{x}\Rightarrow \Conid{Q}\;(\Conid{G}\;\Varid{x}){}\<[E]%
\\
\>[3]{}\kappa_\Conid{Z}\mathbin{:}{}\<[15]%
\>[15]{}\Conid{Q}\;\Conid{Z}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
It gives rise to the following derivation without cycling:
\noindent $\underline{Q\ (S\ Z)} \leadsto Q\ Z, \underline{Q\ (S\ (G\ Z))} \leadsto Q\ Z, Q\ (G\ Z), \underline{Q\ (S \ (G\ (G\ Z)))} \leadsto \ldots$.
When such derivations arise, we cannot terminate the derivation by cycle detection. %% and thus cannot apply the above method.
Let us look at a similar situation for type classes. Consider a datatype-generic representation of perfect trees: a
nested datatype~\cite{bird1998nested}, with fixpoint \ensuremath{\Conid{Mu}} of the higher-order functor \ensuremath{\Conid{HPTree}} \cite{johann2009haskell}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{16}{@{}>{\hspre}c<{\hspost}@{}}%
\column{16E}{@{}l@{}}%
\column{19}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{data}\;\Conid{Mu}\;\Varid{h}\;\Varid{a}{}\<[16]%
\>[16]{}\mathrel{=}{}\<[16E]%
\>[19]{}\Conid{In}\;\{\mskip1.5mu \Varid{out}\mathbin{::}\Varid{h}\;(\Conid{Mu}\;\Varid{h})\;\Varid{a}\mskip1.5mu\}{}\<[E]%
\\[\blanklineskip]%
\>[3]{}\mathbf{data}\;\Conid{HPTree}\;\Varid{f}\;\Varid{a}\mathrel{=}\Conid{HPLeaf}\;\Varid{a}\mid \Conid{HPNode}\;(\Varid{f}\;(\Varid{a},\Varid{a})){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
These two datatypes give rise to the following \ensuremath{\Conid{Eq}} type class instances.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{5}{@{}>{\hspre}l<{\hspost}@{}}%
\column{16}{@{}>{\hspre}c<{\hspost}@{}}%
\column{16E}{@{}l@{}}%
\column{19}{@{}>{\hspre}c<{\hspost}@{}}%
\column{19E}{@{}l@{}}%
\column{20}{@{}>{\hspre}l<{\hspost}@{}}%
\column{22}{@{}>{\hspre}l<{\hspost}@{}}%
\column{31}{@{}>{\hspre}c<{\hspost}@{}}%
\column{31E}{@{}l@{}}%
\column{34}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{instance}\;\Conid{Eq}\;(\Varid{h}\;(\Conid{Mu}\;\Varid{h})\;\Varid{a})\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Varid{h}\;\Varid{a})\;\mathbf{where}{}\<[E]%
\\
\>[3]{}\hsindent{2}{}\<[5]%
\>[5]{}\Conid{In}\;\Varid{x}\equiv \Conid{In}\;\Varid{y}{}\<[19]%
\>[19]{}\mathrel{=}{}\<[19E]%
\>[22]{}\Varid{x}\equiv \Varid{y}{}\<[E]%
\\[\blanklineskip]%
\>[3]{}\mathbf{instance}\;(\Conid{Eq}\;\Varid{a},\Conid{Eq}\;(\Varid{f}\;(\Varid{a},\Varid{a})))\Rightarrow \Conid{Eq}\;(\Conid{HPTree}\;\Varid{f}\;\Varid{a})\;\mathbf{where}{}\<[E]%
\\
\>[3]{}\hsindent{2}{}\<[5]%
\>[5]{}\Conid{HPLeaf}\;\Varid{x}{}\<[16]%
\>[16]{}\equiv {}\<[16E]%
\>[20]{}\Conid{HPLeaf}\;\Varid{y}{}\<[31]%
\>[31]{}\mathrel{=}{}\<[31E]%
\>[34]{}\Varid{x}\equiv \Varid{y}{}\<[E]%
\\
\>[3]{}\hsindent{2}{}\<[5]%
\>[5]{}\Conid{HPNode}\;\Varid{xs}{}\<[16]%
\>[16]{}\equiv {}\<[16E]%
\>[20]{}\Conid{HPNode}\;\Varid{ys}{}\<[31]%
\>[31]{}\mathrel{=}{}\<[31E]%
\>[34]{}\Varid{xs}\equiv \Varid{ys}{}\<[E]%
\\
\>[3]{}\hsindent{2}{}\<[5]%
\>[5]{}\anonymous {}\<[16]%
\>[16]{}\equiv {}\<[16E]%
\>[20]{}\anonymous {}\<[31]%
\>[31]{}\mathrel{=}{}\<[31E]%
\>[34]{}\Conid{False}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The corresponding Horn clause program $\Phi_{HPTree}$ consists of $\Phi_{Pair}$ and the following two clauses :
%\[ \begin{array}{rcl}
%\Phi_2 & = \Phi_1, & |
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\Conid{Mu}\mathbin{:}\Conid{Eq}\;(\Varid{h}\;(\Conid{Mu}\;\Varid{h})\;\Varid{a})\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Varid{h}\;\Varid{a}){}\<[E]%
\\
\>[3]{}\kappa_\Conid{HPTree}\mathbin{:}(\Conid{Eq}\;\Varid{a},\Conid{Eq}\;(\Varid{f}\;(\Varid{a},\Varid{a})))\Rightarrow \Conid{Eq}\;(\Conid{HPTree}\;\Varid{f}\;\Varid{a}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
%\knote{check terminology for loop and cycle throughout}
\noindent The type class resolution for \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} cannot be terminated by cycle
detection. Instead we get a context reduction overflow error in the Glasgow Haskell Compiler, even if we just compare two finite
data structures of the type \ensuremath{\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int}}.
To find a solution to the above problems, % of infinite resolution without cycles,
let us view infinite resolution from
the perspective of coinductive proof in the Calculus of Coinductive Constructions
%. \textit{Calculus of Infinite Construction}.
%Coq implements the \textit{guarded induction principle}
\cite{coquand1994infinite,gimenez1996}.
%\footnote{Following the Curry-Howard tradition, we use the words ``corecursion'' and ``coinduction'' interchangeably in this paper, with ``corecursion'' emphasizing the computational nature and ``coinduction'' emphasizing the reasoning nature.}.
There, in order to prove a proposition $F$ from the assumptions $F_1, .., F_n$,
the proof may involve not only natural deduction and lemmas, but also $F$, provided the use of $F$ is \emph{guarded}.
%by introduction rules.
%the theory of coinductie proofs~\cite{S11}, %, in which, to prove that a formula $A$ is entailed from a program $P$, one has to find an (invariant)
%and in particular to its part concerning coinductive hypothesis formation. %, given by a (possibly different) formula $B$ that implies $A$.
%\frank{The direction of the following sounds good, I think we can also mention how we can actually prove the hypothesis corecursively from the axioms. Even talk about proof term here. Also, It looks like currently the contribution of the paper get mixed into the intro, may be we can talk about our paper in the end of the intro.}
%\knote{It is a choice how you explain this material. I deliberately delayed discussing proof terms, in order to explain them as a separate contribution from coinductive hypothesis formation.
% If there are logic programmers in the PC or among readers -- they may like to hear about the setting without proof terms first.
%As in fact these are potentially two different concerns.
% If there are people interested in Haskell type inference -- they will have the relevant explanation, too
We could say that the existing cycle detection methods treat the atomic formula forming a cycle
as a
\emph{coinductive hypothesis}.
We can equivalently describe the above-explained derivation for $\Phi_{AB}$ in the following terms:
when a cycle with a formula \ensuremath{\Conid{A}\;\Varid{x}} is found in the derivation, $\Phi_{AB}$ gets extended with a coinductive hypothesis $\alpha:\ \ensuremath{\Conid{A}\;\Varid{x}} $.
So to prove \ensuremath{\Conid{A}\;\Varid{x}} coinductively, we would need to apply the clause $\kappa_{A}$ first, and then clause $\kappa_B$, finally apply the coinductive hypothesis.
The resulting proof witness is $\mu \alpha. \ \kappa_A \ (\kappa_B\ \alpha)$.
%, and
%then extending the program $\Phi_P$ with this coinductive hypothesis yeilds finite derivations:
%> kappa^^P : P x => P x
%> alpha : P x
The next logical step we can make is to use the above formalism to extend the syntax of the coinductive hypotheses. %
While cycle detection only uses atomic formulas as coinductive hypotheses, we can try to generalise the syntax of coinductive hypotheses to full Horn formulas.
%, e.g. extending from atomic formulas to full Horn clause formulas, to help us enrich the coinductive reasoning in Horn Clause programs.
%\frank{I reformulate the following para.}
For example, for program $\Phi_Q$, we could prove a lemma
\ensuremath{\Varid{e}\mathbin{:}\Conid{Q}\;\Varid{x}\Rightarrow \Conid{Q}\;(\Conid{S}\;\Varid{x})} coinductively,
which would allow us to form finite derivation for \ensuremath{\Conid{Q}\;(\Conid{S}\;\Conid{Z})}, which is described by $(e \ \kappa_Z)$.
The proof of \ensuremath{\Varid{e}\mathbin{:}\Conid{Q}\;\Varid{x}\Rightarrow \Conid{Q}\;(\Conid{S}\;\Varid{x})} is of a coinductive nature: if we first assume
$\alpha : \ensuremath{\Conid{Q}\;\Varid{x}\Rightarrow \Conid{Q}\;(\Conid{S}\;\Varid{x})}$ and $\alpha_1 : Q \ C$, then all we need to show
is \ensuremath{\Conid{Q}\;(\Conid{S}\;\Conid{C})}.\footnote{Note that here \ensuremath{\Conid{C}} is an eigenvariable.}
To show \ensuremath{\Conid{Q}\;(\Conid{S}\;\Conid{C})}, we apply $\kappa_S$, which gives us \ensuremath{\Conid{Q}\;\Conid{C}}, \ensuremath{\Conid{Q}\;(\Conid{S}\;(\Conid{G}\;\Conid{C}))}. We first discharge \ensuremath{\Conid{Q}\;\Conid{C}}
with $\alpha_1$ and then apply the coinductive hypothesis $\alpha$ which
yields \ensuremath{\Conid{Q}\;(\Conid{G}\;\Conid{C})}, and can be proved with $\kappa_G$ and $\alpha_1$. So we
have obtained a coinductive proof for $e$, which is $\mu \alpha .\lambda
\alpha_1 . \kappa_S\ (\alpha\ (\kappa_G\ \alpha_1))\ \alpha_1$. We can apply
similar reasoning %coinductive
to show that $\Phi_{\ensuremath{\Conid{HPTree}}} \vdash \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} \ \Downarrow (\mu \alpha . \lambda \alpha_1 . \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1\ (\alpha\ (\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)))) \ \kappa_{\ensuremath{\Conid{Int}}}$
using the coinductively proved lemma \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})} \footnote{The proof term can be type-checked with polymorphic recursion.}.
To formalise the above intuitions, we need to solve several technical problems.
%We need to address the following problems in order to effectively automate coinductive reasoning for Horn clause logic.
%\begin{enumerate}
%\item
\textit{1. How to generate suitable lemmas?} We propose to observe a more general notion of a loop invariant than a cycle in the non-terminating resolution. %, and prove the loop invariant coinductively.
In Section \ref{inv} we devise a heuristic method to identify potential loops in the resolution tree and extract \textit{candidate lemmas} in Horn clause form. % for coinductive hypotheses from them.
%This
%loop invariant provides
%insight into obtaining suitable coinductive hypotheses.
\noindent Generally, it is very challenging to develop a practical method for generating
candidate lemmas based on loop analysis, since the admissibility of a loop in reduction is a semi-decidable problem~\cite{zantema1996non}.
%\item
\textit{2. How to enrich resolution to allow coinductive proofs for Horn formulas? and how to formalise the corecursive proof evidence construction?} Coinductive proofs involve not
only applying the axioms, but also modus ponens and generalization. Therefore, the resolution
mechanism will have to be extended in order to support such automation.
\noindent In Section \ref{corec}, we introduce proof relevant \emph{corecursive resolution} -- a calculus that extends the standard resolution rule with two further rules:
one allows us to resolve Horn formula queries, and the other to construct corecursive proof evidence for non-terminating resolution.
%, we
% and corecursive evidence construction. %(called \textit{corecursive resolution}).
%\item
%\textit{What is the corresponce between coinductive evidence and resolution seen as infinite reduction?} %In application such
\emph{3. How to give an operational semantics to the evidence produced by corecursive resolution of Section~\ref{corec}?}
In particular, we need to show the correspondence between corecursive evidence and resolution seen as infinite reduction.
In Section~\ref{ob-equiv}, we prove that for every non-terminating resolution resulting from a \textit{simple loop}, a coinductively provable
candidate lemma can be obtained and its evidence is \textit{observationally equivalent} to the non-terminating resolution process.
\noindent In type class inference, the proof evidence has computational meaning, i.e. the evidence will be run as a program. So the corecursive evidence should be able to recover the original infinite resolution trace.
%This
%correspondence needs to be formally explained
%\end{enumerate}
In Sections~\ref{relwork} and~\ref{fwork} we survey the related work, explain the limitations of our method and conclude the paper.
We have implemented our method of candidate lemma generation based on loop analysis and corecursive
resolution, and incorporated it in the type class inference process of a simple
functional language. %\footnote{Available at: \url{https://github.com/fermat/corecursive-type class}}.
Additional examples %of how our method handles type class inference problems
and implementation information are provided in the extended version. %Appendix \ref{examples}.
%We summarize our main contributions in this paper:
%\begin{itemize}
%\item
%\item
%\item
% \item
%\end{itemize}
% \end{itemize}
% Note that both of these questions had trivial answers when atomic coinductive hypothesis could be generated by cycle detection only.
%> kappa^^f : Q(f(f x )), Q x => Q(f x)
%> kappa^^0 : Q 0
%> kappa^^CH : Q x => Q(f x)
\begin{comment}
\emph{Introducing a method for richer coinductive hypothesis formation for proofs by resolution in Horn clause logic is the first contribution of this paper.}
A heuristic method for the coinductive hypothesis search is introduced in Section~\ref{inv}. Proofs of coinductive soundness of such hypotheses require two extensions to SLD-resolution rule:
\begin{itemize}
\item allowing Horn-Clauses, not just atomic clauses, to be resolvents;
\item introduction of a coinductive inference rule on top of the resolution rule.
Both of these extensuons are given in Section~\ref{corec}.
\end{itemize}
\end{comment}
\begin{comment}
%\frank{Maybe we can somehow merge the type class story as part of the story in the paragraphs before. }
%\knote{Well, up to you. I deliberately seprated the stories, so that the impact of every component is clear. }
Some applications of Horn clause logic and resolution in type inference~\cite{wadler1989make}
require explicit proof-evidence construction.
%In the terminating cases, all we need to record is
%In this paper we use the notation $A_1, ... A_n \Rightarrow B$ for a Horn formula.
%Resolution has been implictly used
In the type class inference in Haskell, a type class can be viewed as an atomic formula and an instance declaration as a Horn formula.
The instance resolution
process
%can then be seen as resolution, with one important requirement:
%the resolution
must compute the evidence for
the type class (i.e. ``construct a dictionary'').
For example, the following declaration
specifies equality class instances for \ensuremath{\Conid{Pair}} and \ensuremath{\Conid{Int}}:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{instance}\;\Conid{Eq}\;\Conid{Int}{}\<[E]%
\\
\>[3]{}\mathbf{instance}\;(\Conid{Eq}\;\Varid{x},\Conid{Eq}\;\Varid{y})\Rightarrow \Conid{Eq}\;(\Varid{x},\Varid{y}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
%The above syntax can be used to model the Haskell type class setting as follows.
%Terms denote Haskell types like |Int| or |(x,y)|, and atomic formulas
%denote Haskell type class constraints on types like |Eq (Int,Int)|.
\noindent Let us represent the instance declarations as a Horn clause program $\Phi_{Pair}$ with the labels indicating the
underlining evidence construction functions:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{17}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\Conid{Int}\mathbin{:}{}\<[17]%
\>[17]{}\Conid{Eq}\;\Conid{Int}{}\<[E]%
\\
\>[3]{}\kappa_\Conid{Pair}\mathbin{:}(\Conid{Eq}\;\Varid{x},\Conid{Eq}\;\Varid{y})\Rightarrow \Conid{Eq}\;(\Varid{x},\Varid{y}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
%construct equality class instance for data |Maybe| and |Int|:
%> instance Eq x => Eq (Maybe x) where ...
%> instance Eq Int where ...
%> kappa^^Maybe :: Eq x => Eq (Maybe x)
%> kappa^^Int :: => Eq Int
\end{comment}
\begin{comment}
\knote{check throughout whether we use => when the body is empty}
\knote{change the below to Pair program}
% logic program instead of $B \leftarrow A_1, ..., A_n$.
When we try to find an instance of the \ensuremath{\Conid{Maybe}} data, the compiler will construct an evidence
for \ensuremath{\Conid{Eq}\;(\Conid{Maybe}\;\Conid{Int})}. This process can be implemented via resolving query \ensuremath{\Conid{Eq}\;(\Conid{Maybe}\;\Conid{Int})} using clauses \ensuremath{\kappa_\Conid{Maybe},\kappa_\Conid{Int}}.
%then produce the corresponding evidence. Thus the evidence in this case is
The constructed evidence is then \ensuremath{(\kappa_\Conid{Maybe}\;\kappa_\Conid{Int})}. It is also called a \emph{dictionary} in the literature, and we will use the two terms interchangeably.
Generally, the disctionary construction for terminating derivations is well-understood in the literature~\cite{wadler1989make}:
the proof-witness terms always take the shape of closed first-order terms, see also an extended discussion of this in~\cite{FuK15}.
We formulate this evidence-producing resolution approach in Section~\ref{preliminary}, in the form of big-step and small-step resolution rules.
However, just like it happens in logic programming, resolution for type classes may diverge.
%It has been noticed, across several different programming languages, that extensions to Hindley-Milner type inference
%may lead to non-terminating derivations by resolution. For example, the issue has been described in Type Class implementations in Haskell~\cite{Lammel:2005}, and
% Featherweight
% Java~\cite{AnconaLagorio11}. In both cases, a loop-detection mechanism is used to terminate diverging cases coinductively.
%\knote{Fu Peng, please double-check me. Also, I am not sure how to make mu appear as Greek letter...}
We note that here, the process of coinductive hypothesis formation is the same as in CoLP, as the coinductive hypothesis is still given by an invariant atomic formula.
But the interesting feature to notice is that now the proof-witness term is no longer a closed first-order term, but a $\lambda$-expression with fixed point.
%Cycle detection method has been one of the most widely accepted in resolution literature, being employed in several areas,
%from Type class resolution~\cite{Lammel:2005,AnconaLagorio11} to the coinductive variant of Prolog CoLP~\cite{SimonBMG07}.
\end{comment}
\begin{comment}
%\begin{comment}
Mathematical induction is pervasive in programming and program
verification. It arises in data definitions (e.g., it describes some
algebraic data structures), it underlies program semantics (e.g., it
explains how to reason about finite iteration and recursion), and it
gets used in proofs (e.g., it supports lemmas about data structures
used in inductive proofs).
%Whereas induction deals with finite things (data, behavior, etc.),
%its dual, co-induction, deals with possibly infinite things.
Coinduction, too, is important in programming and program
verification. It arises in infinite data definitions (e.g., lazily
defined infinite streams), semantics (e.g., of concurrency), and
proofs (e.g., of observational equivalence, or bisimulation, of
potentially infinite processeit supports lemmas about infinite data structures). It is thus desirable to have good
support for both induction and coinduction in systems for reasoning
about programs.
The first implementations of coinduction were pioneered in
%total functional programming (FP),
interactive theorem proving (ITP) \cite{Gimenez98}, and the coinductive methods are just
finiding their way into automated theorem proving (ATP)~\cite{LeinoM14,ReynoldsB15,SimonBMG07}.
where the duality
of inductive and coinductive methods was achieved by distinguishing
inductive from coinductive types, recursive functions consuming inputs
of inductive types from corecursive functions producing outputs of
coinductive types, and methods for constructing inductive proofs from
those for constructing coinductive proofs.
%\end{comment}
Recently, the rapid development of automated theorem proving (ATP) in
general, and SAT/SMT solvers in particular, has opened the way to
introducing induction and coinduction to ATP
\cite{LeinoM14,ReynoldsB15,SimonBMG07}.
%and thus to bridging the
%previously existing gap between coinductive methods in ITP and ATP.
%Some coinductive methods of ITP can be easily translated to ATPs. For
%example, definitions of (inductive and) coinductive types in ITP translate
%naturally into
%first-order
%fixed-point definitions in ATP.
%However, some coinductive methods in
%ITP are much trickier to adapt to ATP. In particular, the process of coinductive hypothesis formation and of productivity of a coinductive proof is
%not as well understood in ATP as in ITP.
%ATP being pervasive in programming language design, e.g. via type inference, limitations of coinductive methods in ATP actually affect a much wider range
%of languages.
%To illustrate these two points,
%SLD-resolution in logic programming.
%consider, as an example, coinductive proofs for Horn clause logic (or Logic Programming (LP)).
%In this paper, we will focus on this problem, while taking first-order Horn caluses and first-order resolution
%as the target ATP paradigm, in which we consider the problem of identifying richer coinductive proof-methods.
%We use Type class instance resolution as the main running example and target application of the methods we propose here.
For example, the following logic program $P_1$ corresponds to the above type class inference problem:
%Let us, for the time being, think of $p$ as some abstract property and even and odd -- as two abstract function symbols.
%Our interest at the moment lies in the infinite derivations these two clauses give rise to.
For a query $eq(odd(int))$, SLD-resolution will give rise to an infinite derivation:
$\underline{\mathtt{eq(odd(int))}} \leadsto \mathtt{eq(even(int))} \leadsto \underline{\mathtt{eq(odd(int))}} \leadsto \ldots$
%State-of-the-art methods of coinductive resolution in coinductive logic programming, such as (CoLP)~\cite{SimonBMG07}, use
The loop detection method of CoLP will find a repeating resolvent
(e.g. $p(odd(int))$) and will close this derivation coinductively. The first occurence of the repeating formula is seen as a coinductive hypothesis, and the second -- as a coinductive conclusion.
% A similar
%loop detection method is employed for type class inference in the
%Glasgow Haskell Compiler (GHC)~\cite{Lammel:2005}, and CoLP is itself
%used for type class inference in Featherweight
%Java~\cite{AnconaLagorio11}.
%Thanks to cycle detection of ~\cite{Lammel:2005}, the resolution for \texttt{Eq (OddList Int)} in Haskell
%terminates and yields a recursive dictionary as witness. This type class inference problem corresponds exactly to the SLD-derivation for \texttt{eq(odd(int))}
%and program $P_1$ shown earlier.
\end{comment}
\begin{comment}
\knote{check we are consistent with numbering to $\Phi$ and that we use either :: or : but not a mixture in Horn clauses}
Trying to derive e.g. \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} will result in a diverging derivation, which at the same time will not exhibit a detectable cycle.
By earlier discussion, we can guess that introducing a richer coinductive hypothesis, e.g. \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})} will help to solve the problem.
\emph{Applying our new method of richer coinductive hypothesis formation in Type Class inference is the second contribution of this paper}.
There is one last problem left to solve: in order to implement such coinductive reasoning in Haskell Type classes,
we must also devise a method that soundly constructs a recursive proof-witness for the derivations involving
such coinductive proofs. This problem requires care, as there are several functional-logic features that come into play together here:
richer (Horn clause) coinductive hypothesis formation on the ``logic'' side, and the corresponding $\lambda$/$\mu$- proof-terms on the ``functional'' side.
Our third contribution in this paper is \emph{the introduction of a general functional-logic calculus for corecursive resolution,
in which Horn clauses are seen as types, and proof-witnessing terms as inhabitants of those types}.
The general idea of type-theoretic approach to resolution in Horn clause logic has been presented in~\cite{FuK15}, but was formulated only for terminating
derivations. In Section~\ref{corec} , we extend this idea with the calculus that constructs the recursive proof evidence for coinductive proofs, thereby
reflecting the above-explained extensions to the syntax of Horn-clause resolution.
%\begin{itemize}
% \item extends the resolution rule with coinductive rule; %, in order to construct coinductive proofs;
% \item enriches the resolution rule to handle Horn-clause goals, not just atomic goals, in order to prove coinductive hypotheses in the form of Horn clauses;
% \item
%\end{itemize}
\end{comment}
\begin{comment}
Finally, in Section~\ref{ob-equiv}, we show...
\knote{Tom, Fu Peng, -- can you give 2 sentences here?}
The new calculus for coinductive proofs by resolution introduced in Section~\ref{corec}
can be seen as a general-purpose functional-logic automated prover on its own right,
surpassing the two application areas of coinductive logic programming and type class resolution.
%It shows the strength of the functional-logic approach to automated proofs: by combining together the
%methods of first-order Horn clause resolution, simply-typed $\lambda$-calculus, and the theory of coinductive proofs,
%the overall
%(meta-) contribution of this paper is
%the resulting
%calculus can be
%inter-disciplinary framework for enriched automated proofs with Horn-clause goals, coinduction and proof-witness construction.
%As such, it generalises the state-of-the-art both in logic programming and type class resolution.
\knote{Do we want to give some name to this "calculus''? In SEction 4, we call it ``Corecursive resolution'', in the intro, we motivate it from perspective of coinductive proofs --
perhaps a fixed name would help, -- same name could give the title to the paper
}
We conclude the paper by discussing related work in Section~\ref{relwork} and future work in Section~\ref{fwork}.
Implementation of the corecursive resolution calculus, heuristic method for coinductive hypothesis search, as well as implementation of and of several
examples of type class inference are available here: \url{link!}.
\end{comment}
\begin{comment}
%There are, however, cases of non-terminating resolution that cannot be handled by simple loop detection. And again, this problem spans over several application areas of first-order resolution.
Consider the following example of the \texttt{Eq} type class instance resolution in Haskell: %, and in particular instantiating it with type \texttt{Int}:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{data}\;\Conid{PTree}\;\Varid{a}\mathrel{=}\Conid{PLeaf}\;\Varid{a}\mid \Conid{PNode}\;(\Conid{PTree}\;(\Conid{Pair}\;\Varid{a}\;\Varid{a})){}\<[E]%
\\[\blanklineskip]%
\>[3]{}\kappa_\Conid{PTree}\mathbin{::}(\Conid{Eq}\;\Varid{a},\Conid{Eq}\;(\Conid{PTree}\;(\Conid{Pair}\;\Varid{a}\;\Varid{a}))\Rightarrow \Conid{Eq}\;(\Conid{PTree}\;\Varid{a}){}\<[E]%
\\
\>[3]{}\kappa_\Conid{Pair}\mathbin{::}(\Conid{Eq}\;\Varid{a},\Conid{Eq}\;\Varid{b})\Rightarrow \Conid{Eq}\;(\Conid{Pair}\;\Varid{a}\;\Varid{b}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
In Haskell, the resolution of \texttt{Eq (DList Int)} requires the resolution of \texttt{Eq
(DList (DList Int))}, which requires the resolution of \texttt{Eq (DList (DList
(DList Int)))} and so on.
In LP, this example would correspond to
program $P_2$ below:\\ % could be seen as a case of mixed inductive-coinductive definition:
$0.\ \mathtt{eq (d(X))} \gets \mathtt{eq(X), eq(d( d (X)))}$\\
$1. \ \mathtt{eq(int)} \gets $.
Likewise, program $P_2$ will give rise to infinite derivations in CoLP:
$\mathtt{eq(d(int))} \leadsto \mathtt{eq(int), eq(d( d (int)))} \leadsto \mathtt{eq(d( d (int)))} \leadsto $ \\$ \mathtt{eq(d(int)), eq(d(d(d(int))))} \leadsto
\mathtt{eq(int), eq(d( d (int))), eq(d(d(d(int))))} \leadsto \ldots$
Here, cycle detection will not help, as there will be a derivation branch
$\mathtt{eq(d(int))} \leadsto \mathtt{ eq(d( d (int)))} \leadsto \mathtt{eq(d(d(d(int))))} \leadsto \ldots$
that does not exhibit a cycle.
These few examples illustrate that, in order to make further progress with richer cases of
corecursive computations by resolution, we must first establish a more general understanding
of the coinductive proof principles for resolution, and in particular the methods of formation of coinductive hypotheses.
In order to develop and implement this method, we have to introduce several new methods. Firstly, we still need to
%Ultimately, there would be cases when coinductive hypotheses will require a richer syntax than that of a Horn clause, and we leave such cases as a future work.
answer the question (ii). % is a harder question to answer; and we will present one possible method in the next few sections.
In Section~\ref{inv}, we introduce a heuristic method for generating the coinductive hypotheses, by observing invariant patterns in a resolution tree arising from a given
query. In Section~\ref{corec}, we introduce a method that proves the generated coinductive lemmas coinductively sound.
Finally, in order to apply these methods in type class resolution in Haskell, we develop, in Sections~\ref{}, a method for viewing derivations by resolution
through the prism of simply-typed $\lambda-$calculus.
It has been noticed by Girard~\cite{Girard:1989}, that resolution rule $\frac{A \lor B \ \ \ \neg B \lor D}{A \lor D}$ can be expressed by means of
the cut rule in intuitionistic sequent calculus:
$\frac{A \Rightarrow B \ \ \ B \Rightarrow D}{A \Rightarrow D}$.
Although the resolution rule is classically equivalent to the cut rule,
the cut rule is better suited for performing computation
and at the same time preserving constructive content. In Section\ref{} we present
a type system reflecting this intuition: if $p_1$ is a proof of $A \Rightarrow B$ and $p_2$ is a proof of $B \Rightarrow D$, then $\lambda x . p_2\ (p_1\ x)$ is a proof of $A \Rightarrow D$. Thus, a proof can be recorded alongside with each cut rule.
*For Fu Peng to tie it up with dictionary construction... Perhaps re-phrase the above*
*Check all sections are accounted for once we are done*
*Also, make sure to explain the difference between the STLC used here and the one introduced in our LOPSTR15 paper*
%This methos involves a
%simply typed lambda calculus formulation of resolution, extending~\cite{DBLP:journals/corr/FuK15} with a coinductive rule.
%Apart from answering the questions (i) and (ii) in the positive, the third contribution of this paper is in
%systematic adaptation of the method that was first introduced in~\cite{DBLP:journals/corr/FuK15} and allows a type-theoretic approach to resolution.
%It views Horn clauses as types. Type inhabiatants
% are the terms representing the proof strategy applied in the derivation.
%As we take Haskell type class resolution to be the main motivation and source of examples here,
%we make the full use of this idea of proof-evidence construction and connect it to the methods of dictionary construction in Haskell Type Class resolution.
% However, it is a mere coincidence that works only in simple cases. The Coq proof shown above in fact
%includes several consistency chceks. The first one is checking that coinductive hypothesis (\texttt{cofix CH}) is taken on an object of coinductive type. This is in correspondence of marking predicates as coinductive in CoLP. Next, it checks that the application of this hypothesis in the lasrt line of the proof is guarded by application of constructors
%of coinductive type \texttt{p} to the subgoal that gives rise to \texttt{CH}. This kind of guardedness guarantee is very hard to formulate (let alone give) in first-order resolution setting. This first limitation is due to the absence of proper notion of types and type constructors in Horn clause programming.
%The second facility that is present in Coq but absent in CoLP is the ability to form a more complex coinductive hypothesis within a proof.
Haskell's type class mechanism was initially conceived to provide a structured
approach to adhoc overloading. However, over the years and aided by various
extensions they have exceeded this initial scope to become a powerful mechanism
for type-directed computation and implicit code generation.
The standard implementation of type classes consists of two phases. \emph{At compile
time}, the type checker derives a so-called type class constraint for every use
of a type class method. Such a constraint is in fact a proof obligation that
is discharged by means of resolution against Horn clauses that come in the form of
type class instances. The type checker distills witnesses from the proofs in the form
of function dictionaries. These dictionaries are passed \emph{at runtime} to provide
implementations for the overloaded type class methods.
Of course it is essential that the resolution process, and thus the compiler,
terminates. To ensure this property stringent conditions have been
imposed on type class instances~\cite{SulzmannDJS07}. Unfortunately, these were found
to be overly restrictive as they rule out many interesting applications.
% For instance, L\"ammel and Peyton Jones \cite{Lammel:2005} argue the
% neccessity for loosening these conditions in their approach to generic
% programming.
Hence, the GHC Haskell compiler provides various language extensions (e.g.,
{\tt UndecidableInstances} and {\tt FlexibleContexts}) to lift the stringent
conditions. With these extensions type inference is no longer guaranteed to
terminate and becomes the programmer's responsability.
In order to relax a little the termination requirement and to support their
approach to datatype-generic programming, L{\"a}mmel and Peyton
Jones~\cite{Lammel:2005} have adapted the type class resolution mechanism to
permit cycles. Consider the following mutually recursive definitions of even
and odd lists and their \texttt{Eq} type class instances.
\begin{tabbing}\tt
~~~~~data~OddList~a~~~\char61{}~~Nil~\char124{}~OCons~a~\char40{}EvenList~a\char41{}\\
\tt ~~~~~data~EvenList~a~~\char61{}~~ECons~a~\char40{}OddList~a\char41{}\\
\tt ~\\
\tt ~~~~~instance~\char40{}Eq~a\char44{}~Eq~\char40{}EvenList~a\char41{}\char41{}~\char61{}\char62{}~~Eq~\char40{}OddList~a\char41{}~where\\
\tt ~~~~~~~Nil~~~~~~~~~\char61{}\char61{}~~Nil~~~~~~~~~~\char61{}~~True\\
\tt ~~~~~~~OCons~x~xs~~\char61{}\char61{}~~OCons~y~ys~~~\char61{}~~x~\char61{}\char61{}~y~\char38{}\char38{}~xs~\char61{}\char61{}~ys\\
\tt ~~~~~~~\char95{}~~~~~~~~~~~\char61{}\char61{}~~\char95{}~~~~~~~~~~~~\char61{}~~False\\
\tt ~\\
\tt ~~~~~instance~\char40{}Eq~a\char44{}~Eq~\char40{}OddList~a\char41{}\char41{}~\char61{}\char62{}~Eq~\char40{}EvenList~a\char41{}~where\\
\tt ~~~~~~~ECons~x~xs~~\char61{}\char61{}~~ECons~y~ys~~~\char61{}~~x~\char61{}\char61{}~y~\char38{}\char38{}~xs~\char61{}\char61{}~ys\char58{}
\end{tabbing}
Thanks to cycle detection the resolution of \texttt{Eq (OddList Int)}
terminates and yields a recursive dictionary as witness.
Yet, in more advanced scenarios, cycle detection is not strong enough to obtain
termination. Indeed, consider the following datatype and equality instance:
\begin{tabbing}\tt
~~~~~data~DList~a~\char61{}~Nil~\char124{}~Cons~a~\char40{}DList~\char40{}DList~a\char41{}\char41{}\\
\tt ~\\
\tt ~~~~~instance~\char40{}Eq~a\char44{}~Eq~\char40{}DList~\char40{}DList~a\char41{}\char41{}\char41{}~\char61{}\char62{}~Eq~\char40{}DList~a\char41{}~where\\
\tt ~~~~~~~Nil~~~~~~~\char61{}\char61{}~Nil~~~~~~~~~~\char61{}~True\\
\tt ~~~~~~~Cons~x~xs~\char61{}\char61{}~Cons~y~ys~~~~\char61{}~x~\char61{}\char61{}~y~\char38{}\char38{}~xs~\char61{}\char61{}~ys\\
\tt ~~~~~~~\char95{}~~~~~~~~~\char61{}\char61{}~\char95{}~~~~~~~~~~~~\char61{}~False
\end{tabbing}
The resolution of \texttt{Eq (DList Int)} requires the resolution of \texttt{Eq
(DList (DList Int))}, which requires the resolution of \texttt{Eq (DList (DList
(DList Int)))} and so on. The process diverges without cycling. In other words, the
type checker does not terminate.
In this paper we address the above divergence issue. We show that there is a
perfectly reasonable corecursive dictionary that witnesses the \texttt{DList}
proof obligation. Moreover, we provide a general resolution mechanism, based on the techniques for co-inductive
proof search introduced by Fu and Komendantskaya
\cite{DBLP:journals/corr/FuK15} and Komendantskaya \etal
\cite{KomendantskayaEtAl15}, that derives the witness in finite time. Key to our approach is to infer
a co-inductive hypothesis, e.g., in the case of the \texttt{DList} example, we infer:
$$
\texttt{Eq a => Eq (DList a)}
$$
which we use to discharge the constraint {\tt Eq (DList (DList (DList
a)))}.
% But our work is not limited to a simple extension of the GHC type
% checker. In order to introduce our extension we formulate a novel {a what?
% description?} of type checking process. We separete the work carried out in the
% inner loop of the constraint solver
Specifically, our contributions are:\todo{reformulate contributions}
\begin{itemize}
\item We separate the concerns of type checker in the simplification
phase into three stages; we identify co-inductive invariant
search, co-inductive hypothesis synthesis; and hypothesis proof.
\item We describe a new technique for each of the stages that is
improving existing technology.
\item We combine the presented techniques such that type checing is
sound and terminating as opposed to the previous
state-of-the-art where the termination is not guaranteed.
\end{itemize}
\end{comment}
%The related work is discussed in the Section \ref{relwork}.
% \item Paterson conditions\cite{SulzmannDJS07}:
% \todo{Are there any other conditions implied by the language standard?}
% \begin{itemize}
% \item The context C of a class declaration can mention only type
% variables, not type
% constructors, and in each individual class constraint CC all the
% type variables
% are distinct
% \item For each declaration instance $C \Rightarrow TC \; t_1 \ldots t_n$:
% \begin{itemize}
% \item No variable has more occurrences in a type class
% constraint in the context $C$ than the head
% $TC \; t_1 \ldots t_n$.
% \item Each type class constraint in the context C has
% fewer constructors and
% variables (taken together counting repetitions) than the
% head.
% \end{itemize}
% \item The instance declarations must not overlap. That is, for
% any two instances declarations instance
% $C \Rightarrow TC \; t_1 \ldots t_n$ and instance
% $C_0 \Rightarrow TC t'_1 \ldots t'_n$
% there is no substitution $\phi$ such that
% $\phi(t_1) = \phi(t'_1),\ldots,\phi(t_n) = \phi(t'_n)$.
% \end{itemize}
%\input{overviewK}
%%include overviewK.tex
%===============================================================================
%\section{Overview}
%\label{overview}
%%include overview.lhs
%===============================================================================
\begin{comment}
\section{Old Overview}
\knote{I have started to clean up formatting and grammar. E.g. citations were given inconsistently with and without spaces}
Type class and its extensions~\cite{wadler1989make,kaes1988parametric,jones2003qualified}, have found many useful applications, describing monad~\cite{peyton1993imperative},
implementing quickcheck~\cite{claessen2011quickcheck}. It is very desirable to construct all the evidences at compile time,
\knote{desirable for whom? do something with this sentence}
and report unconstructable evidence as error. To achieve
this while maintaining reasonable flexiblity requires a lot of
careful considerations on the syntactic form of instance declaration and the evidence construction process. The subtleties of the issues and design decisions of
type class in Haskell are well documented in \cite{Jones97}. For example, Haskell 98 imposes the restriction that each instance declaration must be obviously terminates,
\knote{firstly -- grammar: do you mean ``must obvioulsy terminate''? but obviously is a strange term in this context... ``Should be structurally terminating''?}
i.e. for each instance declaration \texttt{C1, ..., Cm => H},
the \texttt{Ci} must be of the form \texttt{C a1 ... an}, where \texttt{ai} are type variables. With all the good intentions of this restriction, sometimes these restrictions still gets in the way of programming,
\knote{what does it mean -- ``get on the way of programming''? -- reformulate}
for example, a declaration \texttt{Eq a, Eq (List (Tree a)) => Eq (Tree a)} will be banned
\knote{what does it mean banned? rejected by compiler? -- be precise}
even though it looks like a natural declaration for equality class for
the type \texttt{data Tree a = Node a (List (Tree a))}. There are extensions that aim to relax some part of the Haskell 98 requirements and to extend the evidence construction mechanism to support circular evidence, the following is an example (From \cite{Lammel:2005}).
{\footnotesize
\begin{tabbing}\tt
~instance~Data~SizeD~t~\char61{}\char62{}~Size~t~where~\char46{}\char46{}\char46{}\\
\tt ~instance~Sat~\char40{}cxt~Char\char41{}~\char61{}\char62{}~Data~cxt~Char~where~\char46{}\char46{}\char46{}\\
\tt ~instance~Size~t~\char61{}\char62{}~Sat~\char40{}SizeD~t\char41{}~where~\char46{}\char46{}\char46{}
\end{tabbing}
}
\noindent If we want to see whether the evidence of \texttt{Size Char} is constructable, we
need to make sure evidence for \texttt{Data SizeD Char} is constructable, which requires
evidence for \texttt{Sat (SizeD Char)}, which requires \texttt{Size Char}. Now we are back
to where we started.
\knote{back where we started is confusing -- as it makes one feel we have made a circle in argumentation, but that is in fact a cycle in inference... }
In \cite{Lammel:2005}, evidence construction process is extended with cycle
aware mechanism. The evidence to be constructed is assumed to be already given, and
the construction process proceeds as usual, possibly using the assumed ``hypothesis'' coinductively.
\knote{changed the half sentence above, -- check me if ok?}
In the example above, the evidence of \texttt{Size Char} will be assumed already given, when the evidence construction process reach \texttt{Size Char} again, the construction process will terminate and construct a circular evidence (the knot is tied)\footnote{This approach is implemented by GHC(Glasgow Haskell Compiler) in the \texttt{UndecidableInstances} flag. }.
\begin{figure}[htbp]
\makebox[\textwidth]{\hrulefill}{
\footnotesize
\begin{tabbing}\tt
~data~Comp~f~g~a~\char61{}~Comp~\char40{}f~\char40{}g~a\char41{}\char41{}\\
\tt ~data~Pair~a~\char61{}~Pair~a~a\\
\tt ~data~GSeqF~a~r~\char61{}~Nil~\char124{}\char124{}~Cons~a~r\\
\tt ~data~Fix~f~g~\char61{}~Fix~\char40{}f~\char40{}Fix~\char40{}Comp~g~f\char41{}~g\char41{}\char41{}\\
\tt ~\\
\tt ~instance~Eq~\char40{}\char41{}~where~\char46{}\char46{}\char46{}\\
\tt ~instance~Eq~\char40{}f~\char40{}g~a\char41{}\char41{}~\char61{}\char62{}~Eq~\char40{}Comp~f~g~a\char41{}~where\\
\tt ~~~Comp~s~~\char61{}\char61{}~~Comp~t~~\char61{}~~s~\char61{}\char61{}~t\\
\tt ~\\
\tt ~instance~Eq~a~\char61{}\char62{}~Eq~\char40{}Pair~a\char41{}~where\\
\tt ~~~Pair~x1~y1~~\char61{}\char61{}~~Pair~x2~y2~~\char61{}~~x1~\char61{}\char61{}~x2~\char38{}\char38{}~y1~\char61{}\char61{}~y2\\
\tt ~\\
\tt ~instance~\char40{}Eq~a\char44{}~Eq~r\char41{}~\char61{}\char62{}~Eq~\char40{}GSeqF~a~r\char41{}~where\\
\tt ~~~Nil~~~~~~~~\char61{}\char61{}~~Nil~~~~~~~~\char61{}~~True\\
\tt ~~~Cons~x~xs~~\char61{}\char61{}~~Cons~y~ys~~\char61{}~~x~\char61{}\char61{}~y~\char38{}\char38{}~ys~\char61{}\char61{}~ys\\
\tt ~~~\char95{}~~~~~~~~~~\char61{}\char61{}~\char95{}~~~~~~~~~~~\char61{}~~False\\
\tt ~\\
\tt ~instance~Eq~\char40{}f~\char40{}Fix~\char40{}Comp~g~f\char41{}~g\char41{}\char41{}~\char61{}\char62{}~Eq~\char40{}Fix~f~g\char41{}~where\\
\tt ~~~Fix~s~~\char61{}\char61{}~~Fix~t~~\char61{}~~s~\char61{}\char61{}~t\\
\tt ~\\
\tt ~test~\char61{}~Fix~\char40{}Cons~\char40{}\char41{}~\char40{}Fix~\char40{}Comp~\char40{}Pair~Nil~Nil\char41{}\char41{}\char41{}\char41{}~\char61{}\char61{}~Fix~Nil
\end{tabbing}
\footnotesize
\hrulefill}
\caption{Equality instances for a generic multi-way tree}
\label{fig:ex1}
\end{figure}
Unfortunitely, circularity is just one way for the evidence construction to be diverging,
\knote{diverging occurs for the first time here. If different from non-termination -- explain how, if not different -- just use non-termination consistently }
there are nontrivial code that will result in divergent without forming any cycle.
\knote{I do not understand that sentence as given}
Fig. \ref{fig:ex1} is a generic definition of multi-way trees where every node at level $n$ has $0$ or $2^n$ subtrees. The instance declarations is what one would write given the data type declarations. However, the function \texttt{test} will make the type checker diverge, since it gives rise to the constraint \texttt{Eq (Fix (GSeqF ()) Pair)}, which has the following context reduction trace:
\knote{check the above sentence: again diverge versus never terminate, does test on its own gives divergence? in which sense \texttt{Eq (Fix (GSeqF ()) Pair)} is a constraint? do you really want to call it a constriant -- then this needs some semi-formal explanation... }
\begin{center}
{\footnotesize
\noindent $\{\texttt{Eq (Fix (GSeqF ()) Pair)}\} \to^* \{\texttt{Eq (Fix (Comp Pair (GSeqF ())) Pair)}\} \to^* \{\texttt{Eq (Fix (Comp Pair (Comp Pair (GSeqF ()))) Pair)}\} \to^* ... $
}
\end{center}
\noindent We can see the constraint is periodically increased by \texttt{(Comp Pair)}. But if we look at the definition of \texttt{test}, it is comparing two finite data, we would want it to be type checked and evaluated to \texttt{False}!
Internally, \texttt{test} is represented as:
{\footnotesize
\noindent \texttt{test = (==) d (Fix (Cons () (Fix (Comp (Pair Nil Nil))))) (Fix Nil)}
}
\noindent where \texttt{d} is some corecursive evidence that is used finitely by the context
\noindent \texttt{ (==) * (Fix (Cons () (Fix (Comp (Pair Nil Nil))))) (Fix Nil)}. The divergent of GHC in this case means the compiler can not construct such corecursive evidence.
\end{comment}
%===============================================================================
\section{Preliminaries: Resolution with Evidence}
\label{preliminary}
This section provides a standard formalisation of resolution with evidence
together with two derived forms: a
\emph{small-step} variant of resolution and a reification of resolution in a
resolution tree.
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
%\paragraph{Syntax and Notation}
We consider the following syntax.
\begin{definition}[Basic syntax]
{\small
\[\begin{array}{l@{\hspace{5mm}}l@{\hspace{5mm}}c@{\hspace{5mm}}l}
\text{Term} & t \ & ::= & \ x \ | \ K\ | \ t\ t' \\
\text{Atomic Formula} & A, B, C, D\ & ::= & \ P\ t_1 \ ...\ t_n \\
\text{Horn Formula} & H \ & ::= & \ B_1,..., B_n \Rightarrow A \\
\text{Proof/Evidence} & e \ & ::= & \ \kappa \ |\ e \ e' \\
\text{Axiom Environment} & \Phi \ & ::= & \cdot \ | \ \Phi, (\kappa : H)
\end{array} \]}
\end{definition}
We consider first-order applicative terms, where $K$ stands for some
constant symbol. Atomic formulas are predicates
on terms, and Horn formulas are defined as usual. We assume that
all variables $x$ in Horn formulas are implicitly universally quantified.
There are no \textit{existential variables} in the Horn formulas, i.e.,
$\bigcup_i \mathrm{FV}(B_i) \subseteq \mathrm{FV}(A)$ for $B_1,\ldots,B_n
\Rightarrow A$.
The axiom environment $\Phi$ is a set of Horn formulas labelled with distinct
evidence constants $\kappa$. Evidence terms $e$ are made of evidence
constants $\kappa$ and their applications. Finally,
we often use $\underline{A}$ to abbreviate $A_1,..., A_n$ when the number $n$ is
unimportant.
% We assume that the heads of the Horn clauses in
% $\Phi$ are non-overlapping.
%% \knote{This example came back:}
%% \frank{I have move this back to intro. I think there is a place for this in intro.}
%\frank{I think the following paragraph can be explained in the intro.}
The above syntax can be used to model the Haskell type class setting as follows.
Terms denote Haskell types like \ensuremath{\Conid{Int}} or \ensuremath{(\Varid{x},\Varid{y})}, and atomic formulas
denote Haskell type class constraints on types like \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})}. Horn formulas
correspond to the type-level information of type class instances. % like:
%\knote{the eaxmple is gone to the intro}
%> instance Eq Int
%> instance (Eq x, Eq y) => Eq (x,y)
Our evidence $e$ models type class dictionaries, following Wadler and Blott's
dictionary-passing elaboration of type classes \cite{wadler1989make}. In particular the constants
$\kappa$ refer to dictionaries that capture the term-level information of type
class instances, i.e., the implementations of the type class methods. Evidence
application $(e\ e')$ accounts for dictionaries that are parametrised by other
dictionaries. Horn formulas in turn represent type class instance
declarations. The axiom environment $\Phi$ corresponds to Haskell's global
environment of type class instances. Note that the treatment of type class instance declaration
and their corresponding evidence construction here
are based on our own understanding of many related works (\cite{Jones97,jones2003qualified}), which are also discussed in Section \ref{relwork}.
% For instance, based on the above two instances
% we have:
%\[ \Phi_{|Pair|} = |kInt : Eq Int|, |kPair : (Eq x, Eq y) => Eq (x,y)| \]
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
%\paragraph{Resolution}
In order to define resolution together with evidence generation, we use resolution judgement $\Phi \vdash A \Downarrow e$ to state that the
atomic formula $A$ is entailed by the axioms $\Phi$, and that the proof
term $e$ witnesses this entailment. It is defined by means of the following
inference rule.
\begin{definition}[Resolution]\label{def:resolution}
\fbox{$\Phi \vdash A \Downarrow e$}
\label{context-red}
{\small
\[\begin{array}{c}
\infer[\text{if}~(\kappa : B_1,..., B_n \Rightarrow A) \in \Phi]
{\Phi \vdash \sigma A \Downarrow \kappa~e_1 \cdots e_n}
{ \Phi \vdash \sigma B_1 \Downarrow e_1 \quad \cdots \quad \Phi \vdash \sigma B_n \Downarrow e_n
}
\end{array}
\]}
\end{definition}
% To model context reduction in type classes, we introduce the following reduction rule, where
% $S$ is a set of atomic formulas.
% \begin{definition}[Resolution]
% \fbox{$\Phi \vdash S \to_\kappa S'$}
% \label{context-red}
% \[\begin{array}{c}
% \infer
% {\Phi \vdash S \uplus \{ A'\} \to_\kappa S \cup \{\sigma A_1,..., \sigma A_m\}}
% {(\kappa : A_1,..., A_m \Rightarrow A) \in \Phi \quad\quad A \mapsto_{\sigma} A'}
% \end{array}
% \]
% \end{definition}
Using this definition we can show $\Phi_{\ensuremath{\Conid{Pair}}} \vdash \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})} \Downarrow \ensuremath{\kappa_\Varid{Pair}\;\kappa_\Varid{Int}\;\kappa_\Varid{Int}}$.
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
%\paragraph{Small-Step Resolution}
In case resolution is diverging, it is often more convenient to consider
a \emph{small-step} resolution judgement (in analogy to the small step
operational semantics) that performs one resolution step at a time and allows
us to observe the intermediate states.
The basic idea is to rewrite the initial query $A$ step by step into its
evidence~$e$. This involves \emph{mixed terms} on the way that consist partly
of evidence, and partly of formulas that are not yet resolved.
\begin{definition}[Mixed Terms]
{\small
\[\begin{array}{l@{\hspace{5mm}}l@{\hspace{5mm}}c@{\hspace{5mm}}l}
\text{Mixed term} & q \ & ::= & \ A \ |\ \kappa \ | \ q \ q' \\
\text{Mixed term context} & \mathcal{C} \ & ::= & \ \bullet \ | \ \mathcal{C}\ q \ | \ q\ \mathcal{C}\\
\end{array}
\]}
\end{definition}
At the same time we have defined mixed term contexts $\mathcal{C}$ as mixed
terms with a hole $\bullet$, where $\mathcal{C}[q]$ substitutes the hole with $q$ in the usual way.
% TOM: The syntax does not admit multiple holes. Do we need that feature?
% The notation $\mathcal{C}[q_1, ..., q_n]$ means replacing the holes in
% $\mathcal{C}$ from left to right with $q_1, ..., q_n$. We conveniently remove
% duplications in this representation, i.e. $\mathcal{C}[D, D]$ will be
% represented as $\mathcal{C}[D]$. We write $\kappa\ \underline{q}$ to mean
% $(...((\kappa\ q_1)...)\ q_n)$.
\begin{definition}[Small-Step Resolution]
\fbox{$\Phi \vdash q \rightarrow q'$}
\label{context-red}
{\small
\[\begin{array}{c}
\infer[\text{if}~(\kappa : \underline{B} \Rightarrow A) \in \Phi]
{\Phi \vdash \mathcal{C}[\sigma A] \rightarrow \mathcal{C}[\kappa~\sigma\underline{B}]}
{ }
\end{array}
\]}
\end{definition}
For instance, we resolve \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})} in three small
steps: $\Phi_{\ensuremath{\Conid{Pair}}} \vdash \ensuremath{\Conid{Eq}\;(\Conid{Int},\Conid{Int})} \rightarrow \ensuremath{\kappa_\Varid{Pair}\;(\Conid{Eq}\;\Conid{Int})\;(\Conid{Eq}\;\Conid{Int})}$,
$\Phi_{\ensuremath{\Conid{Pair}}} \vdash \ensuremath{\kappa_\Varid{Pair}\;(\Conid{Eq}\;\Conid{Int})\;(\Conid{Eq}\;\Conid{Int})} \rightarrow \ensuremath{\kappa_\Varid{Pair}\;\kappa_\Varid{Int}\;(\Conid{Eq}\;\Conid{Int})}$ and
$\Phi_{\ensuremath{\Conid{Pair}}} \vdash \ensuremath{\kappa_\Varid{Pair}\;\kappa_\Varid{Int}\;(\Conid{Eq}\;\Conid{Int})} \rightarrow \ensuremath{\kappa_\Varid{Pair}\;\kappa_\Varid{Int}\;\kappa_\Varid{Int}}$.
We write $\Phi \vdash q \to^{*} q'$ to denote the transitive closure of
small-step resolution.
% The term rewrite system $K(\Phi)$ that mimics resolution against axioms $\Phi$ is defined
% as follows.
% \begin{definition}[Induced Term Rewrite System]
% \label{label}
% For each $(\kappa : \underline{A} \Rightarrow B) \in \Phi$, we
% have $(B \to \kappa \ \underline{A}) \in K(\Phi)$.
% \end{definition}
% If obtaining the evidence or observing proof from the resolution is the only
% purpose of performing resolution, then we can use the functionalisation of the
% axioms to perform rewriting on the query instead of resolution. The following
% theorem formalize this intuition.
The following theorem formalizes the intuition that resolution and small-step resolution coincide.
\begin{theorem}
\label{func:eq}
$\Phi \vdash A \Downarrow e$ iff $ \Phi \vdash A \to^* e$.
\end{theorem}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
%\paragraph{Resolution Trees}
The proof tree for a judgement $\Phi \vdash A \Downarrow e$ is called a
\emph{resolution tree}. It conveniently records the history of resolution and,
for instance, it is easy to observe the ancestors of a node. This last feature
is useful for our heuristic loop invariant analysis in Section \ref{inv}.
Our formalisation of trees in general is as follows: We use $w, v$ to denote
positions $\langle k_1, k_2, ..., k_n \rangle$ in a tree, where $k_i \geq 1 $
for $ 1 \leq i \leq n $. Let $\epsilon$ denote the empty position or
\emph{root}. We also define $\langle k_1, k_2, ..., k_n \rangle \cdot i =
\langle k_1, k_2, ..., k_n, i\rangle $ and $\langle k_1, k_2, ..., k_n \rangle
+ \langle l_1,..., l_m \rangle = \langle k_1, k_2, ..., k_n, l_1, ..., l_m
\rangle$. We write $w > v$ if there exists a non-empty $v'$ such that $w = v + v'$. For a tree $T$, $T(w)$ refers to the node at position $w$, and
$T(w, i)$ refers to the edge between $T(w)$ and $T(w\cdot i)$. We use $\Box$ as a special proposition to denote
success.
Resolution trees are defined as follows, note that they are a special case of \textit{rewriting
trees}~\cite{KomendantskayaEtAl15,KJ15}:
%Resolution trees are trees of the following form.
\begin{definition}[Resolution Tree]
The resolution tree for atomic formula $A$ is
a tree $T$ satisfying:
\begin{itemize}
\item $T(\epsilon) = A$.
\item $T(w \cdot i) = \sigma B_i$ and $T(w, i) = \kappa^i$ with $i \in \{1
,..., n\}$ if $T(w) = \sigma D$ and $(\kappa : B_1, ..., B_n \Rightarrow D) \in
\Phi$. When $n = 0$, we write $T(w \cdot i) = \Box$ and $T(w, i) = \kappa$ for
any $i > 0$.
% \item otherwise $T(w) \uparrow$ and $T(w, i) \uparrow$.
\end{itemize}
\end{definition}
% TOM: DO WE NEED THIS DEFINITION:
% \begin{definition}[Projection]
% Let $(\kappa : B_1, ..., B_n \Rightarrow A) \in \Phi$. Then we define the projection of $\kappa$ on index $i$ as $\kappa^i : B_i \Rightarrow A$.
% \end{definition}
%\paragraph{Infinite Resolution}
In general, the resolution tree can be infinite, this means that resolution is
non-terminating, which we denote as $\Phi \vdash A \Uparrow$.
Figure~\ref{fig:ex2} shows a finite fragment of the infinite resolution tree for $\Phi_{\ensuremath{\Conid{HPTree}}} \vdash \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} \Uparrow$.
%Fig.~\ref{fig:ex2} shows an example of such an infinite resolution tree.
%\knote{Example of HPtree went to the intro}
%The corresponding extended axiom environment is:
%\[ \begin{array}{rcl}
% \Phi_2 & = \Phi_1, & |kMu : Eq (h (Mu h) a) => Eq (Mu h a)|, \\
% & & |kHPTree : (Eq a, Eq (f (a, a))) => Eq (HPTree f a)|
% \end{array}\]
\begin{figure}[tbp]
\makebox[\textwidth]{
\begin{tikzpicture}[every tree node/.style={},
level distance=1.20cm,sibling distance=1.00cm,
edge from parent path={(\tikzparentnode) -- (\tikzchildnode)}, font=\scriptsize]
\Tree [.\node{\underline{\ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})}}};
\edge node[auto=right]{$\ensuremath{\kappa_{\Varid{Mu}}}^1$};
[.\node{\ensuremath{\Conid{Eq}\;(\Conid{HPTree}\;(\Conid{Mu}\;\Conid{HPTree})\;\Conid{Int})}};
\edge node[auto=right]{$\ensuremath{\kappa_{\Varid{HPTree}}}^1$};
[.\node{\ensuremath{\Conid{Eq}\;\Conid{Int}}};
\edge node[auto=right]{$\ensuremath{\kappa_\Varid{Int}}$};
[.\node{$\Box$};
]
]
\edge node[auto=left]{$\ensuremath{\kappa_{\Varid{HPTree}}}^2$};
[.\node{\underline{\ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;(\Conid{Int},\Conid{Int}))}}};
\edge node[auto=right]{$\ensuremath{\kappa_{\Varid{Mu}}}^1$};
[.\node{\ensuremath{\Conid{Eq}\;(\Conid{HPTree}\;(\Conid{Mu}\;\Conid{HPTree})\;(\Conid{Int},\Conid{Int}))}};
\edge node[auto=right]{$\ensuremath{\kappa_{\Varid{HPTree}}}^1$};
[.\node{...};]
\edge node[auto=left]{$\ensuremath{\kappa_{\Varid{HPTree}}}^2$};
[.\node{...};]
]
]
]
]
\end{tikzpicture}
}
\caption{The infinite resolution tree for $\Phi_{\ensuremath{\Conid{HPTree}}} \vdash \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} \Uparrow$}
\label{fig:ex2}
\end{figure}
We note that Definitions~~\ref{def:resolution} and~\ref{context-red} describe a special case of SLD-resolution in which unification taking place in derivations is restricted to term-matching.
This restriction is motivated by two considerations. The first one comes directly from the application area of our results: type class resolution uses exactly this restricted version of SLD-resolution.
The second reason is of more general nature. As discussed in detail in~\cite{FuK15,KJ15}, SLD-derivations restricted to term-matching reflect the \emph{theorem proving} content of a proof by SLD-resolution. That is,
if $A$ can be derived from $\Phi$ by SLD-resolution with term-matching only, then $A$ is inductvely entailed by $\Phi$. If, on the other hand, $A$ is derived from $\Phi$ by SLD-resolution with unification and computes a substitution $\sigma$,
then $\sigma A$ is inductively entailed by $\Phi$. In this sense, SLD-resolution with unification additionally has a \emph{problem-solving} aspect.
%\frank{Can we not mention proof-search here? I think with LP-TM you can do searching as well.}
In developing proof-theoretic approach to resolution here, we thus focus on resolution by term-matching.
%\frank{A general comment: proof-theoretic approach is not limited to matching, we know what proof-theoretic meaning for LP-Unif as well, so I am wondering can we remove the last sentences in these two paragraphs? }
The resolution rule of Definition~\ref{def:resolution} resembles the definition of the consequence operator~\cite{Llo87} used to
define declarative semantics of Horn clause Logic.
In fact, the forward and backward closure of the rule of Definition~\ref{def:resolution} can be directly used to construct the usual least and greatest Herbrand models
for Horn clause logic, as shown in~\cite{KJ15}. There, it was also shown that SLD-resolution by term-matching is sound but incomplete relative to the least Herbrand models.
%In the following sections, we will only consider Definition~\ref{def:resolution} proof-theoretically.
% Thus the process of context reduction and dictionary construction can be viewed as the process
% of applying the resolution rule to reduce the initial query into an empty set, and then assemble
% all the reduction steps into an evidence. We now describe a way to construct evidence by term rewriting,
% i.e. to construct an evidence for the query $A$, we can apply a set of rewrite rules to rewrite $A$ to
% a proof term. The rewrite rule will be operating on the following \textit{mixed terms}.
%===============================================================================
\section{Candidate Lemma Generation}
\label{inv}
This section explains how we generate candidate lemma from a
potentially infinite resolution tree. Based on Paterson's condition we obtain
a finite pruned approximation (Definition~\ref{closed}) of this resolution tree.
Anti-unification on this approximation yields an abstract atomic formula and
the corresponding abstract approximated resolution tree. It is from this abstract
tree that we read off the candidate lemma (Definition~\ref{invariant}).
%Section~\ref{diss} discusses the intuition and the meaning behind this process
%in more detail.
% \begin{comment}
% \begin{definition}[Syntax]
% \[\begin{array}{l@@{\hspace{5mm}}l@@{\hspace{5mm}}c@@{\hspace{5mm}}l}
% \text{Term} & t \ & ::= & \ x \ || \ f(t_1,..., t_n) \\
%
% % Evidence $e \ & ::= & \ \kappa \ || \ \alpha \ || \ \lambda \alpha . e \ || \ e \ e'$
%
% \text{Atomic Formula} & A, B, C, D\ & ::= & \ P(t_1, ..., t_n) \\
%
% \text{Horn Formula} & H \ & ::= & \ A_1,..., A_n \Rightarrow A \\
%
% \text{Axioms} & \Phi \ & ::= & \cdot \ || \ \kappa : H, \Phi
% \end{array}
% \]
% \end{definition}
%
% Terms denote first-order types in a functional language, and atomic formulas
% represent type class constraints. Horn formulas in turn represent type class instance
% declarations.
%
% We use $\underline{A}$ to abbreviate $A_1,..., A_n$, when the number $n$ is
% unimportant. We write $A \mapsto_\sigma A'$ to express that $A$ matches $A'$
% with substitution $\sigma$, i.e., $\sigma A \equiv A'$. We use $\mathrm{FV}(A)$
% to denote the set of variables in $A$.
%
% We assume that there are no \textit{existential variables} in the Horn formulas, i.e.,
% $\bigcup_i \mathrm{FV}(B_i) \subseteq \mathrm{FV}(A)$ for $\underline{B}
% \Rightarrow A$. The axioms $\Phi$ are a set of Horn formulas with distinct labels
% $\kappa$. The labels are used to build a proof term. In line with Haskell we
% also assume that the instance heads of the axioms in $\Phi$ are non-overlapped.
%
% \begin{definition}[Projection]
% Let $(\kappa : B_1, ..., B_n \Rightarrow A) \in \Phi$. Then we define the projection of $\kappa$ on index $i$ as $\kappa^i : B_i \Rightarrow A$.
% \end{definition}
%
% We use $\uparrow$ and $\downarrow$ as post-fix meta-predicates to mean
% respectively undefined and defined. We use $\Box$ as a special proposition to
% denote success. We use $w, v$ to denote position sequence $\langle k_1, k_2,
% ..., k_n \rangle$ in a tree, where $k_i \geq 1 $ for $ 1 \leq i \leq n $.
% Let $\epsilon$ denote the empty position. We also define $\langle k_1, k_2, ..., k_n
% \rangle \cdot i = \langle k_1, k_2, ..., k_n, i\rangle $ and $\langle k_1, k_2,
% ..., k_n \rangle + \langle l_1,..., l_m \rangle = \langle k_1, k_2, ..., k_n,
% l_1, ..., l_m \rangle $. For a tree $T$, $T(w)$ refers to the node at position
% $w$, and $T(w, i)$ refers to the edge between $T(w)$ and $T(w\cdot i)$. The
% following definition of resolution tree is a special case of \textit{rewriting
% tree} \cite{KomendantskayaEtAl15}.
%
%
% \begin{definition}[Resolution tree]
% We define the resolution tree induced by atomic formula $C$ to be
% a tree $T$ satisfying the following conditions:
% \begin{itemize}
% \item $T(\epsilon) = C$.
% \item $T(w \cdot i) = \sigma B_i$ and $T(w, i) = \kappa^i$ with $i \in \{1 ,..., n\}$ if $T(w) = A$ and $\kappa : B_1, ..., B_n \Rightarrow A' \in \Phi$ with $A' \mapsto_\sigma A$. When $n = 0$, we write $T(w \cdot i) = \Box$ and $T(w, i) = \kappa$ for any $i > 0$.
% %% \item $T(w \cdot i) = \sigma B_i$ with $i \in \{1 ,..., n\}$ if $T(w) = (\kappa, \sigma)$ and $\kappa : B_1 ,..., B_n \Rightarrow A \in \Phi $. When $n = 0$, we write $T(w \cdot i) = \Box $ for any $i > 0$.
% \item otherwise $T(w) \uparrow$ and $T(w, i) \uparrow$.
% \end{itemize}
%
% %% \begin{itemize}
% %% \item $T(w) = A$ or $T(w) \uparrow$.
% %% \item $T(w, i) = (\kappa, \Delta)$ or $T(w, i) \uparrow$.
% %% \end{itemize}
% \end{definition}
%
% % \begin{definition}[Leaf]
% % A node in a rewriting tree $T(w)$ is called a \textit{leaf} if $T(w) \downarrow$ and $T(w \cdot i) = \uparrow$ for any $i$. A finite success rewriting tree is a tree where every leaf is $\Box$.
% % \end{definition}
%
% %% \begin{definition}[Tree transition]
% %% Let $T(w) = A$ with $T(w \cdot i) \uparrow, T(w, i) \uparrow$ for any $i$. Suppose there exists $\kappa : B_1,..., B_n \Rightarrow A' \in \Phi$ such that $A' \mapsto_\sigma A$. We define a tree transition from $T$ to $T'$ (denoted by $T \hookrightarrow_{w, \kappa} T'$), when $T'$ is the same as $T$ except $T'(w, i) = (\kappa, \sigma \Delta), T'(w \cdot i) = \sigma B_i$ for $i \in \{1,..., n\}$. When $n = 0$, $T(w, i) = (\kappa, \sigma \Delta), T(w\cdot i) = \Box$ for all $i \geq 1$.
% %% \end{definition}
% \end{comment}
We use $\Sigma(A)$ and $\mathrm{FVar}(A)$ to denote the
multi-sets of respectively function symbols and variables in $A$.
\begin{definition}[Paterson's Condition]
For $(\kappa : \underline{B} \Rightarrow A) \in \Phi$, we say $\kappa$
satisfies Paterson's condition if $(\Sigma(B_i) \cup \mathrm{FVar}(B_i))
\subset (\Sigma(A) \cup \mathrm{FVar}(A))$ for each $B_i$.
\end{definition}
Paterson's condition is used in Glasgow Haskell Compiler to enforce termination of context
reduction \cite{SulzmannDJS07}. In this paper, we use it as a practical
criterion to detect problematic instance declarations. Any declarations that do
not satisfy the condition could potentially introduce diverging behavior in
the resolution tree.
% We now
% define the notion of a \textit{critical triple} for as an approximation for the source of non-termination.
If $\kappa : A_1,..., A_n \Rightarrow B$, then we have $\kappa^i : A_i \Rightarrow B$ for projection on index $i$.
\begin{definition}[Critical Triple]
\label{loop}
Let $v = (w \cdot i) + v'$ for some $v'$. A critical triple in $T$ is a triple $\langle \kappa^i, T(w), T(v) \rangle$ such that $T(v, i) = T(w, i) = \kappa^i$, and $\kappa^i$ does not satisfy Paterson's condition.
\end{definition}
We will omit $\kappa^i$ from the triple and write $\langle T(w), T(v)
\rangle$ when it is not important. Intuitively, it means the nodes $T(w)$ and $T(v)$ are
using the same problematic projection $\kappa^i$, which could give rise to infinite resolution.
The absence of a critical triple in a resolution tree means
that it has to be finite \cite{SulzmannDJS07}, while the presence of
a critical triple only means that the tree is \textit{possibly} infinite. In
general the infiniteness of a resolution tree is undecidable and
the critical triples provide a convenient over-approximation.
\begin{definition}[Closed Subtree]
\label{closed}
A closed subtree $T$ is a subtree of a resolution tree such that for all leaves $T(v) \not = \Box$,
the root $T(\epsilon)$ and $T(v)$ form a critical triple.
\end{definition}
The critical triple in Figure \ref{fig:ex2} is formed by the underlined nodes. The
closed subtree in that figure is the subtree without the infinite branch below node
\ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;(\Conid{Int},\Conid{Int}))}. A closed subtree can intuitively be
understood as a finite approximation of an infinite resolution tree. We use it
as the basis for generating candidate lemma by means of
anti-unification \cite{plotkin1970note}.
%\section{Anti-unification and Abstract Unfolding}
\begin{definition}[Anti-Unifier]
We define the least general anti-unifier of atomic formulas $A$ and $B$ (denoted by $A \sqcup B$) and
the least general anti-unifier of the terms $t$ and $t'$ (denoted by $t \sqcup t'$) as:
\begin{itemize}
\item $P\ t_1\ ..., t_n\ \sqcup P\ t_1'\ ..., t_n' = P\ (t_1 \sqcup t_1')\ ...\ (t_n \sqcup t_n')$
\item $K\ t_1\ ...\ t_n \sqcup K \ t_1'\ ...\ t_n' = K\ (t_1\sqcup t_1')\ ...\ (t_n\sqcup t_n')$
\item Otherwise, $A \sqcup B = \phi(A,B), t \sqcup t' = \phi(t,t')$, where $\phi$ is an injective function from a pair of terms (atomic formulas) to a set of fresh variables.
\end{itemize}
\end{definition}
Anti-unification allows us to extract the common pattern from different ground atomic formulas.
\begin{definition}[Abstract Representation]
\label{abs:rep}
Let $\langle T(\epsilon), T(v_1)\rangle,..., \langle T(\epsilon), T(v_n) \rangle$ be all the critical triples in a closed subtree $T$.
Let $C = T(\epsilon) \sqcup T(v_1) \sqcup ... \sqcup T(v_n)$, then the abstract
representation $T'$ of the closed subtree $T$ is a tree such that:
\begin{itemize}
\item $T'(\epsilon) = C$
\item $T'(w \cdot i) = \sigma B_i$ and $T'(w, i) = \kappa^i$ with $i \in \{1
,..., n\}$ if $T'(w) = \sigma D$ and $(\kappa : B_1, ..., B_n \Rightarrow D) \in
\Phi$. When $n = 0$, we write $T'(w \cdot i) = \Box$ and $T'(w, i) = \kappa$ for
any $i > 0$.
\item $T'(w)$ is undefined if $w > v_i$ for some $1 \leq i \leq n$.
\end{itemize}
\end{definition}
The abstract representation unfolds the anti-unifier of all the critical
triples. Thus the abstract representation can always be embedded into the
original closed subtree. It is an abstract form of the closed subtree, and we
can extract the candidate lemma from the abstract representation.
\begin{definition}[Candidate Lemma]
\label{invariant}
Let $T$ be an abstract representation of a closed subtree, then the candidate lemma
induced by this abstract representation is $T(v_1),..., T(v_n) \Rightarrow T(\epsilon)$,
where the $T(v_i)$ are all the leaves for which $T(v_i) \Rightarrow T(\epsilon)$ satisfies Paterson's
condition.
\end{definition}
Figure \ref{fig:ex3} shows the abstract representation of the closed subtree of Figure \ref{fig:ex2}.
We read off the candidate lemma as \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})}.
\begin{figure}[tbp]
\makebox[\textwidth]{
\begin{tikzpicture}[every tree node/.style={},
level distance=1.20cm,sibling distance=1.00cm,
edge from parent path={(\tikzparentnode) -- (\tikzchildnode)}, font=\scriptsize]
\Tree [.\node{$\underline{\ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})}}$};
\edge node[auto=right]{$\ensuremath{\kappa_{\Varid{Mu}}}^1$};
[.\node{\ensuremath{\Conid{Eq}\;(\Conid{HPTree}\;(\Conid{Mu}\;\Conid{HPTree})\;\Varid{x})}};
\edge node[auto=right]{$\ensuremath{\kappa_{\Varid{HPTree}}}^1$};
[.\node{\ensuremath{\Conid{Eq}\;\Varid{x}}};
]
\edge node[auto=left]{$\ensuremath{\kappa_{\Varid{HPTree}}}^2$};
[.\node{\underline{\ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;(\Varid{x},\Varid{x}))}}};
]
]
]
]
\end{tikzpicture}
}
\caption{The abstract representation of the closed subtree of Figure~\ref{fig:ex2}}
\label{fig:ex3}
\end{figure}
The candidate lemma plays a double role. Firstly, it allows us to
construct a finite resolution tree. For example, we know that \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} gives rise to infinite tree with the axiom environment $\Phi_{\ensuremath{\Conid{HPTree}}}$. However, a finite
tree can be constructed with \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})},
since it reduces \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} to \ensuremath{\Conid{Eq}\;\Conid{Int}}, which succeeds trivially
with \ensuremath{\kappa_\Varid{Int}}. Next we show how to prove the candidate lemma coinductively, and
such proofs will encapsulate the
infinite aspect of the resolution tree. Since an infinite resolution tree gives
rise to infinite evidence, the finite proof of the lemma has to be
coinductive. We discuss such evidence construction in detail in Section~\ref{corec} and Section~\ref{ob-equiv}.
% TOO MUCH DISCUSSION
%
% Ideally, we want to prove the invariant formula corecursively, the process is described in the
% next section. After confirming the provability, we would be able to use the invariant formula to help us
% construct a finite representation of the infinite evidence. For example, assume $p$ is the proof of \texttt{Eq x => Eq (Mu HPTree x)}, then
% the evidence for \texttt{Eq (Mu HPTree Unit)} would be $(p \ \kappa_4)$. Of course, not all invariant formula generated from Definition \ref{invariant} are provable, this is due to the approximation nature of our abstraction process. However, our current
% method works well for a wide range of examples that involves using higher order
% fix point operator to represent nested data type and we will discuss the intuition behind
% this abstraction process in Section \ref{diss}.
%===============================================================================
\section{Corecursive Resolution}
\label{corec}
% The resolution process defined in Section~\ref{preliminary} reduces atomic
% formulas and provides first-order evidence. It cannot generate corecursive evidence for the corecursive
% hypotheses in Section~\ref{inv}, nor it can use the corecursive hypotheses alongside
% the axiom environment to reduce other formulas.
% In this section we extend the definition of resolution to do both.
% \knote{May be re-formulate the above para?}
In this section, we extend the definition of resolution from Section~\ref{preliminary}
by introducing two additional rules: one to handle coinductive proofs, and another -- to allow Horn formula goals, rather than atomic goals, in the derivations.
%% These extensions allow us to integrate reasoning about richer (Horn formula) coinductive hypotheses with corecursive evidence construction.
We call the resulting calculus \textit{corecursive resolution}.
%and formulate Corecursive Resolution rule,
%whi
\begin{definition}[Extended Syntax]
\label{syntax}
{\small
\[
\begin{array}{l@{\hspace{5mm}}l@{\hspace{5mm}}c@{\hspace{5mm}}l}
\text{Proof/Evidence} & e & ::= & \kappa ~\mid~ e \ e' ~\mid~ \textcolor{blue}{\alpha} ~\mid~ \textcolor{blue}{\lambda \alpha . e} ~\mid~ \textcolor{blue}{\mu \alpha. e} \\
\text{Axiom Environment} & \Phi & ::= & \cdot ~\mid~ \Phi, (\textcolor{blue}{e} : H)
\end{array}
\]}
\end{definition}
To support coinductive proofs, we extend the syntax of evidence with functions
$\lambda \alpha . e$, variables $\alpha$ and fixed point $\mu \alpha . e$ (which models the corecursive equation $\alpha = e$ in which $\alpha$ occurs in $e$). Also
we allow the Horn clauses $H$ in the axiom environment $\Phi$ to be supported by any
form of evidence $e$ (and not necessarily by constants $\kappa$).
% The let-binding in the evidence can be corecursive, i.e. for $\mylet{\alpha = e}{e'}$, $\alpha \in \mathrm{FV}(e)$. Axioms is augmented with variable and
% corecursive definition. $(\alpha : H) = e$ means $\alpha$ of type $H$ is corecursively
% defined as $e$, i.e. $\alpha \in \mathrm{FV}(e)$. To check $\Phi, (\alpha : H) = e$ is well-formed,
% just need to check $\Phi \vdash H \Downarrow \mylet{\alpha = e}{\alpha}$.
\begin{definition}[Corecursive Resolution]\label{def:cresolution}
The following judgement for corecursive resolution extends the resolution in Definition~\ref{def:resolution}. {\small
\[\begin{array}{c}
\infer[\text{if}~(e : B_1,..., B_m \Rightarrow A) \in \Phi]
{\Phi \vdash \sigma A \Downarrow e~e_1 \cdots e_n}
{ \Phi \vdash \sigma B_1 \Downarrow e_1 \quad \cdots \quad \Phi \vdash \sigma B_n \Downarrow e_n
}
\\ \\
\infer[(\textsc{Mu})]
{\Phi \vdash \underline{A} \Rightarrow B \Downarrow \mu \alpha . e }
{\Phi, (\alpha : \underline{A} \Rightarrow B) \vdash \underline{A} \Rightarrow B \Downarrow e & \mathrm{HNF}(e)}
\quad\quad
\infer[(\textsc{Lam})]
{\Phi \vdash \underline{A} \Rightarrow B \Downarrow \lambda \underline{\alpha} . e}
{\Phi, (\underline{\alpha} : \underline{A}) \vdash B \Downarrow e}
\end{array}
\]}
% & \gamma = [\underline{c}/\underline{x}] & \underline{c}~\text{fresh constants} & \underline{\alpha}~\text{fresh}
\end{definition}
Note that $\mathrm{HNF}(e)$ means $e$ has to be in \textit{head normal form}
$\lambda \underline{\alpha}.\kappa\ \underline{e}$. This requirement is essential to ensure
the corecursive evidence satisfies the \textit{guardedness} condition.\footnote{See the extended version for a detailed discussion.} The \textsc{Lam} rule implicitly assumes the treatment of \textit{eigenvariables},
i.e. we instantiate all the free variables in $\underline{A} \Rightarrow B$
with fresh term constants.
We implicitly assume that axiom environments are well-formed.
\begin{definition}[Well-formedness of environment]
{\small
\[
\begin{array}{c}
\infer{\cdot \vdash \mathsf{wf} }{}
\quad\quad
\infer{\Phi, \alpha : H \vdash \mathsf{wf} }{\Phi \vdash \mathsf{wf}}
\quad\quad
\infer{\Phi, \kappa : H \vdash \mathsf{wf} }{\Phi \vdash \mathsf{wf}}
\quad\quad
\infer{\Phi, e : H \vdash \mathsf{wf} }{\Phi \vdash H \Downarrow e}
\end{array}
\]}
\end{definition}
% \begin{comment}
% After we normalize (i.e. first apply the \textsc{Corec} rule, then apply the \textsc{Imp} rule) the initial environment, we can then apply the following \textit{corecursive resolution}.
%
%
% \begin{definition}[Corecursive resolution]
% Given axioms $\Phi$, the resolution for $B$ is corecursive if the first reduction step
% from $\Phi \vdash \{ B \}$ is $\to_\kappa$ for some $\kappa : H \in \Phi$.
% \end{definition}
% The requirement of first resolution step in the corecursive resolution is to ensure
% the evidence generated by the corecursive resolution can be reduced to \textit{head normal form}, we refer to the appendix for a detailed treatment.
%
%
% \begin{theorem}
% \label{corec:thm}
% If there is a corecursive resolution $\Phi, \alpha : \underline{A} \Rightarrow B, \underline{\alpha} : \underline{A} \vdash \{B\} \to^* \emptyset$, then $(\alpha : \underline{A} \Rightarrow B) \mapsto \lambda \underline{\alpha} . e$ for some proof term $e$.
% \end{theorem}
% \begin{proof}
% By Theorem \ref{func:eq}, we have $K(\Phi, \alpha : \underline{A} \Rightarrow B, \underline{\alpha} : \underline{A}) \vdash B \to^* e$. Thus $(\alpha : \underline{A} \Rightarrow B) \mapsto \lambda \underline{\alpha} . e$.
% \end{proof}
% \end{comment}
As an example, let us consider resolving the candidate lemma \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{My}\;\Conid{HPTree}\;\Varid{x})} against
the axiom environment $\Phi_{\ensuremath{\Conid{HPTree}}}$. This yields the following derivation, where
$\Phi_1 = \Phi_{\ensuremath{\Conid{HPTree}}}, (\alpha : \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})})$ and $\Phi_2 = \Phi_1, (\alpha_1 : \ensuremath{\Conid{Eq}\;\Conid{C}})$:
% \[
% \begin{array}{lcrcl}
% \kappa_1 &:& {Eq}\ (f\ ({Mu}\ f)\ a) &\Rightarrow& {Eq}\ ({Mu}\ f\ a) \\
% \kappa_2 &:& ({Eq}\ a, {Eq}\ (f\ ({Pair}\ a\ a))) &\Rightarrow& {Eq}\ ({HPTree}\ f\ a) \\
% \kappa_3 &:& ({Eq}\ a, {Eq}\ b) &\Rightarrow& {Eq}\ ({Pair}\ a\ b) \\
% \kappa_4 &:& Eq\ Unit
% \end{array}
% \]
%
% \noindent Note that $f, a, b$ are variables. Let $\Phi_1 = \Phi, \alpha : | Eq x => Eq (Mu HPTree x)|$, $\Phi_2 = \Phi_1, \alpha_1 : |Eq C| $. We have the following derivation:
{\small
\begin{center}
\infer{\Phi_{\ensuremath{\Conid{HPTree}}}\vdash \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})} \Downarrow \mu \alpha . \lambda \alpha_1 . \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1\ (\alpha\
(\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)))}
{\infer{\Phi_1 \vdash \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})} \Downarrow \lambda \alpha_1 . \kappa_{\ensuremath{\Conid{Mu}}}
\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1\ (\alpha\
(\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)))}
{\infer{(\Phi_2 = \Phi_1, \alpha_1 : \ensuremath{\Conid{Eq}\;\Conid{C}}) \vdash \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{C})} \Downarrow \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1\ (\alpha\
(\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)))}
{\infer{\Phi_2 \vdash \ensuremath{\Conid{Eq}\;(\Conid{HPTree}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{C}))} \Downarrow \kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1\ (\alpha\
(\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1))}{
\infer{\Phi_2 \vdash \ensuremath{\Conid{Eq}\;\Conid{C}} \Downarrow \alpha_1}{} & \infer{\Phi_2 \vdash \ensuremath{\Conid{Eq}\;(\Conid{HPTree}\;(\Conid{C},\Conid{C}))} \Downarrow \alpha\
(\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)}{
\infer{\Phi_2 \vdash \ensuremath{\Conid{Eq}\;(\Conid{C},\Conid{C})} \Downarrow (\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)}
{\infer{\Phi_2 \vdash \ensuremath{\Conid{Eq}\;\Conid{C}} \Downarrow \alpha_1}{} & \infer{\Phi_2 \vdash \ensuremath{\Conid{Eq}\;\Conid{C}} \Downarrow \alpha_1}{}}}}} }}
\end{center}
}
\noindent Once we prove \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})} from $\Phi_{\ensuremath{\Conid{HPTree}}}$ by corecursive resolution, we can add it to the
axiom environment and use it to prove the ground query \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})}. Let $\Phi' = \Phi_{\ensuremath{\Conid{HPTree}}}, (\mu \alpha . \lambda \alpha_1 . \kappa_1\ (\kappa_2\ \alpha_1\ (\alpha\ (\kappa_3\ \alpha_1\ \alpha_1))) : \ensuremath{\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Varid{x})})$. We have the following derivation.
{\small
\[
\begin{array}{c}
\infer{\Phi' \vdash \ensuremath{\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;\Conid{Int})} \Downarrow (\mu \alpha . \lambda \alpha_1 . \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{HPTree}\ \alpha_1\ (\alpha\ (\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)))) \
\kappa_{\ensuremath{\Conid{Int}}}} {\Phi' \vdash \ensuremath{\Conid{Eq}\;\Conid{Int}} \Downarrow \kappa_{\ensuremath{\Conid{Int}}}}
\end{array}
\]
}
\begin{comment}
We begin with initial environment $\Phi \vdash \{{Eq}\ x \Rightarrow
{Eq}\ ({Mu}\ {HPTree}\ x)\}$. By preprocessing, we have $\Phi'
\vdash \{ {Eq}\ ({Mu}\ {HPTree}\ C)\}$, where $\Phi' = \Phi, \alpha
: {Eq}\ x \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ x), \alpha_1 : {Eq}\ C$
and $C$ is an constant. Thus we have the following corecursive
resolution.
{\footnotesize
\begin{center}
$\Phi' \vdash \{ {Eq}\ ({Mu}\ {HPTree}\ {C})\} \to_{\kappa_1} \{
{Eq}\ ({HPTree} \ ({Mu}\ {HPTree})\ {C}) \}
\to_{\kappa_2}\{{Eq}\ {C}, {Eq}\ ({Mu}\ {HPTree}\ ({Pair}\ {C}\
{C}))\} \to_{\alpha_1} \{ {Eq}\ ({Mu}\ {HPTree}\ ({Pair}\ {C}\
{C}))\} \to_\alpha \{ {Eq}\ ({Pair}\ {C}\ {C})\} \to_{\kappa_3}
\{{Eq}\ {C}, {Eq}\ {C} \} \to_{\alpha_1} \{{Eq}\ {C}\}
\to_{\alpha_1} \emptyset$
\end{center}
}
\noindent By theorem \ref{corec:thm}, we obtain the following
corecursive evidence:
\noindent $(\alpha : {Eq}\ x \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ x))
\mapsto \lambda \alpha_1 . \kappa_1\ (\kappa_2\ \alpha_1 \ (\alpha \
(\kappa_3 \ \alpha_1 \ \alpha_1)))$.
\end{comment}
%===============================================================================
\section{Operational Semantics of Corecursive Evidence}
\label{ob-equiv}
% \begin{comment}
% \textbf{Relation to Term Rewriting.} Assume all the axioms are Horn formulas, due to lack of existantial variable, axioms can be viewed as a set of rewrite rule, for example, $\kappa : A_1,..., A_n \Rightarrow B$ can be viewed as a rewrite
% rule $B \to \kappa\ A_1\ ...\ A_n$, thus resolving the query together with obtaining evidence
% can be reified as the rewrite process on the query. In Section \ref{inv}, the method we use to obtain the invariant formula is closely related to \textit{loop detection} in term
% rewriting. A loop is detected if we observe an abstract reduction of the shape
% $A \to^* \mathcal{C}[\sigma A]$, where $\mathcal{C}$ is some contexts. The notion of abstract representation in Definition \ref{abs:rep} is trying to capture the abstract reduction $A \to^* \mathcal{C}[\sigma A]$.
%
% For us it is not enough to just detect a loop, we also want to introduce
% a \textit{sound} rewrite rule(Horn formula) to terminate this infinite process.
% Assume the atomic formulas $D_1, ..., D_n$ in $\mathcal{C}$
% are irreducible. To ensure
% the soundness of the rewrite rule, it will have to be corecursively provable. One rule
% that we could add in this case is $D_1, ..., D_n \Rightarrow A$, or $A \to \alpha\ D_1 ...\ D_n$, then we would have $A \to^* \mathcal{C}[\sigma A] \to \mathcal{C}[(\alpha\ (\sigma D_1) ... (\sigma D_n))]$. So to terminate this process, we just need to make sure $\sigma D_i$ terminates for
% all $i$. A \textit{simple condition} that one can check is $\sigma D_i \to^* \mathcal{C}_i[D_i]$ for all $i$ with $\mathcal{C}_i$ does not contain any atomic formula other than $D_i$. If this simple condition is met,
% then we can be sure that\footnote{Please see appendix for the proof.}: 1. $D_1, ..., D_n \Rightarrow A$ is corecursively provable. 2. $A$ is terminating with the new rule $A \to \alpha\ D_1 ...\ D_n$. 3. The infinite rewrite process of $A$ corresponds to the infinite unfolding of $\alpha \ D_1 ... \ D_n$ with the corecursive definition of $\alpha$.
% \end{comment}
The purpose of this section is to give operational
semantics to corecursive resolution, and in particular, we are interested in giving
operational interpretation to the
corecursive evidence constructed as a result of applying corecursive resolution.
In type class applications, for example, the evidence constructed for a query will be run as a program.
It is therefore important to establish the exact relationship
between the non-terminating resolution as a process and the proof-term that we obtain via corecursive resolution. %: the task is to show their correspondence.
%introduced
%considers correctness of the corecursive resolution introduced in
%the previous section.
We prove that corecursive evidence indeed faithfully
captures the otherwise infinite resolution process of Section~\ref{preliminary}.
%with finite corecursive evidence.
% It is natural to ask whether the corecursive evidence obtained this way is a genuine reflection of the infinite resolution
% process. In this section, we show that the ability to generate corecursive evidence is closely related to
% the ability of the loop detection in term rewriting(through small step resolution). Moreover, we show for a simple class of looping resolution, it is \textit{observationally equivalent} to the infinite unfolding of its corecursive evidence.
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
%\paragraph{Simple Loops}
%\tom{What is this text about? About explaining that we only consider simple loops?}
In general, we know that if $\Phi \vdash A \to^* \mathcal{C}[\sigma A]$, then we can observe the following looping infinite reduction trace:
\[ \Phi \vdash A \to^* \mathcal{C}[\sigma A] \to^* \mathcal{C}[\sigma \mathcal{C}[\sigma^2 A]] \to^* \mathcal{C}[\sigma \mathcal{C}[\sigma^2 \mathcal{C}[\sigma^3 A]]] \to ... \]
Each iteration of the loop gives rise to repeatedly applying
substitution $\sigma$ to the reduction context $\mathcal{C}$.
In principle, this mixed term context $\mathcal{C}$ may contain an atomic
formula $B$ that itself is normalizing, where $\sigma B$ spawns another loop.
Clearly this is a complicating factor. For instance, a
loop can spawn off additional loops in each iteration. Alternatively, a loop
can have multiple iteration points such as
$\Phi \vdash A \to^* \mathcal{C}[\sigma_1 A, \sigma_2 A, ..., \sigma_n
A]$.\footnote{Note that we abuse notation here to denote contexts with multiple holes.
Also we abbreviate identical instantiation of $\mathcal{C}[D, \ldots, D]$ those multiple holes to $\mathcal{C}[D]$.}
These complicating factors are beyond the scope of this section. We focus
only on \textit{simple loops}. These are loops with a single iteration point
that does not spawn additional loops.
We use $|\mathcal{C}|$ to denote the set of atomic formulas in the context
$\mathcal{C}$. If all atomic formulas $D \in |\mathcal{C}|$ are irreducible
with respect to $\Phi$, then we call $\mathcal{C}$ a \textit{normal context}.
\begin{definition}[Simple Loop]
Let $\Phi \vdash B \to^* \mathcal{C}[\sigma B]$, where $\mathcal{C}$ is
normal. If for all $D \in |\mathcal{C}|$, we have that $\Phi \vdash \sigma D \to^*
\mathcal{C}'[D]$ with $| \mathcal{C}' | = \emptyset$, then we call $\Phi
\vdash B \to^* \mathcal{C}[\sigma B]$ a simple loop.
\end{definition}
In the above definition, the normality of $\mathcal{C}$ ensures that the loop
has a single iteration point. Likewise the condition $\Phi \vdash \sigma D \to^*
\mathcal{C}'[D]$, which implies that $\Phi \vdash \sigma^n D \to^*
\mathcal{C}'^n[D]$, guarantees that each iteration of the loop
spawns no further loops.
\begin{definition}[Observational Point]
\label{observe}
Let $\Phi \vdash B \to^* \mathcal{C}'[\sigma B]$ be a simple loop and $\Phi \vdash B \to^* q$. We call $q$ an observational point if it is of the form $\mathcal{C}[\delta B]$. We use $\mathcal{O}(B)_{\Phi}$ to denote the set of observational points in the simple loop.
\end{definition}
For example, we have the following infinite resolution trace generated by the simple loop (with the subterms of observational points underlined).
{\scriptsize
\begin{center}
$\Phi_{\ensuremath{\Conid{HPTree}}} \vdash \underline{{Eq}\ ({Mu}\ {HPTree} \ x)} \to \kappa_{\ensuremath{\Conid{Mu}}}\ ({Eq}\ ({HPTree}\ ({Mu}\ {HPTree})\ x)) \to \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ ({Eq}\ x) \ \underline{({Eq}\ ({Mu}\ {HPTree}\ (x,x)))}) \to
\kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ ({Eq}\ x) \ (\kappa_{\ensuremath{\Conid{Mu}}} \ (Eq \ (HPTree \ (Mu \ HPTree)\ (x,x))))) \to
\kappa_{\ensuremath{\Conid{Mu}}} (\kappa_{\ensuremath{\Conid{HPTree}}} ({Eq}\ x) (\kappa_{\ensuremath{\Conid{Mu}}} (\kappa_{\ensuremath{\Conid{HPTree}}} (Eq (x,x)) (Eq (Mu\ HPTree \ ((x,x),(x,x))))))) \to \kappa_{\ensuremath{\Conid{Mu}}} (\kappa_{\ensuremath{\Conid{HPTree}}} ({Eq}\ x) (\kappa_{\ensuremath{\Conid{Mu}}} (\kappa_{\ensuremath{\Conid{HPTree}}} (\kappa_{\ensuremath{\Conid{Pair}}} (Eq\ x) (Eq\ x))) \underline{\ensuremath{(\Conid{Eq}\;(\Conid{Mu}\;\Conid{HPTree}\;((\Varid{x},\Varid{x}),(\Varid{x},\Varid{x}))))}})))$ $\to ... $
\end{center}
}
\noindent In this case, we have $\sigma = [\ensuremath{(\Varid{x},\Varid{x})}/\ensuremath{\Varid{x}}]$ and $\Phi \vdash \sigma ({Eq}\ x) \to \kappa_{\ensuremath{\Conid{Pair}}}\ ({Eq}\ x)\ ({Eq}\ x)$.
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
%\paragraph{Reduction of Corecursive Evidence}
The corecursive evidence encapsulates an infinite derivation in a finite fixpoint
expression. We can recover the infinite resolution by reducing the
corecursive expression.
To define small-step \textit{evidence reduction}, we first extend
mixed terms to cope with richer
corecursive evidence.
\begin{definition}
Mixed term $q \ ::= \ A \ |\ \kappa \ | \ q \ q'\ | \ \textcolor{blue}{\alpha}\ |\ \textcolor{blue}{\lambda \alpha.q} \ | \ \textcolor{blue}{\mu \alpha.q}$
\end{definition}
Now we define the small-step evidence reduction relation $q \leadsto q'$.
\begin{definition}[Small Step Evidence Reduction]
\label{label}
\fbox{$q \leadsto q'$}
{\small
\[\begin{array}{c}
\infer{{\mathcal{C}[\mu \alpha . q]} \leadsto_\mu \mathcal{C}[[\mu \alpha . q/\alpha]q]}{}
\quad \quad
\infer{\mathcal{C}[(\lambda \alpha . q) \ q'] \leadsto_\beta \mathcal{C}[[q'/\alpha] q] }{}
\end{array}
\]}
\end{definition}
Note that for simplicity we still use the mixed term context $\mathcal{C}$ as defined in
Section \ref{preliminary}, but we only allow the reduction of an outermost redex, i.e.,
a redex that is not a subterm of some other redex. In other words,
reduction unfolds the evidence term strictly downwards from the
root, this follows closely the way evidence is constructed during
resolution.
We call the states where we perform a $\mu$-transition \emph{corecursive points}.
Note that $\mu$-transitions unfold
a corecursive definition.
These
correspond closely to the observational points in resolution.
\begin{definition}[Corecursive Point]
Let $q' \leadsto^* q$. We call $q$ a corecursive point if it is of the form $\mathcal{C}[(\mu \alpha.e) \ q_1 ...\ q_n]$. We use $\mathcal{S}(q')$ to denote the set of corecursive points in $q' \leadsto^* q$.
\end{definition}
%\tom{Basically you have a corecursive point whenever you apply a $\mu$ transition, right?}
Let $e \equiv \mu \alpha . \lambda \alpha_1 . \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1\ (\alpha\ (\kappa_{\ensuremath{\Conid{Pair}}}\ \alpha_1\ \alpha_1)))$. We have the following evidence reduction trace (with the subterms of corecursive points underlined):
{\scriptsize
\begin{center}
$\underline{e \ ({Eq}\ x)} \leadsto_\mu (\lambda \alpha_1
. \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1 \ (e \
(\kappa_{\ensuremath{\Conid{Pair}}} \ \alpha_1 \ \alpha_1))))\ ({Eq}\ x)
\leadsto_\beta \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ ({Eq}\ x) \
\underline{(e \ (\kappa_{\ensuremath{\Conid{Pair}}} \ ({Eq}\ x) \ ({Eq}\ x)))})
\leadsto_\mu \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ ({Eq}\ x) \
((\lambda \alpha_1 . \kappa_{\ensuremath{\Conid{Mu}}}\ (\kappa_{\ensuremath{\Conid{HPTree}}}\ \alpha_1
\ (e \ (\kappa_{\ensuremath{\Conid{Pair}}} \ \alpha_1 \ \alpha_1)))) \
(\kappa_{\ensuremath{\Conid{Pair}}} \ ({Eq}\ x) \ ({Eq}\ x)))) \leadsto_\beta
\kappa_{\ensuremath{\Conid{Mu}}} (\kappa_{\ensuremath{\Conid{HPTree}}} ({Eq}\ x) (\kappa_{\ensuremath{\Conid{Mu}}}
(\kappa_{\ensuremath{\Conid{HPTree}}} (\kappa_{\ensuremath{\Conid{Pair}}} ({Eq}\ x) ({Eq}\ x))\underline{(e (\kappa_{\ensuremath{\Conid{Pair}}} (\kappa_{\ensuremath{\Conid{Pair}}} ({Eq}\ x) ({Eq}\
x)) (\kappa_{\ensuremath{\Conid{Pair}}} ({Eq}\ x) ({Eq}\ x)) ))})))$
$\leadsto_\mu ...$
\end{center}
}
%\paragraph{Observational Equivalence}
Observe that the mixed term contexts of the observational points and the
corecursive points in the above traces coincide. This allows us to show
observational equivalence of resolution and evidence reduction without
explicitly introducing actual infinite evidence.
The following theorem shows that if resolution gives rise to a simple loop,
then we can obtain a corecursive evidence $e$ (Theorem \ref{equiv} (1)) such that
the infinite resolution trace is observational equivalent to $e$'s evidence
reduction trace (Theorem \ref{equiv} (2)).
\begin{theorem}[Observational Equivalence]
\label{equiv}
Let $\Phi \vdash B \to^* \mathcal{C}[\sigma B]$ be a simple loop and $|\mathcal{C}| = \{D_1, ..., D_n\}$.
Then:
\noindent \textit{1.} We have $\Phi \vdash D_1, ..., D_n \Rightarrow B \Downarrow \mu \alpha . \lambda \alpha_1 .... \lambda \alpha_n . e$ for some $e$.
\noindent \textit{2.} $\mathcal{C}[\delta B] \in \mathcal{O}(B)_\Phi$ iff $\mathcal{C}[(\mu \alpha . \lambda \underline{\alpha} . e) \ \underline{q}] \in \mathcal{S}((\mu \alpha . \lambda \underline{\alpha} . e) \ \underline{D})$.
\end{theorem}
The proof can be found in the extended version.
% observational equivalent to the infinite unfolding of . Intuitively, the infinite resolution
% process of $\mathrm{Eq}\ (\mathrm{Mu}\ \mathrm{HPTree} \ x)$ is tranferred to the corecursive
% definition of $\alpha$, which can be unfolded lazily by the weak head reduction.
%% On the other hand, we can show that if
%% $\sigma D_i$ can be normalized to $D_i$ for all $D_i$, then the invariant formula $\alpha : D_1,..., D_n \Rightarrow A$, is corecursively provable . Thus using the corresponding rewrite rule $A \to \alpha\ D_1 ...\ D_n$ will result in the following terminating trace: $A \to^* \mathcal{C}[\sigma A] \to \mathcal{C}[(\alpha\ (\sigma D_1) ... (\sigma D_n))] \to^* \mathcal{C}[(\alpha\ D_1 ... \ D_n)]$. Since the proof of $D_1,..., D_n \Rightarrow A$ is correcursive, $\alpha$ will be a corecursive functional definition.
%% Thus the infinite process is transferred from rewriting of the formula $A$ to the potential
%% infinite evaluation of function $\alpha$.
% \textbf{Current Limitation}
% \textbf{Potential Work-around}
%===============================================================================
\section{Related Work}
\label{relwork}
\emph{Calculus of Coinductive Constructions.} Interactive theorem prover Coq pioneered implementation of the \textit{guarded coinduction principle} (\cite{coquand1994infinite,gimenez1996}).
The Coq termination checker may prevent some nested uses of coinduction, %e.g.
%certain nested use of coinduction is prohibited,
e.g. a proof term such as $(\mu \alpha . \lambda x . \kappa_0\ (\kappa_1\ x\ (\alpha\ (\alpha\ x)))) \ \kappa_2$ is not accepted by Coq, while from the outermost reduction point of view, this proof term is productive.
\emph{Loop detection in term rewriting.} Distinctions between cycle, loop and non-looping
has long been established in term rewriting research (\cite{dershowitz1987,zantema1996non}). For us, detecting loop is the first step of invariant analysis, but we also want to extract corecursive evidence such that it captures the infinite reduction trace.
\emph{Restricted datatypes.} Hughes (Section 4 \cite{hughes1999restricted})
observed the cyclic nature of the instance declarations \ensuremath{\mathbf{instance}\;\Conid{Sat}\;(\Conid{EqD}\;\Varid{a})\Rightarrow \Conid{Eq}\;\Varid{a}} and
\ensuremath{\mathbf{instance}\;\Conid{Eq}\;\Varid{a}\Rightarrow \Conid{Sat}\;(\Conid{EqD}\;\Varid{a})}. He proposed to treat the looping context
reduction as failure, in which case the compiler would need to search for an alternative
reduction.
\emph{Scrap Your Boilerplate with Class.} The cycle
detection method \cite{Lammel:2005} was proposed to
generate corecursive evidence for a restricted
class of non-terminating resolution. It is supported by the current Glasgow Haskell Compiler.
\emph{Derivable type classes.} Hinze and Peyton Jones \cite{hinze2001}
wanted to use an instance of the form
\noindent \ensuremath{\mathbf{instance}\;(\Conid{Binary}\;\Varid{a},\Conid{Binary}\;(\Varid{f}\;(\Conid{GRose}\;\Varid{f}\;\Varid{a})))\Rightarrow \Conid{Binary}\;(\Conid{GRose}\;\Varid{f}\;\Varid{a})}, but discovered that it causes resolution to diverge.
They suggested the following as a replacement:
\noindent \ensuremath{\mathbf{instance}\;(\Conid{Binary}\;\Varid{a},\forall \Varid{b}\hsforall \hsdot{\mathrel{\,\cdot\,}}{\;.\;}\Conid{Binary}\;\Varid{b}\Rightarrow \Conid{Binary}\;\Varid{f}\;\Varid{b})\Rightarrow \Conid{Binary}\;(\Conid{GRose}\;\Varid{f}\;\Varid{a})}.
Unfortunately, Haskell does not support instances with \textit{polymorphic higher-order instance contexts}.
Nevertheless, allowing such implication constraints
would greatly increase the expressitivity of corecursive resolution. In the terminology of
our paper, it amounts to extending Horn formulas to intuitionistic formulas.
Working with intuitionistic formulas would require a certain amount of searching,
as the non-overlapping condition for Horn formulas is not enough to ensure uniqueness of
the evidence. For example, consider the following axioms:
\begin{center}
$\kappa_1 : (A \Rightarrow B\ x) \Rightarrow D\ (S\ x)$
$\kappa_2 : A, D\ x \Rightarrow B\ (S\ x)$
$\kappa_3 :\ \Rightarrow D\ Z$
\end{center}
% \begin{center}
% $\kappa_1 : ((A \Rightarrow B) \Rightarrow B) \Rightarrow B$
% $\kappa_2 :\ \Rightarrow A$
% \end{center}
\noindent We have two distinct proof terms for $D\ (S\ (S\ (S\ (S\ Z)))))$:
\begin{center}
$\kappa_1\ (\lambda \alpha_1 . \kappa_2\ \alpha_1\ (\kappa_1\ (\lambda \alpha_2
. \kappa_2\ \underline{\remph{\alpha_1}}\ \kappa_3)))$
$\kappa_1\ (\lambda \alpha_1 . \kappa_2\ \alpha_1\ (\kappa_1\ (\lambda \alpha_2
. \kappa_2\ \underline{\remph{\alpha_2}}\ \kappa_3)))$
\end{center}
% There are two distinct proofs for $B$, i.e. $\kappa_1 \ (\lambda \alpha . \alpha \ \kappa_2) : B $ and $\mu \beta . \kappa_1 \ (\lambda \alpha . \beta) : B$.
\noindent This is
undesirable from the perspective of generating evidence for type class.
\emph{Instance declarations and (Horn Clause) logic programs}. The process of simplifying type class
constraints is formally described as the notion of \textit{context reduction}
by Peyton Jones et. al.~\cite{Jones97}. In Section 3.2 of the same paper also
describes the form and the requirements of instance declarations. Type class
evidence and their connection to type system are studied in Mark Jones's
thesis~\cite[Chapter 4.2]{jones2003qualified}. Context reduction,
instance declaration and their connection to proof relevant resolution are also
discussed under the name of \textit{LP-TM} (logic programming with
term-matching) in Fu and Komendantskaya~\cite[Section 4.1]{FuK15}.
%% \paragraph{Calculus of Infinite Construction}. Coq implements the
%% \textit{guarded induction principle} (\cite{coquand1994infinite},
%% \cite{gimenez1996}), i.e. in order to prove a proposition $F$, from the
%% assumptions $F_1, .., F_n$, it is enough to build a proof term using not only
%% natural deduction and lemmas, but also using $F$, providing the use of $F$ is
%% guarded by introduction rules.
%===============================================================================
\section{Conclusion and Future Work}\label{fwork}
We have introduced a novel approach to non-terminating resolution.
Firstly, we have shown that the popular cycle detection methods employed for logic programming or type class resolution
can be understood via more general coinductive proof principles (\cite{coquand1994infinite,gimenez1996}).
Secondly, we have shown that
resolution can be enriched with rules that capture the intuition of richer coinductive hypothesis formation.
This extension allows to provide corecursive evidence to some derivations that could not be handled by previous methods.
Moreover, corecursive resolution is formulated in a proof-relevant way, i.e. proof-evidence construction is an essential part
of corecursive resolution. This makes it easier to integrate it directly into type class inference.
%Firstly, it is possible to incorporate coinductive hypothesis
%to introduce heuristics in order to search for a
\begin{comment}
To obtain corecursive evidence for a query that has non-terminating resolution,
our approach is to first generate a richer coinductive hypothesis in the form of
an invariant formula, and to prove this formula automatically by corecursive
resolution, then use the proven invariant formula as a lemma to facilitate the construction
of finite evidence for the initial query.
We first describe a heuristic method to generate invariant formulas in Section
\ref{inv}. This method exploits Paterson's condition and anti-unification. It
is essentially a form of loop detection for the resolution trace generated by
the ground query. The head of the invariant formula generated by our method is
least general due to the use of anti-unification. This is a desirable property
in practice since it avoids unnecessary overlap with other axioms.
To construct corecursive evidence for the invariant formulas, in Section
\ref{corec}, we extend resolution to allow corecursion and Horn formula queries. The corecursive resolution has
a direct type-theoretic interpretation and the corecursive evidence it generates is weak-head
normalizing.\footnote{See Appendix \ref{ap:guard}.} In
Section \ref{ob-equiv}, divergent resolution due to simple loops is shown to be
observational equivalent to the infinite unfolding of its corecursive evidence.
\end{comment}
We have implemented the techniques of Sections \ref{inv} and \ref{corec}, and have incorporated
them as part of the evidence construction process for a simple language that
admits previously non-terminating examples.\footnote{See the extended version for more examples and information about the implementation. Extended version is available from authors' homepages.} %A prototype is available from \url{https://github.com/fermat/corecursive-type class}.
\textbf{Future Work} In general, the interactions between different loops
can be complicated. Consider $\Phi_{\ensuremath{\Conid{Pair}}}$ with the following
declarations (denoted by $\Phi_M$):
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\Conid{M}\mathbin{:}\Conid{Eq}\;(\Varid{h}_{1}\;(\Conid{M}\;\Varid{h}_{1}\;\Varid{h}_{2})\;(\Conid{M}\;\Varid{h}_{2}\;\Varid{h}_{1})\;\Varid{a})\Rightarrow \Conid{Eq}\;(\Conid{M}\;\Varid{h}_{1}\;\Varid{h}_{2}\;\Varid{a}){}\<[E]%
\\
\>[3]{}\kappa_\Conid{H}\mathbin{:}(\Conid{Eq}\;\Varid{a},\Conid{Eq}\;((\Varid{f}_{1}\;\Varid{a}),(\Varid{f}_{2}\;\Varid{a})))\Rightarrow \Conid{Eq}\;(\Conid{H}\;\Varid{f}_{1}\;\Varid{f}_{2}\;\Varid{a}){}\<[E]%
\\
\>[3]{}\kappa_\Conid{G}\mathbin{:}\Conid{Eq}\;((\Varid{g}\;\Varid{a}),(\Varid{f}\;(\Varid{g}\;\Varid{a})))\Rightarrow \Conid{Eq}\;(\Conid{G}\;\Varid{f}\;\Varid{g}\;\Varid{a}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\begin{figure}[tbp]
\makebox[\textwidth]{
\begin{tikzpicture}[every tree node/.style={},
level distance=1.00cm,sibling distance=.40cm,
edge from parent path={(\tikzparentnode) -- (\tikzchildnode)}, font=\scriptsize]
\Tree [.\node{$\underline{\ensuremath{\Conid{Eq}\;(\Conid{M}\;\Conid{H}\;\Conid{G}\;\Conid{Int})}}_1$};
\edge node[auto=right]{$\kappa_{M}$};
[.\node{\ensuremath{\Conid{Eq}\;(\Conid{H}\;(\Conid{M}\;\Conid{H}\;\Conid{G})\;(\Conid{M}\;\Conid{G}\;\Conid{H})\;\Conid{Int}}};
\edge node[auto=right]{$\kappa_{H}^1$};
[.\node{\ensuremath{\Conid{Eq}\;\Conid{Int}}};
\edge node[auto=right]{$\kappa_{\ensuremath{\Conid{Int}}}$};
[.\node{$\Box$};
]
]
\edge node[auto=right]{$\kappa_H^2$};
[.\node{\ensuremath{\Conid{Eq}\;((\Conid{M}\;\Conid{H}\;\Conid{G}\;\Conid{Int}),(\Conid{M}\;\Conid{G}\;\Conid{H}\;\Conid{Int}))}};
\edge node[auto=right]{$\kappa_{\ensuremath{\Conid{Pair}}}^1$};
[.\node{$\underline{\ensuremath{\Conid{Eq}\;(\Conid{M}\;\Conid{H}\;\Conid{G}\;\Conid{Int})}}_1$};
]
\edge node[auto=right]{$\kappa_{\ensuremath{\Conid{Pair}}}^2$};
[.\node{$\underline{\ensuremath{\Conid{Eq}\;(\Conid{M}\;\Conid{G}\;\Conid{H}\;\Conid{Int})}}_2$};
\edge node[auto=right]{$\kappa_M$};
[.\node{\ensuremath{\Conid{Eq}\;(\Conid{G}\;(\Conid{M}\;\Conid{G}\;\Conid{H})\;(\Conid{M}\;\Conid{H}\;\Conid{G})\;\Conid{Int})}};
\edge node[auto=right]{$\kappa_G$};
[.\node{\ensuremath{\Conid{Eq}\;((\Conid{M}\;\Conid{H}\;\Conid{G}\;\Conid{Int}),(\Conid{M}\;\Conid{G}\;\Conid{H}\;((\Conid{M}\;\Conid{H}\;\Conid{G})\;\Conid{Int})))}};
\edge node[auto=right]{$\kappa_{\ensuremath{\Conid{Pair}}}$};
[.\node{$\underline{\ensuremath{\Conid{Eq}\;(\Conid{M}\;\Conid{H}\;\Conid{G}\;\Conid{Int})}}_1$};
]
\edge node[auto=right]{$\kappa_{\ensuremath{\Conid{Pair}}}$};
[.\node{$\underline{\ensuremath{\Conid{Eq}\;(\Conid{M}\;\Conid{G}\;\Conid{H}\;((\Conid{M}\;\Conid{H}\;\Conid{G})\;\Conid{Int}))}}_2$};
]
]
]
]
]
]
]
\end{tikzpicture}
}
\caption{A Partial Resolution tree for $\Phi_M \vdash \ensuremath{\Conid{Eq}\;(\Conid{M}\;\Conid{H}\;\Conid{G}\;\Conid{Int})} \Uparrow$}
\label{fig:ex4}
\end{figure}
\noindent A partial resolution tree generated by the query \ensuremath{\Conid{Eq}\;(\Conid{M}\;\Conid{H}\;\Conid{G}\;\Conid{Int})} is
described in Figure \ref{fig:ex4}. In this case the cycle (underlined with the
index $1$) is mutually nested with a loop (underlined with index $2$). Our method in
Section \ref{inv} is not able to generate any candidate lemmas. Yet there are two
candidate lemmas for this case (with the proof of $e_2$
refer to $e_1$):
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{e}_{1}\mathbin{:}(\Conid{Eq}\;\Varid{x},\Conid{Eq}\;(\Conid{M}\;\Conid{G}\;\Conid{H}\;\Varid{x}))\Rightarrow \Conid{Eq}\;(\Conid{M}\;\Conid{H}\;\Conid{G}\;\Varid{x}){}\<[E]%
\\
\>[3]{}\Varid{e}_{2}\mathbin{:}\Conid{Eq}\;\Varid{x}\Rightarrow \Conid{Eq}\;(\Conid{M}\;\Conid{G}\;\Conid{H}\;\Varid{x}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\noindent % In order to further extend the method of generating coinductive hypotheses,
We would
like to improve our heuristics to allow generating multiple candidate lemmas, where
their corecursive evidences mutually refer to each other.
There are situations where resolution is non-terminating but does not form any loop such
as $\Phi \vdash A \to^* \mathcal{C}[\sigma A]$. Consider the following program $\Phi_D$:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\kappa_\mathrm{1}\mathbin{:}\Conid{D}\;\Varid{n}\;(\Conid{S}\;\Varid{m})\Rightarrow \Conid{D}\;(\Conid{S}\;\Varid{n})\;\Varid{m}{}\<[E]%
\\
\>[3]{}\kappa_\mathrm{2}\mathbin{:}\Conid{D}\;(\Conid{S}\;\Varid{m})\;\Conid{Z}\Rightarrow \Conid{D}\;\Conid{Z}\;\Varid{m}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\noindent For query \ensuremath{\Conid{D}\;\Conid{Z}\;\Conid{Z}}, the resolution diverges without forming any loop. We would have
to introduce extra equality axioms in order to obtain finite corecursive evidence.\footnote{See the extended version for a solution in Haskell using type family and more discussion.} We would like
to investigate the ramifications of incorporating equality axioms in the corecursive resolution in the future.
%\tom{This is not true, is it? I do have sent you the evidence in terms of type families.}
We plan to extend the observational equivalence result of Section
\ref{ob-equiv} to cope with more general notions of loop and extend our approach to
allow intuitionistic formulas as candidate lemmas.
% ******** say something about extending syntax of CH???********
Another avenue for future work is a formal proof that the calculus of Definition~\ref{def:cresolution} is sound relative to the the greatest Herbrand models~\cite{Llo87},
and therefore reflects the broader notion of the coinductive entailment for Horn clause logic as discussed in the introduction.
\subsection*{Acknowledgements} We want to thank Patricia Johann and the FLOPS reviewers for their helpful
comments, Franti\v sek Farka for many discussions. Part of this work was funded
by the Flemish Fund for Scientific Research.
\bibliographystyle{plain}
\bibliography{paper}
\newpage
\appendix
%===============================================================================
\section{Proof of Theorem \ref{equiv}}\label{app:proof}
% \begin{theorem}
% If $K(\Phi)$ is pure and non-overlapping, then $K(\Phi)$ is confluent.
% \end{theorem}
%% \begin{definition}
%% A mixed term $q$ is solvable if there is a reduction of the shape $q \to^* \kappa \ q_1 ... \ q_n$ for
%% some $q_1,..., q_n$.
%% \end{definition}
%% \begin{definition}
%% We write $[q]_{K(\Phi)}$ to denote a possibly infinite proof term tree such that:
%% \begin{itemize}
%% \item If $q$ is not solvable, then $[q]_{K(\Phi)} (w) = \uparrow$ for any position sequence $w$.
%% \item If $q \to^* \kappa\ q_1 ...\ q_n $, then $[q]_{K(\Phi)} (\epsilon) = \kappa$ and $[q]_{K(\Phi)}(\langle i \rangle + v) = [q_i]_{K(\Phi)}(v)$.
%% \end{itemize}
%% \end{definition}
%% \begin{definition}
%% We write $[q]_{K(\Phi)} \sim [q']_{K(\Phi)'}$ if for any position sequence $w$, $[q]_{K(\Phi)}(w) = [q']_{K(\Phi)'}(w)$.
%% \end{definition}
% \begin{theorem}
% Let $\Phi \vdash B \to^* \mathcal{C}[\sigma B]$ be a simple loop and $||\mathcal{C}|| = \{D_1, ..., D_n\}$.
% \begin{enumerate}
% \item We have $\Phi \vdash D_1, ..., D_n \Rightarrow B \Downarrow \mylet{\alpha = \lambda \alpha_1 .... \lambda \alpha_n . e}{\alpha}$ for some $e$.
% \item Let $\Psi = \Phi, (\alpha : \underline {D} \Rightarrow B) = e$. We have
% \end{enumerate}
% \end{theorem}
\begin{theorem}
Let $\Phi \vdash B \to^* \mathcal{C}[D_1, ..., D_n, \sigma B]$
with $|\mathcal{C}| = \emptyset$ and $D_i$ are normal for all $i$. Suppose $\Phi \vdash \sigma D_i \to^* \mathcal{C}_i[D_i]$, where $| \mathcal{C}_i | = \emptyset$ for any $D_i$. We have the following:
\begin{enumerate}
\item $\Phi \vdash D_1, ..., D_n \Rightarrow B \Downarrow \mu \alpha . \lambda \alpha_1 .... \lambda \alpha_n . e$.
\item Let $e' \equiv \mu \alpha . \lambda \alpha_1 .... \lambda \alpha_n . e$. We have:
$\mathcal{C}'[\sigma^m B] \in \mathcal{O}(B)_{\Phi}$ iff $\mathcal{C}'[e' \ \mathcal{C}_1^m[D_1] ...\ \mathcal{C}_n^m[D_n]] \in \mathcal{S}(e' \ \underline{D})$.
\end{enumerate}
\end{theorem}
\begin{proof}
\begin{enumerate}
\item We have the following finite derivation.
\begin{center}
\[
\begin{array}{c}
\infer{\Phi \vdash \underline{D} \Rightarrow B \Downarrow
\mu \alpha . \lambda \alpha_1 .... \lambda \alpha_n
. e} { \infer{\Phi, \alpha : \underline{D}
\Rightarrow B \vdash \underline{D} \Rightarrow B
\Downarrow \lambda \alpha_1 .... \lambda \alpha_n
. e}{\infer{\Phi, \alpha : \underline{D} \Rightarrow B,
\underline{\alpha} : \underline{D} \vdash B \Downarrow
e}{\infer{...}{}}}}
\end{array} \]
\end{center}
\noindent By Theorem \ref{func:eq}, we just need to reduce $B$ to a proof term using
the rules $\Psi_1 = \Phi, \alpha : \underline{D} \Rightarrow B, \underline{\alpha} : \underline{D}$.
We have the following reduction:
\begin{center}
$ \Psi_1 \vdash B \to^* \mathcal{C}[D_1, ..., D_n, (\sigma B)]
\to^* \mathcal{C}[\alpha_1 ... \alpha_n, (\sigma B)] \to
\mathcal{C}[\alpha_1, ... ,\alpha_n, (\alpha\ (\sigma\ D_1)
... (\sigma\ D_n)) ] \to^* \mathcal{C}[ \alpha_1, ... \alpha_n,
(\alpha\ \mathcal{C}_1[D_1] ... \mathcal{C}_n[D_n])] \to
\mathcal{C}[\alpha_1 ... \alpha_n (\alpha\
\mathcal{C}_1[\alpha_1] ...\ \mathcal{C}_n[\alpha_n])]$
\end{center}
Thus we have the corecursive evidence
$\mu \alpha .\lambda \alpha_1 . .. \alpha_n
. e$ for $ D_1, ...,
D_n \Rightarrow B$, and $e \equiv \mathcal{C}[ \alpha_1, ... \alpha_n, (\alpha\
\mathcal{C}_1[\alpha_1]\ ...\ \mathcal{C}_n[\alpha_n])]$.
\item Using the same notation in (1), let $e' \equiv \mu \alpha .\lambda \alpha_1 . .. \alpha_n
. e$, we can observe following equivalence reduction traces:
\begin{center}
$\Phi \vdash B \to^* \mathcal{C}[D_1, ..., D_n, (\sigma B)] \to^* \mathcal{C}[D_1, ..., D_n, \mathcal{C}[\mathcal{C}_1[D_1], ..., \mathcal{C}_n[D_n], (\sigma^2 B)]] \to ...$
\
$\ (e'\ D_1 ...\ D_n) \leadsto^* \mathcal{C}[ D_1, ... D_n, (e'\ \mathcal{C}_1[D_1]\ ...\ \mathcal{C}_n[D_n])] \leadsto^* \mathcal{C}[ D_1, ..., D_n, \mathcal{C}[ \mathcal{C}_1[D_1], ..., \mathcal{C}_n [D_n], (e'\ (\mathcal{C}_1[\mathcal{C}_1[D_1]])\ ...\ (\mathcal{C}_n[\mathcal{C}_n[D_n]]))]] \leadsto^* ...$
\end{center}
We proceed by induction on $m$. When $m = 0$, it is obvious. Let $m = k + 1$. By IH,
we know that $\mathcal{C}'[\sigma^k B] \in \mathcal{O}(B)_{\Phi}$ iff $\mathcal{C}'[e' \ \mathcal{C}_1^k[D_1] ...\ \mathcal{C}_n^k[D_n]] \in \mathcal{S}(e'\ \underline{D})$. We have $\Phi \vdash \mathcal{C}'[\sigma^k B] \to^* \mathcal{C}'[\mathcal{C}[\sigma^k D_1, ..., \sigma^k D_n, (\sigma^{k+1} B)]] \to^*$
$\mathcal{C}'[\mathcal{C}[\mathcal{C}_n^k[D_1], ..., \mathcal{C}_n^k[D_n], (\sigma^{k+1} B)]]$.
On the other hand, $\mathcal{C}'[e' \ \mathcal{C}_1^k[D_1] ...\ \mathcal{C}_n^k[D_n]] \leadsto^*$
$\mathcal{C}'[\mathcal{C}[\mathcal{C}_n^k[D_1], ..., \mathcal{C}_n^k[D_n], (e' \ \mathcal{C}_1^{k+1}[D_1] ...\ \mathcal{C}_n^{k+1}[D_n])]]$. Thus we have the observational equivalence.
\end{enumerate}
\end{proof}
\section{Weak Head Normalization of Corecursive Evidence}
\label{ap:guard}
\begin{definition}
\label{syntax}
\[
\begin{array}{l@{\hspace{5mm}}l@{\hspace{5mm}}c@{\hspace{5mm}}l}
\text{Formula} & F, G & ::= & A ~\mid~ \forall x . F ~\mid~ \ F \Rightarrow F' \\
\text{Evidence/Proofs} & e & ::= & \kappa ~\mid~ \alpha ~\mid~ \lambda \alpha . e ~\mid~ e \ e' ~\mid~
\mu \alpha . e \\
\text{Contexts/Axioms} & \Phi & ::= & \cdot ~\mid~ e : F, \Phi
\end{array}
\]
% Corecursive evidence definition $\Psi \ ::= \cdot \ || \ \Psi, \alpha \mapsto e$
\end{definition}
We write $ G_1, ..., G_n \Rightarrow
A$ as a shorthand for $ G_1 \Rightarrow ... \Rightarrow
G_n \Rightarrow A$. Note that Horn formulas are special case of formulas.
\begin{definition}
Weak Head reduction context $ \mathcal{C} \ ::= \ \bullet \ | \ \mathcal{C}\ e$
\end{definition}
\begin{definition}[Weak Head Reduction]
\label{label}
\fbox{$ e \leadsto e'$}
\[\begin{array}{c}
\infer{{\mathcal{C}[\mu \alpha . e]} \leadsto_\mu \mathcal{C}[[\mu \alpha . e/\alpha]e]}{}
\quad \quad
\infer{\mathcal{C}[(\lambda \alpha . e) \ e'] \leadsto_\beta \mathcal{C}[[e'/\alpha] e] }{}
\end{array}
\]
\end{definition}
Note that weak head reduction context do not allow reduction under the constant $\kappa$. It is
more restricted than the context in Section \ref{preliminary}.
\begin{definition}[General Corecursive Resolution]
\[\begin{array}{c}
\infer[\text{if}~(e : G_1,..., G_m \Rightarrow A) \in \Phi]
{\Phi \vdash \sigma A \Downarrow \kappa~e_1 \cdots e_n}
{ \Phi \vdash \sigma G_1 \Downarrow e_1 \quad \cdots \quad \Phi \vdash \sigma G_n \Downarrow e_n
}
\\ \\
\infer
{\Phi \vdash F \Downarrow \mu \alpha . e }{\Phi, \alpha : F \vdash F \Downarrow e & \mathrm{HNF}(e)}
\quad\quad
\infer
{\Phi \vdash \underline{G} \Rightarrow B \Downarrow \lambda \underline{\alpha} . e}
{\Phi, \underline{\alpha} : \underline{G} \vdash B \Downarrow e}
\end{array}
\]
\end{definition}
% \begin{definition}[Well-formed Context]
% \[
% \begin{array}{c}
% \infer{\cdot \vdash \mathsf{wf} }{}
% \quad\quad
% \infer{\Phi, \alpha : F \vdash \mathsf{wf} }{\Phi \vdash \mathsf{wf}}
% \quad\quad
% \infer{\Phi, \kappa : F \vdash \mathsf{wf} }{\Phi \vdash \mathsf{wf}}
% \quad\quad
% \infer{\Phi, (\alpha : F) = e \vdash \mathsf{wf} }{\Phi \vdash \mylet{\alpha = e}{\alpha} : F }
% \end{array}
% \]
% \end{definition}
\begin{definition}[Howard's Type System]
\label{proofsystem}
\[
\begin{array}{c}
\infer[(\textsc{Assump})]{\Phi \vdash a : F}{(a : F) \in \Phi}
\quad\quad
\infer[(\textsc{App})]{\Phi \vdash e_2\ e_1 : F}{\Phi \vdash e_1 : F' & \Phi \vdash e_2 : F' \Rightarrow F}
\\
\\
\infer[(\textsc{Abs})]{\Phi \vdash \lambda \alpha.e : F' \Rightarrow F}{\Phi, \alpha : F' \vdash e : F}
\quad\quad
\infer[(\textsc{Gen})]{\Phi \vdash e: \forall x . F}{\Phi \vdash e : F & x \notin \mathrm{FV}(\Phi)}
\\
\\
\infer[(\textsc{Inst})]{\Phi \vdash e : [t/x]F}{\Phi \vdash e : \forall x . F}
\quad\quad
\infer[(\textsc{Mu})]{\Phi \vdash \mu \alpha . e : F}{\Phi, \alpha : F \vdash e : F & \mathrm{HNF}(e)}
\end{array}
\]
\end{definition}
\begin{theorem}
If $\Phi \vdash F \Downarrow e$, then $\Phi \vdash e : F$.
\end{theorem}
\begin{proof}
By induction on the derivation of $\Phi \vdash F \Downarrow e$.
\end{proof}
\begin{comment}
\begin{proof}
By induction on the derivation of $\Phi \vdash F \Downarrow e$.
\noindent \textit{Case.}
\
\infer[\text{if}~(\kappa :\ \Rightarrow A) \in \Phi] {\Phi \vdash
\sigma A \Downarrow \kappa} {}
Obvious.
\noindent \textit{Case.}
\
\infer[\text{if}~(\kappa : G_1,..., G_m \Rightarrow A) \in \Phi, m
\geq 1] {\Phi \vdash \sigma A \Downarrow \kappa~e_1 \cdots e_n} {
\Phi \vdash \sigma G_1 \Downarrow e_1 \quad \cdots \quad \Phi
\vdash \sigma G_n \Downarrow e_n }
By IH, we have $\Phi \vdash e_1 : \sigma G_1 \cdots \Phi \vdash
e_n : \sigma G_n$. Thus by \textsc{Inst} and \textsc{App}, we have
$\Phi \vdash \kappa~e_1 \cdots e_n : \sigma A$.
\noindent \textit{Case.}
\
\infer{\Phi \vdash F \Downarrow \mylet{\alpha = e}{\alpha} }{\Phi,
\alpha : F \vdash F \Downarrow e & \mathrm{HNF}(e)}
By IH, we have $\Phi, \alpha : F \vdash e : F$, thus by
\textsc{Let} rule, we have $\Phi \vdash \mylet{\alpha = e}{\alpha}
: F$.
\noindent \textit{Case.}
\
\infer {\Phi \vdash \underline{G} \Rightarrow B \Downarrow \lambda
\underline{\alpha} . e} {\Phi, \underline{\alpha} :
\underline{G} \vdash B \Downarrow e}
By IH, we have $\Phi, \underline{\alpha} :\underline{G} \vdash e :
B$, thus we can apply \textsc{Abs} rule, which give us $\Phi
\vdash \lambda \underline{\alpha} . e : \underline{G} \Rightarrow
B $.
\end{proof}
\begin{definition}
\
$\phi(\kappa) := \kappa$
$\phi(\alpha) := \alpha$
$\phi(\mylet{\alpha = e}{\alpha}) := \mathbf{fix}(\lambda \alpha
. \phi(e))$
$\phi(\lambda \alpha . e) := \lambda \alpha . \phi(e)$
$\phi( e\ e') := \phi(e)\ \phi(e')$
\end{definition}
\end{comment}
\begin{theorem}
If $\Phi \vdash e : F$, then $e$ is terminating with respect to weak head reduction.
\end{theorem}
\begin{proof} Sketch. The proof is very similar to standard normalization proof for simply typed
lambda calculus. The only tricky rule is the \textsc{Mu} rule:
\
\infer{\Phi \vdash \mu \alpha. e : \underline{G} \Rightarrow A}{\Phi, \alpha : \underline{G} \Rightarrow A \vdash e : \underline{G} \Rightarrow A & \mathrm{HNF}(e)}
\
\noindent We want to show $\mu \alpha. e$ is in the reducible set of type $\underline{G} \Rightarrow A$. Since $e = \lambda \underline{\alpha}. \kappa\ \underline{e}$, we just need to show for any reducible $\underline{u}$ of type $\underline{G}$, we have $(\mu \alpha. e) \ \underline{u}\leadsto_\mu (\lambda \underline{\alpha}. \kappa\ [\mu \alpha. e/\alpha]\underline{e})\ \underline{u}$ is terminating. This is the case due to the expression is
guarded by $\kappa$.
\end{proof}
\section{Examples}
\label{examples}
\input{example.tex}
%%include example.lhs
\begin{comment}
\section{Corecursive Evidence Construction(will be moved to appendix)}
\label{app:corec}
This section describes our procedure to automatically construct corecursive
evidence for invariant formulas. We first generalize Horn formulas to
implicational intuitionistic formulas and then formalize the evidence
construction procedure in terms of Howard's simple type system~\cite{Howard80}.
It is a generalization of resolution by term-matching in
\cite{DBLP:journals/corr/FuK15}. The procedure is shown to be sound with
respect to the simple type system.
The sort of axioms is extended with proof variable annotations $(\alpha:F)$ and corecursive definitions
$(\alpha : F) \mapsto e$. The latter means that $\alpha$ of type $F$ is corecursively defined as
$e$. We write $a$ to mean $\kappa$ or $\alpha$. We write $(a : F) \in \Phi$ to
mean $(\alpha : F) \in \Phi$, $(\kappa : F)\in \Phi$ or $(\alpha : F) \mapsto e
\in \Phi$.
We use Howard's type system because it expresses evidence construction
for a sufficiently rich notion of formulas (e.g., in contrast with the atomic
intuitionistic sequent calculus~\cite{DBLP:journals/corr/FuK15}). We can
easily introduce corecursive evidence with the following permissive
judgement for well-formed contexts.
Here $\mathrm{HNF}(e)$ means that $e$ is in (head normal) form $\lambda
\underline{\alpha}. \kappa \ e'$. This requirement ensures a notion of
productiveness for the corecursive evidence, which is captured in the normalization theorem.
%Above formulation is from \cite{Howard80}. % , the rule $\mathcal{C}$ is extra-logical
% in the sense that with its addition, we do not have strong normalization anymore.
% \begin{definition}[Eta-Equivalence]
% We define eta-reduction $\lambda \alpha. e\ \alpha \to_\eta e$ for $\alpha \notin \mathrm{FV}(e)$. The congruence closure of $\to_\eta$ is denoted by $=_\eta$.
% \end{definition}
% \begin{comment}
% \begin{definition}[Weak Head Reduction]
% \
%
% {\footnotesize
% \begin{tabular}{lllll}
% \\
% \infer{\Phi \vdash \alpha \to_\beta e}{(\alpha \mapsto e) \in \Phi}
% &
%
% &
% \infer{\Phi \vdash (\lambda \alpha . e)\ e' \to_\beta [e'/\alpha]e }{}
%
% &
%
% &
%
% \infer{\Phi \vdash e_1\ e_2 \to_\beta e_1'\ e_2 }{\Phi \vdash e_1 \to_\beta e_1'}
%
% \end{tabular}
% }
% \end{definition}
% \end{comment}
\begin{theorem}
If $\Phi \vdash e : F$ and $\Phi \vdash \mathsf{wf}$, then $e$ is terminating w.r.t. weak head reduction.
\end{theorem}
The proof makes use of standard Tait-Girard reducibility; we elide the details.
Note that the type system does not have the strong normalization property due
to the corecursive definition.
% \begin{comment}
% In order to specify the evidence construction process, we first define a process called \textit{concretization}, which eliminates all the quantifiers in a formula and replaces the quantified variables that occurs at the negative position by dummy constants, these dummy constants are also called \textit{eigenvariables} in the literature. Suppose $F = \forall x_1 ... \forall x_n. F'$, where the root of $F'$ is not a quantifier. We define the fresh instance of $F$, denoted by $\hat{F}$, as $[{y}_n/{x}_n,..., y_1/x_1]F'$, where $y_1,..., y_n$ are fresh variable. We define $\gamma_A F = \sigma \hat{F} $, where for any $ x \in (\mathrm{FV}(\hat{F}) - \mathrm{FV}(A))$, we have $[c_x/x] \in \sigma$ with $c_x$ is a fresh constant.
%
% \begin{definition}[Concretization]
% We recursively define the concretization function $\pi$ and its helper function $\varpi$ as following.
% \begin{itemize}
% \item $\pi(F) = \pi(\hat{F})$.
% \item $\pi(G_1,..., G_n \Rightarrow A) = \varpi(\gamma_A G_1) ,..., \varpi(\gamma_A G_n)\Rightarrow A$
% \item $\varpi(G_1,..., G_n \Rightarrow A) = \pi(G_1),..., \pi(G_n) \Rightarrow A$
% \end{itemize}
% \end{definition}
%
% % \begin{theorem}
% % If $\Phi \vdash e : F$, then $\pi(\Phi) \vdash e : \pi(F)$.
% % \end{theorem}
%
% We say $G$ is the \textit{concretization of $F$ as axiom}, if $G = \pi(F)$. We say $G$ is the
% \textit{concretization of $F$ as query} if $\pi(F \Rightarrow Q) = G \Rightarrow Q$ for some proposition $Q$. Note that the concretization as query is different from concretization as axiom. For example, the formula $\forall x. P(x) \Rightarrow P(x)$, its concretization as query will be $P(c_x) \Rightarrow P(c_x)$, with $c_x$ be a constant, while its concretization as axiom is $P(x) \Rightarrow P(x)$. From now on, we assume all the formulas appeared in the axioms are concretized as axiom and the query will be concretized as query.
%
% \end{comment}
The following definition generalizes the notion of type class context
reduction~\cite{Jones97} to queries in implicational form.
\begin{definition}[Generalized Resolution]\label{context-red}
\[\begin{array}{c}
\infer
{S \uplus \{ (\Phi_i, A')\} \to_a S \cup \{(\Phi_i, \sigma G_1),..., (\Phi_i, \sigma G_m)\}}
{(a : \forall \underline{x} . G_1,..., G_m \Rightarrow A) \in \Phi_i \quad\quad A \mapsto_{\sigma} A'} \\ \\
\infer
{S \uplus \{ (\Phi_i, \forall \underline{x} . \underline{G} \Rightarrow A)\} \to_{\lambda \underline{\alpha}} S \cup \{([\Phi_i, \underline{\alpha} : \gamma \underline{G}], \gamma A) \}}
{\underline{\alpha}~\text{fresh}\quad\quad\gamma = [\underline{c}/\underline{x}]\quad\quad \underline{c}~\text{fresh constants}}
\end{array}
\]
\end{definition}
When the query is an atomic formula, andt the axioms are Horn formulas, then
the first reduction rule above coincides with the usual notion of type class
context reduction. The second reduction rule allows the reduction of
implicational formulas. Note that $\gamma$ in the second reduction rule
replaces the quantified variables $\underline{x}$ with fresh term constants
$\underline{c}$. This corresponds to the treatment of \textit{eigenvariables} in
theorem proving.
The following theorem ensures that successful context reduction gives rise to valid evidence.
\begin{theorem}[Soundness]
\label{soundness}
If $\{(\Phi_1, F_1),..., (\Phi_n, F_n)\} \to^* \emptyset$, then there exist $e_i$ such that $\Phi_i \vdash e_i : F_i$ ($1 \leq i \leq n$).
\end{theorem}
% \begin{comment}
% In practice, we do not want to generate different evidences base on different choices in the context reduction. One way to eliminate this possibility is to require all the axioms are \textit{non-overlapping}. Checking non-overlapping in our generalized setting is more subtle than for Horn formulas. % We define $\varpi_A F = \sigma' F $, where $\mathrm{dom}(\sigma') = \mathrm{FV}(A)$ and $\mathrm{codom}(\sigma')$ are fresh constants.
% Note that $\cup_{\mathrm{multi}}$ denotes multi-set union.
%
%
% \begin{definition}
% We define function $\mathrm{Pos}(F)$ and $\mathrm{Neg}(F)$ to be:
% \begin{itemize}
% \item $\mathrm{Pos}(G_1,..., G_n \Rightarrow A) = \{A\} \cup_{\mathrm{multi}} \mathrm{Neg}(G_1) \cup_{\mathrm{multi}}\ ...\ \cup_{\mathrm{multi}} \mathrm{Neg}(G_n)$
%
% \item $\mathrm{Neg}(G_1,..., G_n \Rightarrow A) = \mathrm{Pos}(G_1) \cup_{\mathrm{multi}}\ ...\ \cup_{\mathrm{multi}} \mathrm{Pos}(G_n)$
% \end{itemize}
% \end{definition}
%
% \begin{definition}[Non-overlapping]
% Given a set of axioms $\Phi$, it is non-overlapping if all the atomic formulas in $\mathrm{Pos}(\Phi)$ have no common instance. % Given a query $F$, it is non-overlapping with $\Phi$ if all the atomic formulas in $\mathrm{Pos}(\Phi) \cup \mathrm{Neg}(F)$ have no common instance.
% \end{definition}
%
% We will see later why we need this generalized notion of non-overlapping condition.
%
% \end{comment}
The generalized context reduction of Definition \ref{context-red} does not
directly generate corecursive evidence. This is tackled in the following
reduction strategy.
\begin{definition}[Corecursive Strategy]
The reduction beginning with $\{([\Phi, \alpha : \forall \underline{x}. \underline{G} \Rightarrow A], \forall \underline{x}. \underline{G} \Rightarrow A)\}$ , where $\alpha$ is fresh, is corecursive if it is of the
form $\{([\Phi, \alpha : \forall \underline{x}.\underline{G} \Rightarrow A], \forall \underline{x}. \underline{G} \Rightarrow A)\} \to_{\lambda \underline{\alpha}}\{([\Phi, \alpha : \forall \underline{x}. \underline{G} \Rightarrow A, \underline{\alpha} : \gamma \underline{G}], \gamma A)\} \to_\kappa\cdot \to^* ...$ where $\underline{\alpha}$ are fresh and $\to_\kappa$ does not appear in $\to^*$. %, after first step, we apply $\to_\alpha$ whenever possible.
\end{definition}
Hence to obtain corecursive evidence for $G$ in $\Phi$, we can use the
corecursive strategy to reduce $\{([\Phi, \alpha : G], G)\}$, where $\alpha$ is
fresh. The following theorem shows that
the corecursive strategy indeed yields well-formed corecursive evidence.
\begin{theorem}
If the reduction path $\{([\Phi, \alpha : \forall \underline{x}. \underline{G} \Rightarrow A], \forall \underline{x}.\underline{G} \Rightarrow A)\} \to^* \emptyset$ is corecursive, then
$\Phi, (\alpha : \forall \underline{x}. \underline{G} \Rightarrow A) \mapsto e \vdash \mathsf{wf}$ for some $e$.
\end{theorem}
% \begin{comment}
% \begin{definition}[Mix Terms]
% $p \ ::= \ (\Phi, F) \ || \ \kappa \ p_1 ... \ p_n \ || \ \alpha \ p_1 ... \ p_n \ || \ \lambda \underline{\alpha} . p$
% \end{definition}
%
% \begin{definition}[Functionalisation]
% Given a set of axioms $\Phi$, we define a set of rewrite rule $K(\Phi)$ by:
%
% \begin{itemize}
% \item $(\Phi, G_1,..., G_n \Rightarrow A) \to_{\lambda} \lambda \alpha_1. ... \lambda \alpha_n . ([\Phi, \alpha_1 : G_1,..., \alpha_n : G_n], A) \in K(\Phi)$, where $n > 0$ and $\alpha_1,..., \alpha_n$ are fresh.
% \item For $\kappa : G_1,..., G_n \Rightarrow A \in \Phi$, we have $ (\Phi, A) \to_{\kappa} \kappa\ (\Phi, G_1)\ ...\ (\Phi, G_n) \in K(\Phi)$.
% \end{itemize}
% \end{definition}
%
% \begin{theorem}
% $\{(\Phi, F)\} \to^* \emptyset$ iff $(\Phi, F) \to^* e$ for some proof term $e$ such that $\Phi \vdash e : F$.
% \end{theorem}
%
%
%
% With the non-overlapping condition, we can obtain the following confluent result. The confluent of the generalized context reduction guarantees that the evidence we obtained will always be unique.
%
% \begin{theorem}
% If $\Phi$ is non-overlapping, then the generalized context reduction using $\Phi$ is confluent.
% \end{theorem}
%
% % For an invariant formula $F$ is necessarily overlapped with one axiom $\kappa$, let $ \Phi' = (\Phi - \{\kappa\})\cup \{F\}$, we need to ensure $F$ is non-overlapping with $\Phi'$.
% Now let us see why we want to ensure the generalized notion of non-overlapping. Because potential overlapped in this generalized setting is subtle, consider the following program:
%
% $\kappa_1 : ((A \Rightarrow B) \Rightarrow B) \Rightarrow B$
%
% $\kappa_2 :\ \Rightarrow A$
%
% \noindent The heads of $\kappa_1, \kappa_2$ do not overlapped. Consider query $B$, there exist two distinct proofs using the corecursive strategy: $\kappa_1\ (\lambda \alpha . \alpha\ \kappa_2) : B$ and $(\alpha_1 : B) \mapsto \kappa_1 \ (\lambda \alpha . \alpha_1)$. As we see one proof is finite while the other is infinite, this is undesirable in practice. This phenomenon is due to overlapping, since $\mathrm{Pos}(((A \Rightarrow B) \Rightarrow B) \Rightarrow B) = \{ B, B\}$.
%
% The following theorem shows that Paterson's condition can be used to ensure the termination of the corecursive evidence construction.
% \begin{theorem}
% \label{termination}
% If $F$ is an invariant formula for $\kappa \in \Phi$ and $\Phi - \{\kappa\}$ satisfies Paterson's condition, then $\{([\Phi, \alpha : F], F)\}$ is terminating by the corecursive strategy.
% \end{theorem}
% \end{comment}
As an example, let us consider the following axioms $\Phi$:
\[
\begin{array}{lcrcl}
\kappa_1 &:& \mathrm{Eq}\ (f\ (\mathrm{Mu}\ f)\ a) &\Rightarrow& \mathrm{Eq}\ (\mathrm{Mu}\ f\ a) \\
\kappa_2 &:& (\mathrm{Eq}\ a, \mathrm{Eq}\ (f\ (\mathrm{Pair}\ a\ a))) &\Rightarrow& \mathrm{Eq}\ (\mathrm{HPTree}\ f\ a) \\
\kappa_3 &:& (\mathrm{Eq}\ a, \mathrm{Eq}\ b) &\Rightarrow& \mathrm{Eq}\ (\mathrm{Pair}\ a\ b) \\
\kappa_4 &:&\ &\Rightarrow& \mathrm{Eq} \ \mathrm{Unit}
\end{array}
\]
\noindent Note that $f, a, b$ are variables. The concretization of the invariant formula ${Eq}\ x \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ x)$ as query (resp. as axiom) is ${Eq}\ {C} \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ {C})$ (resp. ${Eq}\ x \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ x)$), where ${C}$ is a dummy constant. % Let $Q$ be a unique proposition, the positive atomic formulas in $(({Eq}\ x \Rightarrow {Eq}\ ({C}\ x)) \Rightarrow {Eq}\ ({Fix}\ {C}\ {Pair})) \Rightarrow Q$ are $\{Q, {Eq}\ ({C}\ x)\}$, which is non-overlapping with $\Phi$.
Let $\Phi' = \Phi, \alpha : {Eq}\ x \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ x)$. We have the following terminating context reduction:
{\footnotesize
\begin{center}
$\{(\Phi', {Eq}\ {C} \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ {C}))\} \to_{\lambda \alpha_1} $
$\{([\Phi', \alpha_1 :{Eq}\ {C}], {Eq}\ ({Mu}\ {HPTree}\ {C}))\} \to_{\kappa_1}$
$\{([\Phi', \alpha_1 : {Eq}\ {C}], {Eq}\ ({HPTree} \ ({Mu}\ {HPTree})\ {C}))\} \to_{\kappa_2}$
$\{([\Phi', \alpha_1 : {Eq}\ {C}], {Eq}\ {C}), ([\Phi', \alpha_1 : {Eq}\ {C}], {Eq}\ ({Mu}\ {HPTree}\ ({Pair}\ {C}\ {C}))\} \to_{\alpha_1}$
$\{([\Phi', \alpha_1 : {Eq}\ {C}], {Eq}\ ({Mu}\ {HPTree}\ ({Pair}\ {C}\ {C}))\} \to_{\alpha}$
$\{([\Phi', \alpha_1 : {Eq}\ {C}], {Eq}\ ({Pair}\ {C}\ {C})\} \to_{\kappa_3}$
$\{([\Phi', \alpha_1 : {Eq}\ {C}], {Eq}\ {C}), ([\Phi', \alpha_1 : {Eq}\ {C}], {Eq}\ {C}) \} \to_{\alpha_1} \cdot \to_{\alpha_1} \emptyset$
\end{center}
}
\noindent We obtain the following corecursive evidence:
\noindent $(\alpha : {Eq}\ x \Rightarrow {Eq}\ ({Mu}\ {HPTree}\ x)) \mapsto \lambda \alpha_1 . \kappa_1\ (\kappa_2\ \alpha_1 \ (\alpha \ (\kappa_3 \ \alpha_1 \ \alpha_1)))$.
\noindent Thus we have evidence $(\alpha \ \kappa_4)$ for query ${Eq}\ ({Mu}\ {HPTree}\ {Unit})$.
\section{Observational Equivalence}
\label{rewrite}
% \begin{comment}
% \textbf{Relation to Term Rewriting.} Assume all the axioms are Horn formulas, due to lack of existantial variable, axioms can be viewed as a set of rewrite rule, for example, $\kappa : A_1,..., A_n \Rightarrow B$ can be viewed as a rewrite
% rule $B \to \kappa\ A_1\ ...\ A_n$, thus resolving the query together with obtaining evidence
% can be reified as the rewrite process on the query. In Section \ref{inv}, the method we use to obtain the invariant formula is closely related to \textit{loop detection} in term
% rewriting. A loop is detected if we observe an abstract reduction of the shape
% $A \to^* \mathcal{C}[\sigma A]$, where $\mathcal{C}$ is some contexts. The notion of abstract representation in Definition \ref{abs:rep} is trying to capture the abstract reduction $A \to^* \mathcal{C}[\sigma A]$.
%
% For us it is not enough to just detect a loop, we also want to introduce
% a \textit{sound} rewrite rule(Horn formula) to terminate this infinite process.
% Assume the atomic formulas $D_1, ..., D_n$ in $\mathcal{C}$
% are irreducible. To ensure
% the soundness of the rewrite rule, it will have to be corecursively provable. One rule
% that we could add in this case is $D_1, ..., D_n \Rightarrow A$, or $A \to \alpha\ D_1 ...\ D_n$, then we would have $A \to^* \mathcal{C}[\sigma A] \to \mathcal{C}[(\alpha\ (\sigma D_1) ... (\sigma D_n))]$. So to terminate this process, we just need to make sure $\sigma D_i$ terminates for
% all $i$. A \textit{simple condition} that one can check is $\sigma D_i \to^* \mathcal{C}_i[D_i]$ for all $i$ with $\mathcal{C}_i$ does not contain any atomic formula other than $D_i$. If this simple condition is met,
% then we can be sure that\footnote{Please see appendix for the proof.}: 1. $D_1, ..., D_n \Rightarrow A$ is corecursively provable. 2. $A$ is terminating with the new rule $A \to \alpha\ D_1 ...\ D_n$. 3. The infinite rewrite process of $A$ corresponds to the infinite unfolding of $\alpha \ D_1 ... \ D_n$ with the corecursive definition of $\alpha$.
% \end{comment}
In this section we show that context reduction can be expressed as first-order term rewriting
of the query $A$ into its proof term. The process involves \emph{mixed} terms, that are
part query and part proof term.
\begin{definition}[Mixed terms]
Mixed terms $q\ ::= \ A \ | \ \alpha \ | \ f_\alpha \ | \ \kappa \ | \ q\ q'$
\end{definition}
Note that $f_\alpha$ is a function symbol uniquely identified by $\alpha$. %\tom{What kind of function symbol?}
% The following is a definition of constructing a rewrite system on the mixed terms from the set of axioms.
%
% We first formalize the type class context reduction as first order rewrite system, then
% we show an \textit{observational equivalence} result for the \textit{simple loop} of context reduction, i.e. the corecursive proof term for the simple loop is an accurate model for the corresponding infinite type class context reduction.
% We assume all the formulas in this section are Horn formulas.
The following definition shows how to construct a term rewrite system on these mixed
terms from a set of axioms.
\begin{definition}[Functionalisation]
\label{label}
We construct a set of rewrite rules $K(\Phi)$ from $\Phi$ as follows:
\begin{itemize}
\item For each $(\kappa : \underline{A} \Rightarrow B) \in \Phi$, we
have $(B \to \kappa \ \underline{A}) \in K(\Phi)$.
\item For each $(\alpha : \underline{A} \Rightarrow B) \mapsto \lambda \underline{\alpha} . e \in \Phi$, we have $B \to f_\alpha \ \underline{A} \in K(\Phi)$ and $f_\alpha\ \underline{\alpha} \to [f_\alpha/\alpha]e \in K(\Phi)$.
\end{itemize}
\end{definition}
Thus $K(\Phi)$ is a set of first order rewrite rules on mixed terms. If $\Phi$ does not contain any corecursive definition, then $K(\Phi)$ is called \textit{pure}.
We define \textit{mixed term context} $\mathcal{C}$ to be the mixed term extended with the symbol $\bullet$ to denote a hole. The notation $\mathcal{C}[q_1, ..., q_n]$ means replacing the holes in $\mathcal{C}$ from left to right with $q_1, ..., q_n$. We conveniently remove duplications in this representation, i.e. $\mathcal{C}[D, D]$ will be represented as $\mathcal{C}[D]$. We write
$K(\Phi) \vdash q \to q'$ if $q \equiv \mathcal{C}[q_1]$, $q' \equiv \mathcal{C}[\sigma r]$ and $ l \to r \in K(\Phi)$ with $l \mapsto_\sigma q_1$.
The following theorem formalize the intuition that context reduction can be viewed as a rewriting process.
\begin{theorem}
\label{func:eq}
Assume $K(\Phi)$ is pure and non-overlapping. $ \{(\Phi, A)\} \to^* \emptyset$ iff $K(\Phi) \vdash A \to^* q$ where $q$ is a proof term.
\end{theorem}
We know that if $A \to^* \mathcal{C}[\sigma A]$, then the reduction loops. We use $|\mathcal{C}|$ to denote the set of atomic formulas in the context $\mathcal{C}$. If
for any $D \in |\mathcal{C}|$, $D$ is in normal form, then we call $\mathcal{C}$ a \textit{normal context}.
\begin{definition}[Simple Loop]
Let $|\mathcal{C}| = \{ D_1, ..., D_n\}$ be a normal context and $K(\Phi) \vdash B \to^* \mathcal{C}[\sigma B]$. If for any $D_i$, $K(\Phi) \vdash \sigma D_i \to^* \mathcal{C}_i[D_i]$ with $| \mathcal{C}_i | = \emptyset$, then we call $K(\Phi) \vdash B \to^* \mathcal{C}[\sigma B]$(or just $K(\Phi) \vdash B$ ) a simple loop.
\end{definition}
% \begin{definition}[Direct Corecursion]
% Let $||\mathcal{C}|| = \{ D_1, ..., D_n\}$ be a normal context and $K(\Phi) \vdash B \to^* \mathcal{C}[(f_\alpha\ q_1 ...\ q_n)]$, where $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$. If for any $D_i$, $K(\Phi) \vdash \sigma D_i \to^* \mathcal{C}_i[D_i]$ with $|| \mathcal{C}_i || = \emptyset$, then we call $K(\Phi) \vdash B \to^* \mathcal{C}[(f_\alpha\ q_1 ...\ q_n)]$(or just $K(\Phi) \vdash B$ ) a direct corecurion.
% \end{definition}
We use $\mathcal{R}(A)_{K(\Phi)}$ to denote the set of mixed terms reachable from $A$, i.e. $q \in \mathcal{R}(A)_{K(\Phi)}$ iff $K(\Phi) \vdash A \to^* q$.
\begin{definition}[Observational Point]
\label{observe}
Let $K(\Phi) \vdash B \to^* \mathcal{C}[\sigma B]$ be a simple loop and $q \in \mathcal{R}(B)_{K(\Phi)}$.
We call $q$ an observational point if it is of the form $\mathcal{C}'[\sigma^m B]$, for some $\mathcal{C}'$ such that $|\mathcal{C}' | = | \mathcal{C} |$ and $m \geq 1$.
\end{definition}
We use $\mathcal{O}(A)_{K(\Phi)}$ to denote the set of observational points in $\mathcal{R}(A)_{K(\Phi)}$.
Intuitively, the infinite rewrite process using the pure rules means the proof evidence for the query will be an infinite first order proof term, while most of the time the computation (weak head reduction) only uses/observes finite part of this infinite term, these finite parts are formalized as contexts $\mathcal{C}'$ of the observational points in Definitition \ref{observe}.
%$K(\Phi) \vdash B \to^* \mathcal{C}[q]$ with $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$ and
\begin{definition}[Corecursive Point]
Let $q \in \mathcal{R}(B)_{K(\Phi)}$. We call $q$ a corecursive point if it is of the form $\mathcal{C}[ f_\alpha \ q_1 ...\ q_n]$, where $\mathcal{C}$ is normal, $|\mathcal{C}| \not = \emptyset$, and there
is a rule $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$ with $f_\alpha$ occurs in $e$.
\end{definition}
We use $\mathcal{S}(A)_{K(\Phi)}$ to denote the set of corecursive points in $\mathcal{R}(A)_{K(\Phi)}$. If we
have a corecursive rewrite rule $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$, we can applying
this rule infinitely, thus for the same intuition as observational points, we can define corecursive points
to capture the finite contexts.
% We extend the mixed term with lambda abstraction $\lambda \alpha . q$ and extend the functionalisation of
% $\alpha : A_1, ..., A_n \Rightarrow B \mapsto e$ to be $B \to \alpha \ A_1 ...\ A_n$ and $\alpha \to e$. The reduction
% will be extended with beta reduction.
% \begin{definition}[Trace equivalence]
% Let $\Psi_1 \vdash B$ and $\Psi_2 \vdash B$ be two simple loops. They are called trace equivalence iff
% $\mathcal{O}(B)_{\Psi_1} = \mathcal{O}(B)_{\Psi_2}$.
% \end{definition}
The following theorem shows that if the pure rewrite rules give rise to a simple loop, then we can obtain a
corecursive proof term (Theorem \ref{ob:equiv} (1)) such that the original infinite trace of reduction is observationally equivalent to the infinite trace generated by the corecursive proof term (Theorem \ref{ob:equiv} (2)).
\begin{theorem}
\label{ob:equiv}
Assume $K(\Phi)$ is pure and non-overlapping. Let $K(\Phi) \vdash B \to^* \mathcal{C}[D_1, ..., D_n, \sigma B]$
with $|\mathcal{C}| = \emptyset$ and $D_i$ are normal for all $i$. Suppose $K(\Phi) \vdash \sigma D_i \to^* \mathcal{C}_i[D_i]$, where $| \mathcal{C}_i | = \emptyset$ for any $D_i$. We have the following:
\noindent \textit{1.} $D_1, ..., D_n \Rightarrow B$ is corecursively provable by some corecursive definition $\alpha \mapsto \lambda \alpha_1 .... \lambda \alpha_n . e$.
\noindent \textit{2.} Let
$\Psi_1 = (K(\Phi) - \{ E' \to \kappa \ E_1 ... \ E_l \}) \cup \{ f_\alpha \ \alpha_1 ... \ \alpha_n \to [f_\alpha/\alpha] e, B \to f_\alpha\ D_1 ...\ D_n \}$, where $\kappa : E_1, ..., E_l \Rightarrow E' \in \Phi$ with $E' \mapsto_\sigma B$. We have: $\mathcal{C}'[\sigma^m B] \in \mathcal{O}(B)_{K(\Phi)}$ iff $\mathcal{C}'[f_\alpha \ \mathcal{C}_1^m[D_1] ...\ \mathcal{C}_n^m[D_n]] \in \mathcal{S}(B)_{\Psi_1}$, where $m \geq 1$.
\end{theorem}
For example, consider the following rewrite rule $K(\Phi)$:
\begin{center}
$Eq\ ({Mu}\ f\ a) \to \kappa_1\ ({Eq}\ (f\ ({Mu}\ f)\ a))$
${Eq}\ ({HPTree}\ f\ a) \to \kappa_2 ({Eq}\ a) \ ({Eq}\ (f\ ({Pair}\ a\ a)))$
${Eq}\ ({Pair}\ a\ b) \to \kappa_3\ ({Eq}\ a)\ ({Eq}\ b) $
% ${Eq} \ {Unit} \to \kappa_4$
\end{center}
\noindent We can dectect the following simple loop (with subterm of observational points underlined):
{\scriptsize
\begin{center}
$K(\Phi) \vdash {Eq}\ ({Mu}\ {HPTree} \ x) \to \kappa_1\ ({Eq}\ ({HPTree}\ ({Mu}\ {HPTree})\ x)) \to \kappa_1\ (\kappa_2\ ({Eq}\ x) \ \underline{({Eq}\ ({Mu}\ {HPTree}\ ({Pair}\ x\ x)))}) \to
\kappa_1\ (\kappa_2\ ({Eq}\ x) \ (\kappa_1 \ (Eq \ (HPTree \ (Mu \ HPTree)\ (Pair\ x\ x))))) \to
\kappa_1 (\kappa_2 ({Eq}\ x) (\kappa_1 (\kappa_2 (Eq (Pair\ x\ x)) (Eq (Mu\ HPTree \ (Pair\ (Pair\ x\ x)\ (Pair\ x\ x))))))) \to \kappa_1 (\kappa_2 ({Eq}\ x) (\kappa_1 (\kappa_2 (\kappa_3 (Eq\ x) (Eq\ x))) \underline{(Eq (Mu\ HPTree \ (Pair (Pair\ x\ x) (Pair\ x\ x))))}))) \to ... $
\end{center}
}
\noindent In this case, we have $\sigma = [({Pair}\ x\ x)/x]$ and $\sigma ({Eq}\ x) \to \kappa_3\ ({Eq}\ x)\ ({Eq}\ x)$.
Thus ${Eq}\ a \Rightarrow {Eq}\ ({Mu}\ {HPTree} \ x)$ is provable with the corecursive evidence $\alpha \mapsto \lambda \alpha_1 . \kappa_1\ (\kappa_2\ \alpha_1 \ (\alpha \ (\kappa_3 \ \alpha_1 \ \alpha_1)))$. Thus we can obtain two rewrite rules: $f_\alpha\ \alpha_1 \to \kappa_1\ (\kappa_2\ \alpha_1 \ (f_\alpha \ (\kappa_3 \ \alpha_1 \ \alpha_1)))$ and ${Eq}\ ({Mu}\ {HPTree} \ x) \to f_\alpha \ ({Eq}\ x)$. Let $\Psi = (K(\Phi) - \{Eq\ ({Mu}\ f\ a) \to \kappa_1\ ({Eq}\ (f\ ({Mu}\ f)\ a))\}) \cup \{f_\alpha\ \alpha_1 \to \kappa_1\ (\kappa_2\ \alpha_1 \ (f_\alpha \ (\kappa_3 \ \alpha_1 \ \alpha_1))), {Eq}\ ({Mu}\ {HPTree} \ x) \to f_\alpha \ ({Eq}\ x)\}$. We can observe the following equivalent reduction trace (with corecursive point underlined):
{\scriptsize
\begin{center}
$\Psi \vdash {Eq}\ ({Mu}\ {HPTree} \ x) \to f_\alpha\ ({Eq}\ x) \to
\kappa_1\ (\kappa_2\ ({Eq}\ x) \ \underline{(f_\alpha \ (\kappa_3 \ ({Eq}\ x) \
({Eq}\ x)))}) \to \kappa_1 (\kappa_2 ({Eq}\ x) (\kappa_1 (\kappa_2 (\kappa_3 ({Eq}\ x)
({Eq}\ x)) \ \underline{(f_\alpha (\kappa_3 (\kappa_3 ({Eq}\ x)
({Eq}\ x)) (\kappa_3 ({Eq}\ x) \
({Eq}\ x)) ))})))\to ...$
\end{center}
}
\section{Proof of Theorem \ref{soundness}}
\begin{theorem}
If $\{(\Phi_1, F_1),..., (\Phi_n, F_n)\} \to^* \emptyset$, then $\Phi_1 \vdash e_1 : F_1, ..., \Phi_n \vdash e_n : F_n$.
\end{theorem}
\begin{proof}
By induction on the length of $\to^*$.
\begin{itemize}
\item Base Case: $ \{(\Phi, A)\} \to_{a} \emptyset$ with $a : A' \in \Phi$ and $\sigma A' \equiv A$. In this case, by rules \textit{assump}, \textit{inst}, we have $\Phi \vdash a : A$.
\item Step Case:
\noindent $\{(\Phi_1,F_1),..., (\Phi_i, A_i),..., (\Phi_n, F_n)\} \to_{a}$
\noindent $\{(\Phi, F_1),..., (\Phi_i, \sigma G_1),..., (\Phi_i, \sigma G_m),..., (\Phi_n, F_n)\} \to^* \emptyset$, with $a : \forall \underline{x} . \underline{G} \Rightarrow B \in \Phi_i$ and $\sigma B \equiv A_i$. By IH,
we have $\Phi_1 \vdash e_1 : F_1, ..., \Phi_i \vdash e_1' : \sigma G_1, ..., \Phi_i \vdash e_m' : \sigma G_m, ..., \Phi_n \vdash e_n : F_n$. Since $\Phi_i \vdash a : \sigma \underline{G} \Rightarrow A_i$ by rule \textit{inst}, we have $\Phi_i \vdash a\ e_1' ...\ e_m' : A_i$ by applying rule \textit{app} multiple times.
\item Step Case:
\noindent $\{(\Phi_1, F_1),..., (\Phi_i, \forall \underline{x} . \underline{G} \Rightarrow A),..., (\Phi_n, F_n)\} \to_{\lambda \underline{\alpha}}$
\noindent $\{(\Phi_1, F_1),..., ([\Phi_i, \underline{\alpha} : \gamma \underline{G}], \gamma A),..., (\Phi_n, F_n\} \to^* \emptyset$. Let $\Phi' = \Phi_i, \alpha_1 : \gamma G_1, ..., \alpha_m : \gamma G_m$. By IH, we have $\Phi_1 \vdash e_1 : F_1, ..., \Phi' \vdash e_i : \gamma A,..., \Phi_n \vdash e_n : F_n$. We apply
rule \textit{abs} and rule \textit{gen}, we get $\Phi_i \vdash \lambda \underline{\alpha}. e_i :
\forall \underline{x}. \underline{G} \Rightarrow A$.
\end{itemize}
\end{proof}
\section{Multi-Loop and Experiments(Will not be included in submission.)}
\begin{theorem}
\label{provability}
Assume $\Phi$ is pure and non-overlapping. Let $|\mathcal{C}| = \emptyset$ and $K(\Phi) \vdash B \to^* \mathcal{C}[D_1, ..., D_n, \sigma_1 B, ..., \sigma_m B]$, where $D_i$ are normal for all $i$. Assume $E \to q \in K(\Phi)$ with $\sigma E \equiv B$, let $\Psi = (K(\Phi) - \{E \to q\}) \cup \{B \to f_\alpha \ D_1 ... \ D_n \}$. For any $D_i$, $\sigma_j$, we have $\Psi \vdash \sigma_j D_i \to^* \mathcal{C}_{j, i}[D_i]$ with $| \mathcal{C}_{j, i} | = \emptyset$. Note that $\mathcal{C}_{j, i}$ may contain $f_\alpha$. We have the following:
\noindent $D_1, ..., D_n \Rightarrow B$ is corecursively provable by some corecursive definition $\alpha \mapsto \lambda \alpha_1 .... \lambda \alpha_n . e$.
\end{theorem}
\begin{proof}
we just need to corecursively reduce $B$ to a proof term by
the rewrite rules $\Psi = K(\Phi) \cup \{B \to f_\alpha\ D_1\ ...\ D_n, D_1
\to \alpha_1, ..., D_n \to \alpha_n\}$. We have the following reduction:
\begin{center}
$ \Psi \vdash B \to^* \mathcal{C}[D_1, ..., D_n, (\sigma_1 B), ...,(\sigma_m B) ]
\to^* \mathcal{C}[\alpha_1 ... \alpha_n, (\sigma_1 B), ...,(\sigma_m B)] \to^*
\mathcal{C}[\alpha_1, ... ,\alpha_n, (f_\alpha\ (\sigma_1\ D_1)
... (\sigma_1\ D_n)), ..., (f_\alpha\ (\sigma_m\ D_1)
... (\sigma_m\ D_n)) ] \to^* \mathcal{C}[ \alpha_1, ... \alpha_n,
(f_\alpha\ \mathcal{C}_{1,1}[D_1] ..., \mathcal{C}_{1, m}[D_n]), ..., (f_\alpha\ \mathcal{C}_{m,1}[D_1] ..., \mathcal{C}_{m,n}[D_n])] \to^* \mathcal{C}[ \alpha_1, ... \alpha_n,
(f_\alpha\ \mathcal{C}_{1,1}[\alpha_1] ..., \mathcal{C}_{1, m}[\alpha_n]), ..., (f_\alpha\ \mathcal{C}_{m,1}[\alpha_1] ..., \mathcal{C}_{m,n}[\alpha_n])] $
\end{center}
So we have $f_\kappa \ \alpha_1 ... \alpha_n \to \mathcal{C}[ \alpha_1, ... \alpha_n,
(f_\alpha\ \mathcal{C}_{1,1}[\alpha_1] ..., \mathcal{C}_{1, m}[\alpha_n]), ..., (f_\alpha\ \mathcal{C}_{m,1}[\alpha_1] ..., \mathcal{C}_{m,n}[\alpha_n])]$
\end{proof}
\begin{definition}[Finitely descends]
We say $D$ can be (finitely) descended to $B$ (by $\sigma$) if there exist a finite
sequence of syntatic equalities: $\sigma D \equiv \delta_1 B$, $\delta_1 D \equiv \delta_2 B$, $\delta_2 D \equiv \delta_3 B$ ..., $\delta_{n-1} D \equiv \delta_n B$ such that $\delta_n$ is identity. We call such $n$ the descending depth.
\end{definition}
\begin{definition}[Multi-Loop]
Let $|\mathcal{C}| = \{ D_1, ..., D_n\}$ be a normal context and $K(\Phi) \vdash B \to^* \mathcal{C}[\sigma_1 B, ..., \sigma_m B]$. If for any $\sigma_j$, $D_i$, either $D_i$ can be descended to $B$ by $\sigma_j$, or $\sigma_j D_i \to^* \mathcal{C}_{j,i}[D_i] $, with $| \mathcal{C}_{j, i} | = \emptyset$, then we call $K(\Phi) \vdash B \to^* \mathcal{C}[\sigma_1 B, ..., \sigma_m B]$(or just $K(\Phi) \vdash B$ ) a multi-loop.
\end{definition}
\begin{definition}[Generalized Observational Point]
Let $K(\Phi) \vdash B \to^* \mathcal{C}[\sigma_1 B, ..., \sigma_m B]$ be a loop and $q \in \mathcal{R}(B)_{K(\Phi)}$.
We call $q$ an observational point if it is of the form $\mathcal{C}'[\theta_1 B, ..., \theta_n B]$, where $\theta_i$ is a substitution and $|\mathcal{C}' | = | \mathcal{C} |$.
\end{definition}
We use $\mathcal{O}(A)_{K(\Phi)}$ to denote the set of observational points in $\mathcal{R}(A)_{K(\Phi)}$.
% $K(\Phi) \vdash B \to^* \mathcal{C}[q]$ with $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$ and
Note that in this section we assume outer-most reduction strategy, the trace equivalence will
fail if we use innermost strategy, a counter example is \texttt{DList}.
\begin{definition}[Generalized Corecursive Point]
Let $q \in \mathcal{R}(B)_{K(\Phi)}$. We call $q$ a corecursive point if it is of the form
\noindent $\mathcal{C}[ (f_\alpha \ q_{1, 1} ...\ q_{1, n}), ..., (f_\alpha \ q_{m, 1} ...\ q_{m, n})]$, where $\mathcal{C}$ is normal, $|\mathcal{C}| \not = \emptyset$, and there
is a rule $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$ with $f_\alpha$ occurs in $e$.
\end{definition}
We use $\mathcal{S}(A)_{K(\Phi)}$ to denote the set of corecursive points in $\mathcal{R}(A)_{K(\Phi)}$.
\begin{theorem}
Assume $\Phi$ is pure and non-overlapping. Let $|\mathcal{C}| = \emptyset$ and $K(\Phi) \vdash B \to^* \mathcal{C}[D_1, ..., D_n, \sigma_1 B, ..., \sigma_m B]$, where $D_i$ are normal for all $i$. Assume $E \to q \in K(\Phi)$ with $\sigma E \equiv B$, For any $\sigma_j$, $D_i$, either $K(\Phi) \vdash \sigma_j D_i \to^* \mathcal{C}_{j, i}[D_i]$ with $| \mathcal{C}_{j, i} | = \emptyset$, or $D_i$ can be descended to $B$ by $\sigma_j$. We have the following:
\
\noindent $D_1, ..., D_n \Rightarrow B$ is corecursively provable by some corecursive definition $\alpha \mapsto \lambda \alpha_1 .... \lambda \alpha_n . e$.
\end{theorem}
\begin{proof}
Let $\Psi = K(\Phi) \cup \{B \to f_\alpha\ D_1\ ...\ D_n, D_1 \to \alpha_1, ..., D_n \to \alpha_n\}$
and $\Psi' = \Psi - \{E \to q\}$.
We want to show that if $D_i$ can be descended to $B$ by $\sigma_j$ with depth $l$, then
$\Psi' \vdash \sigma_j D_i \to^* \mathcal{C}_{j, i}[f_\alpha ]$
\end{proof}
\begin{definition}[Generalized Observational Point]
Let $K(\Phi) \vdash B \to^* \mathcal{C}[\sigma_1 B, ..., \sigma_m B]$ be a loop and $q \in \mathcal{R}(B)_{K(\Phi)}$.
We call $q$ an observational point if it is of the form $\mathcal{C}'[\theta_1 B, ..., \theta_n B]$, where $\theta_i$ is a substitution and $|\mathcal{C}' | = | \mathcal{C} |$.
\end{definition}
% We use $\mathcal{O}(A)_{K(\Phi)}$ to denote the set of observational points in $\mathcal{R}(A)_{K(\Phi)}$.
%$K(\Phi) \vdash B \to^* \mathcal{C}[q]$ with $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$ and
Note that in this section we assume outer-most reduction strategy, the trace equivalence will
fail if we use innermost strategy, a counter example is \texttt{DList}.
\begin{definition}[Generalized Corecursive Point]
Let $q \in \mathcal{R}(B)_{K(\Phi)}$. We call $q$ a corecursive point if it is of the form
\noindent $\mathcal{C}[ (f_\alpha \ q_{1, 1} ...\ q_{1, n}), ..., (f_\alpha \ q_{m, 1} ...\ q_{m, n})]$, where $\mathcal{C}$ is normal, $|\mathcal{C}| \not = \emptyset$, and there
is a rule $f_\alpha \ \alpha_1 ... \ \alpha_n \to e \in K(\Phi)$ with $f_\alpha$ occurs in $e$.
\end{definition}
We use $\mathcal{S}(A)_{K(\Phi)}$ to denote the set of corecursive points in $\mathcal{R}(A)_{K(\Phi)}$.
\begin{conjecture}
\
\noindent In Theorem \ref{provability}, the observational points $\mathcal{O}(B)_{K(\Phi)}$ and the corecusive points $\mathcal{S}(B)_{\Psi'}$ coincide, where $\Psi' = (K(\Phi) - \{E \to q\}) \cup \{B \to f_\alpha \ D_1 ... \ D_n , f_\alpha \ \alpha_1 ... \ \alpha_n \to e\}$.
\end{conjecture}
\end{comment}
\end{document}
In this section, we show several examples with the prototype that we developed. They are
also available from the \texttt{examples} directory in \url{https://github.com/Fermat/corecursive-type-class}.
\subsection{Example 1}
\begin{verbatim}
module bush where
axiom (Eq a, Eq (f (f a))) => Eq (HBush f a)
axiom Eq (f (Mu f) a) => Eq (Mu f a)
axiom Eq Unit
auto Eq (Mu HBush Unit)
\end{verbatim}
The keyword \texttt{axiom} introduces an axiom and the keyword \texttt{auto}
requests the system to prove the formula automatically using the heuristic
corecursive hypothesis generation that we described in Section \ref{inv}. If we
save the above code in the \texttt{bush.asl} file, and, at the command line, type
\texttt{asl bush.asl}, then we get the following output:
\begin{verbatim}
Parsing success!
Type Checking success!
Program Definitions
Ax0 :: (Eq (f (Mu f) a)) => Eq (Mu f a)
= Ax0
Ax1 :: (Eq a, Eq (f (f a))) => Eq (HBush f a)
= Ax1
Ax2 :: Eq Unit
= Ax2
genLemm4 :: (Eq var_1) => Eq (Mu HBush var_1)
= \ b0 . Ax0 (Ax1 b0 (genLemm4 (genLemm4 b0)))
goalLem3 :: Eq (Mu HBush Unit)
= genLemm4 Ax2
Axioms
Ax2 :: Eq Unit
Ax1 :: (Eq a, Eq (f (f a))) => Eq (HBush f a)
Ax0 :: (Eq (f (Mu f) a)) => Eq (Mu f a)
Lemmas
goalLem3 :: Eq (Mu HBush Unit)
genLemm4 :: (Eq var_1) => Eq (Mu HBush var_1)
\end{verbatim}
The corecursive hypothesis generated is \texttt{genLemm4 :: (Eq var\string_1) => Eq (Mu HBush var\string_1)}, its proof is \texttt{\string\ b0 . Ax0 (Ax1 b0 (genLemm4 (genLemm4 b0)))}. The proof
for \texttt{Eq (Mu HBush Unit)} is \texttt{genLemm4 Ax2}.
Using \texttt{axiom} and \texttt{auto} allows us to quickly experiment with
different small examples. Here is the corresponding type-class code.
\begin{verbatim}
module bush where
data Unit where
Unit :: Unit
data Maybe a where
Nothing :: Maybe a
Just :: a -> Maybe a
data Pair a b where
Pair :: a -> b -> Pair a b
data HBush f a where
HBLeaf :: HBush f a
HBNode :: a -> (f (f a)) -> HBush f a
data Mu f a where
In :: f (Mu f) a -> Mu f a
data Bool where
True :: Bool
False :: Bool
class Eq a where
eq :: Eq a => a -> a -> Bool
and = \ x y . case x of
True -> y
False -> False
instance => Eq Unit where
eq = \ x y . case x of
Unit -> case y of
Unit -> True
instance Eq a, Eq (f (f a)) => Eq (HBush f a) where
eq = \ x y . case x of
HBLeaf -> case y of
HBLeaf -> True
HBNode a c -> False
HBNode a c1 -> case y of
HBLeaf -> False
HBNode b c2 -> and (eq a b) (eq c1 c2)
instance Eq (f (Mu f) a) => Eq (Mu f a) where
eq = \ x y . case x of
In s -> case y of
In t -> eq s t
term1 = In HBLeaf
term2 = In (HBNode Unit term1)
test = eq term2 term1
test1 = eq term2 term2
reduce test
reduce test1
\end{verbatim}
Inspecting the output of this code, we see that the result of the evaluation of
\texttt{test} (resp. \texttt{test1}) is \texttt{False} (resp. \texttt{True}). It is quite
verbose and probably irrelevant to see the type-class code, so in the following
we will show examples using only the \texttt{axiom}, \texttt{auto} and \texttt{lemma} keywords.
\subsection{Example 2}
\begin{verbatim}
module lam where
axiom Eq (f (Mu f) a) => Eq (Mu f a)
axiom (Eq a, Eq (f a), Eq (f a), Eq (f (Maybe a))) => Eq (HLam f a)
axiom Eq Unit
axiom Eq a => Eq (Maybe a)
lemma (Eq x) => Eq (Mu HLam x)
lemma Eq (Mu HLam Unit)
\end{verbatim}
Of course, our heuristic \texttt{auto Eq (Mu HLam Unit)} also works for this case. But
we can specify the corecursive hypothesis as lemma and guided our mini-prover to prove the
final goal \texttt{Eq (Mu HLam Unit)}.
\subsection{Example 3}
Are there any examples where \texttt{auto} fails, but where we can come to the rescue with a \texttt{lemma}?
The answer is yes.
\begin{verbatim}
axiom (Eq a, Eq (Pair (f1 a) (f2 a))) => Eq (H1 f1 f2 a)
axiom Eq (Pair (g a) (f (g a))) => Eq (H2 f g a)
axiom Eq (h1 (Mu h1 h2) (Mu h2 h1) a) => Eq (Mu h1 h2 a)
axiom (Eq a, Eq b) => Eq (Pair a b)
axiom Eq Unit
auto Eq (Mu H1 H2 Unit)
\end{verbatim}
If we run this code, our mini-prover diverges, since this example require multiple lemmas
in order to prove the final goal \texttt{Eq (Mu H1 H2 Unit)}.
\begin{verbatim}
axiom (Eq a, Eq (Pair (f1 a) (f2 a))) => Eq (H1 f1 f2 a)
axiom Eq (Pair (g a) (f (g a))) => Eq (H2 f g a)
axiom Eq (h1 (Mu h1 h2) (Mu h2 h1) a) => Eq (Mu h1 h2 a)
axiom (Eq a, Eq b) => Eq (Pair a b)
axiom Eq Unit
lemma (Eq x, Eq (Mu H2 H1 x)) => Eq (Mu H1 H2 x)
lemma Eq x => Eq (Mu H2 H1 x)
lemma Eq (Mu H1 H2 Unit)
\end{verbatim}
\subsection{Example 4}
\label{DZ}
Are there any examples where even \texttt{lemma} does not work? We believe that
the following is such an example.
\begin{verbatim}
axiom D n (S m) => D (S n) m
axiom D (S m) Z => D Z m
\end{verbatim}
Note that \texttt{auto D Z Z} will not work because the corecursive hypothesis
generated by our method is not provable. The following is a solution in Haskell
using type families. We want to point out that using type families is a way to
introduce equality axioms for addition, and these equality axioms are not
derivable from the original axioms. The ability to learn addition seems to
require a higher notion of intelligence.
\begin{verbatim}
{-# LANGUAGE Rank2Types, TypeFamilies, UndecidableInstances #-}
data Z
data S n
data D a b
type family Add m n
type instance Add n Z = n
type instance Add m (S n) = Add (S m) n
k1 :: D n (S m) -> D (S n) m
k1 = undefined
k2 :: D (S m) Z -> D Z m
k2 = undefined
f :: (forall n. D n (S m) -> D (S (Add m n)) Z) -> D Z m
f g = k2 (g (f (g . k1)))
\end{verbatim}
\begin{thebibliography}{10}
\bibitem{AnconaLagorio11}
D.~Ancona and G.~Lagorio.
\newblock Idealized coinductive type systems for imperative object-oriented
programs.
\newblock {\em RAIRO - Theory of Information and Applications}, 45(1):3--33,
2011.
\bibitem{bird1998nested}
R.~Bird and L.~Meertens.
\newblock Nested datatypes.
\newblock In {\em Mathematics of program construction}, pages 52--67. Springer,
1998.
\bibitem{BjornerGMR15}
N.~Bj{\o}rner, A.~Gurfinkel, K.~L. McMillan, and A.~Rybalchenko.
\newblock Horn clause solvers for program verification.
\newblock In {\em Fields of Logic and Computation {II}}, volume 9300 of {\em
Lecture Notes in Computer Science}, pages 24--51. Springer, 2015.
\bibitem{coquand1994infinite}
T.~Coquand.
\newblock Infinite objects in type theory.
\newblock In {\em Types for Proofs and Programs}, pages 62--78. Springer, 1994.
\bibitem{dershowitz1987}
N.~Dershowitz.
\newblock Termination of rewriting.
\newblock {\em Journal of symbolic computation}, 1987.
\bibitem{FuK15}
P.~Fu and E.~Komendantskaya.
\newblock A type-theoretic approach to resolution.
\newblock In {\em 25th International Symposium, LOPSTR 2015. Revised Selected
Papers}, 2015.
\bibitem{GH05}
J.~Gibbons and G.~Hutton.
\newblock Proof methods for corecursive programs.
\newblock {\em Fundamenta Informaticae Special Issue on Program
Transformation}, 66(4):353--366, 2005.
\bibitem{gimenez1996}
C.~E. Gimenez.
\newblock Un calcul de constructions infinies et son application a la
v{\'e}rification de syst{\`e}mes communicants.
\newblock 1996.
\bibitem{hinze2001}
R.~Hinze and S.~Peyton-Jones.
\newblock Derivable type classes.
\newblock {\em Electronic notes in theoretical computer science}, 41(1):5--35,
2001.
\bibitem{hughes1999restricted}
J.~Hughes.
\newblock Restricted data types in haskell.
\newblock In {\em Haskell Workshop}, volume~99, 1999.
\bibitem{johann2009haskell}
P.~Johann and N.~Ghani.
\newblock Haskell programming with nested types: A principled approach.
\newblock 2009.
\bibitem{KomendantskayaEtAl15}
P.~{Johann}, E.~{Komendantskaya}, and V.~{Komendantskiy}.
\newblock {Structural Resolution for Logic Programming}.
\newblock In {\em Tech. Communications of ICLP'15}, July 2015.
\bibitem{jones2003qualified}
M.~P. Jones.
\newblock {\em Qualified types: theory and practice}, volume~9.
\newblock Cambridge University Press, 2003.
\bibitem{Jones97}
S.~P. Jones, M.~Jones, and E.~Meijer.
\newblock Type classes: An exploration of the design space.
\newblock In {\em In Haskell Workshop}, 1997.
\bibitem{KJ15}
E.~Komendantskaya and P.Johann.
\newblock Structural resolution: a framework for coinductive proof search and
proof construction in horn clause logic.
\newblock 2015.
\newblock Submitted, http://arxiv.org/abs/1511.07865.
\bibitem{Lammel:2005}
R.~L\"{a}mmel and S.~Peyton-Jones.
\newblock Scrap your boilerplate with class: Extensible generic functions.
\newblock In {\em Proceedings of the Tenth ACM SIGPLAN International Conference
on Functional Programming}, ICFP '05, pages 204--215, New York, NY, USA,
2005. ACM.
\bibitem{Llo87}
J.~W. Lloyd.
\newblock {\em Foundations of logic programming}.
\newblock Springer Science \& Business Media, 1987.
\bibitem{MD97}
L.~S. Moss and N.~Danner.
\newblock On the foundations of corecursion.
\newblock {\em Logic Journal of IGPL}, 5(2):231--257, 1997.
\bibitem{plotkin1970note}
G.~D. Plotkin.
\newblock A note on inductive generalization.
\newblock {\em Machine intelligence}, 1970.
\bibitem{SimonBMG07}
L.~Simon et~al.
\newblock Co-logic programming: Extending logic programming with coinduction.
\newblock In {\em ICLP}, pages 472--483, 2007.
\bibitem{SulzmannDJS07}
M.~Sulzmann, G.~J. Duck, S.~L.~Peyton Jones, and P.~J. Stuckey.
\newblock Understanding functional dependencies via constraint handling rules.
\newblock {\em J. Funct. Program.}, 17(1):83--129, 2007.
\bibitem{wadler1989make}
P.~Wadler and S.~Blott.
\newblock How to make ad-hoc polymorphism less ad hoc.
\newblock In {\em Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on
Principles of programming languages}, pages 60--76. ACM, 1989.
\bibitem{zantema1996non}
H.~Zantema and A.~Geser.
\newblock {\em Non-looping rewriting}.
\newblock Universiteit Utrecht, Faculty of Mathematics \& Computer Science,
1996.
\end{thebibliography}