Published: 13th September 2017 DOI: 10.4204/EPTCS.258 ISSN: 2075-2180

# Proceedings of the First Workshop onCoalgebra, Horn Clause Logic Programming and Types Edinburgh, UK, 28-29 November 2016

Edited by: Ekaterina Komendantskaya and John Power

 Preface Ekaterina Komendantskaya and John Power Extending Coinductive Logic Programming with Co-Facts Davide Ancona, Francesco Dagnino and Elena Zucca 1 Structural Resolution for Abstract Compilation of Object-Oriented Languages Luca Franceschini, Davide Ancona and Ekaterina Komendantskaya 19 Trace and Stable Failures Semantics for CSP-Agda Bashar Igried and Anton Setzer 36 Structural Resolution with Co-inductive Loop Detection Yue Li 52 An Executable Specification of Typing Rules for Extensible Records based on Row Polymorphism (Extended Abstract) Ki Yung Ahn 68 Abstract Compilation for Type Analysis of Object-Oriented Languages (Extended Abstract) Davide Ancona 70 Refinement Types and Higher-Order Constrained Horn Clauses (Extended Abstract) C.-H. Luke Ong and Steven J. Ramsay 72 Category Theoretic Semantics for Logic Programming: Laxness and Saturation (Extended Abstract) John Power 74

# Preface

The Workshop on Coalgebra, Horn Clause Logic Programming and Types was held on the 28-29 November 2016 in Edinburgh. The workshop marked the end of the EPSRC Grant Coalgebraic Logic Programming for Type Inference, by E. Komendantskaya, Heriot-Watt University and J. Power, University of Bath, UK.

The workshop consisted of two parts:
1. Semantics: Lawvere theories and Coalgebra in Logic and Functional Programming
2. Programming languages: Horn Clause Logic for Type Inference in Functional Languages and Beyond
In both cases, Horn Clauses and Logic programming were in focus of the talks and discussions.

Over recent years, there has been considerable research on the semantics of operational aspects of logic programming. The underlying mathematics has often involved coalgebra on a presheaf category or a variant of a presheaf category, with index given by the Lawvere theory generated by a signature. That has much in common with many years of research on the semantics of functional programming.

The combination of coalgebra with Lawvere theories has already led to applied development, and there seems good reason to hope that that will continue, with application to logic and functional programming both separately and in combination with each other. The workshop brought researchers in the area together to compare the techniques they are developing and the problems they are addressing.

Our semantic investigations led to analysis of theorem proving, and that was reciprocated, with theorem proving further influencing our semantics. Theorem proving in turn led us to study type inference, leading to the central applied focus of our work, thus the second topic of the workshop.

The workshop featured six invited and seven regular talks, with topics ranging from Categorical Logic, Semantics, Type Theory, Proof Theory, Programming Languages and Type Inference. We were very fortunate to have six excellent invited speakers in
• John Power from University of Bath with a talk on Categorical Semantics of Logic Programming: Laxness and Saturation,
• Steven Ramsay from Oxford University with a talk on Refinement Types and Higher-Order Constrained Horn Clauses,
• Tarmo Uustalu from Tallinn University with a talk on Comodels and Interaction,
• Claudio Russo from Microsoft Research Cambridge with a talk on Type Classes for the Masses,
• Davide Ancona from University of Genova with a talk on Abstract Compilation for Type Analysis of Object-Oriented Languages, and
• Ki Yung Ahn from Nanyang Technological University with a talk on Relational Specification of Type Systems Using Logic Programming

Extended abstracts of all accepted contributions appeared in the pre-proceedings of the workshop. The present volume contains a selection of full papers, submitted and peer-reviewed after the workshop. The present volume also includes extended abstracts of four invited talks. We thank the authors for their contributions.

The paper Extending Coinductive Logic Programming with Co-Facts by Davide Ancona, Francesco Dagnino and Elena Zucca presents their novel work on extending the syntax of coinductive logic programming. The key idea is in allowing some unit clauses contained in a logic program to be assigned a coinductive interpretation. The paper shows correcteness of the operational semantics of this extension, and presents a prototype implementation.

The paper Structural Resolution for Abstract Compilation of Object-Oriented Languages by Luca Franceschini, Davide Ancona and Ekaterina Komendantskaya shows an application of structural resolution to resolving nonterminating cases of type inference in Java. Structural resolution is an algorithm for coinductive proof inference that arose from earlier work by Komendantskaya and Power on coalgebraic semantics of logic programming.

The paper Trace and Stable Failures Semantics for CSP-Agda by Bashar Igried and Anton Setzer extends a formalisation CSP-Agda of the process algebra CSP in the interactive theorem prover Agda. Agda is a theorem prover based on dependent types. The presented paper proposes a formalisation of the trace semantics and the stable failures semantics of CSP and proves selected algebraic laws of CSP using these semantics.

The paper Structural Resolution with Co-inductive Loop Detection by Yue Li presents an extension of structural resolution with coinductive loop detection, proves soundness of this approach and presents an implementation of the resulting novel inference algorithm.

The papers were peer-reviewed by the Programme Committee consisting of:
• Ki Yung Ahn, Nanyang Technological University, Singapore
• Davide Ancona, University of Genoa, Italy
• Filippo Bonchi, CNRS, ENS de Lyon, France
• Iavor Diatchki, Galois, Inc, USA
• Patricia Johann, Appalachian State University, USA
• Ekaterina Komendantskaya, Heriot-Watt University, Edinburgh, UK
• Clemens Kupke, University of Strathclyde, UK
• J. Garrett Morris, University of Edinburgh, UK
• Fredrik Nordvall Forsberg, University of Strathclyde, UK
• John Power, University of Bath, UK
• Aaron Stump, The University of Iowa, USA
• Niki Vazou, University of California, San Diego, USA
• Joe Wells, Heriot-Watt University, Edinburgh, UK
• Fabio Zanasi, University College London, UK

Many thanks to the Programme Committee and all who helped to organise the event! In particular we are grateful to Morag Jones, June Maxwell, Iain McCrone and Christine McBride for technical and administrative support. Thanks to International Center for Mathematical Sciences for providing an excellent venue for the workshop. We are grateful to EPSRC (grants EP/K031864/1-2, EP/K028243/1) for supporting this research and this workshop. Finally, we are very grateful to all those who supported the workshop by submitting abstracts and attending the meeting.

Ekaterina Komendantskaya and John Power

# An Executable Specification of Typing Rules for Extensible Records based on Row Polymorphism (Extended Abstract)

Ki Yung Ahn ( Nanyang Technological University)

Type inference is perceived as a natural application of logic programming (LP). Natively supported unification in LP can serve as a basic building block of typical type inference algorithms. In particular, polymorphic type inference in the Hindley--Milner type system (HM) and its extensions are known to be succinctly specifiable and executable in Prolog [5,7]. Our previous work [2] demonstrates Prolog specifications of more advanced features of parametric polymorphism beyond HM such as type-constructor polymorphism (TCPoly) (a.k.a. higher-kinded polymorphisim). In addition to typing judgments ($\Delta;\Gamma \vdash t : \tau$), which relate terms ($t$) to types ($\tau$), there are kinding judgements ($\Delta \vdash \tau : \kappa$), which relate types ($\tau$) to kinds ($\kappa$) in such more advanced polymorphic type systems. Execution of our Prolog specification for such a type system (HM+TCpoly) are multi-staged, that is, kinding judgements and typing judgements are executed in separate stages.

In this talk, we demonstrate a specification for typing records, which is one of the most widely supported compound data structures in real-world programming languages. More specifically, we develop a specification of a type system that supports extensible records based on row polymorphism (RowPoly) [3]. We build upon our previous work on HM+TCPoly because the use of rows in record types are similar to supplying type arguments to a type constructor. For instance, a type constructor for polymorphic lists ($\textsf{List} : \star \to \star$) becomes a specific list type (e.g., $\textsf{List Int}: \star$) when it is supplied a type (e.g., $\textsf{Int}:\star$) as its argument. Similarly, the record type constructor ($\textsf{Rec} : \textsf{row} \to \star$) becomes a specific record type (e.g., $\textsf{Rec}\;\{\textit{name}:\textsf{String},\;\textit{age}:\textsf{Int}\} : \star$) when it is supplied a row (e.g., $\{\textit{name}:\textsf{String},\;\textit{age}:\textsf{Int}\}$ : row) as its argument. %% \footnote{Sometimes, the record constructor $\textsf{Rec}$ is made %% invisible in implementations, i.e., $\textsf{Rec}\;\rho$ is abbreviate as $\rho$ to users.} Similarly to a polymorphic list type $(\forall\alpha:\star.\,\textsf{List}\;\alpha)$ that range over any specific instances of lists, a row-polymorphic record type $(\forall\rho:\textsf{row}.\,\textsf{Rec}\;\{\textsf{name}:\textsf{String}\mid\rho\})$ ranges over any record type with the $\textit{name}$ field of type $\textsf{String}$; e.g., $\textsf{Rec}\,\{\textit{name}:\textsf{String}\}$ when $\rho$ instantiates to the empty row $\{\}$, or $\textsf{Rec}\,\{\textit{name}:\textsf{String},\,\textit{age}:\textsf{Int}\}$ when $\rho$ instantiates to $\{\textit{age}:\textsf{Int}\}$.

The extension from HM+TCPoly to HM+TCPoly+RowPoly consists of two aspects. First is structurally propagating the extension to the kind syntax from $\,\kappa ::= \star \mid \kappa \to \kappa\,$ to $\,\kappa ::= \textsf{row} \mid \star \mid \kappa \to \kappa$. The syntax of types and terms need to be extended with rows and records, and the kiding and typing rules for rows and record types need to be added accordingly. Second is on how to implement those additional rules in Prolog. Unlike lists, rows are order-irrelevant, for instance, $\{\textit{name}:\textsf{String},\,\textit{age}:\textsf{Int}\}$ and $\{\textit{age}:\textsf{Int},\,\textit{name}:\textsf{String}\}$ should be considered equivalent. Moreover, type inference involving row-polymorphic types requires unification between rows of unknown size. Unfortunately, Prolog's native unification supports neither order-irrelevant structures nor collections of unknown size effectively. We overcome this limitation of Prolog's unification by implementing a user-defined unification between rows of unknown size, inspired by the Stolzenburg's work [5] on unification between sets of unknown size.

Our type system specifications are self-contained succinct logic programs with minimal dependencies over external libraries or constraint solving systems, as summarized in Table 1 below.
type system size (in 80 col) auxiliary code and extra-logical built-ins used
HM 15 lines \==, copy_term
HM+TCPoly 30 lines DCG related predicates, gensym
HM+TCPoly+RowPoly 45 lines +40 lines of code for row unification, cut (!)
Table 1. Size increase, additional auxiliary code and extra-logical built-ins used in the Prolog specifications of polymorphic type systems extended from HM with TCPoly and RowPoly.
Each extension of a polymorphic feature adds about 15 lines of Prolog code for the new typing rules to handle additional language constructs. In case of RowPoly, we also needed extra 40 lines of auxiliary Prolog code to implement the unification between rows of possibly unknown size. This user defined row unification is only required used once in the specification of the typing rule for applications $\displaystyle \frac{\Gamma \vdash e_1 : A_1 \to B \quad e_2 : A_2 \quad A_1 \overset{\tiny\textsf{row}\,}{=\mathrel{\mkern-3mu}=} A_2}{\Gamma |- (e_1 ~ e_2) : B }$ where $\overset{\tiny\textsf{row}\,}{=\mathrel{\mkern-3mu}=}$ is the type equivalence modulo reordering of row items. The other typing rules may use the usual structural equivalence. Further details of our specification for row polymorphic type system is available on Arxiv [1].

There are mainly two limitations in our approach of using Prolog to develop relational executable specification of type systems. First is the use of extra-logical predicates and meta-programming methods, which makes it difficult to analyze the specification and argue its correctness. Second is the lack of error message (except getting false from Prolog's failure). For future work, we hope to overcome the first limitation by (1) formulating a more limited but principled theory of meta-programming in LP that is suited for specifying multiple levels of typing rules and (2) by supporting basic operations (e.g., first matching lookup in a context, row unification) as primitives of the LP system and separately verify their internal implementation rather than treating as a part of a user provided specification. Regarding the second limitation, there are many work on type error messages for functional languages (e.g., [6]) but needs further research on which of the ideas would be compatible with our approach.

### References

1. Ki Yung Ahn (2017): An Executable Specification of Typing Rules for Extensible Records based on Row Polymorphism. url:https://arxiv.org/abs/1707.07872.
2. Ki Yung Ahn & Andrea Vezzosi (2016): Executable Relational Specifications of Polymorphic Type Systems Using Prolog. In: Functional and Logic Programming: 13th International Symposium, FLOPS 2016, LNCS, Springer International Publishing, pp. 109–125 doi:10.1007/978-3-319-29604-3_8.
3. Benedict R. Gaster & Mark P. Jones (1996): A Polymorphic Type System for Extensible Records and Variants. Technical Report NOTTCS-TR-96-3, Department of Computer Science, University of Nottingham.
4. Martin Odersky, Martin Sulzmann & Martin Wehr (1999): Type Inference with Constrained Types. Theorey and Practice of Object Systems, Volume 5, pp. 33–55, doi:10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4.
5. Frieder Stolzenburg (1996): Membership-Constraints and Complexity in Logic Programming with Sets. In: Frontiers of Combining Systems: First International Workshop, Munich, March 1996, Springer Netherlands, Dordrecht, pp. 285–302 doi:10.1007/978-94-009-0349-4_15.
6. Peter J. Stuckey, Martin Sulzmann & Jeremy Wazny (2004): Improving Type Error Diagnosis. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell '04, ACM, New York, NY, USA, pp. 80–91, doi:10.1145/1017472.1017486.
7. Martin Sulzmann & Peter J. Stuckey (2008): HM(X) Type Inference is CLP(X) Solving. Journal of Functional Programming, Volume 18, Issue 2, pp. 251–283, doi:10.1017/S0956796807006569.

# Abstract Compilation for Type Analysis of Object-Oriented Languages (Extended Abstract)

Davide Ancona (DIBRIS, University of Genova, Italy)

## Abstract

Abstract compilation (AC) is a technique for static type analysis which is based on coinductive Logic Programming, and consists in translating the code under analysis into a set of Horn clauses, and to solve queries w.r.t. the coinductive interpretation of the generated clauses.

AC can be employed to perform precise type analysis of object-oriented languages, and support data polymorphism with recursive record and union types. To improve AC, two interesting research directions can be investigated: AC provides opportunities for reusing compilation technology, as the use of the Static Single Assignment intermediate representation, which allows more precise analysis; coinductive Constraint Logic Programming with a suitable notion of subtyping can further improve the accuracy of AC.

## Introduction

Abstract compilation (AC) [7,5,8] is a static type analysis approach aiming to reconcile compositional and global analysis through symbolic execution. It consists in translating the program under analysis in a more abstract type based representation expressed by a set of Horn clauses, and to solve an automatically generated goal w.r.t. the coinductive interpretation of such a translation. Coinduction is required to properly deal with both recursive types, represented by cyclic terms, and mutually recursive user-defined functions/methods.

AC allows modular analysis because several compilation schemes can be defined for the same language, each corresponding to a different kind of analysis, without changing the inference engine, which typically implements coinductive logic programming [12, 11, 6]. Compilation schemes based on union and record types have been studied to support parametric and data polymorphism (that is, polymorphic methods and fields) in object-oriented languages, and a smooth integration of nominal and structural types [7]; other proposed compilation schemes aim to detect uncaught exceptions [5], or to exploit advanced intermediate representations allowing more accurate analysis [8, 9].

AC reconciles compositional and global analysis because on the one hand the source code of the program under analysis is compiled once and for all, hence preexisting source code needs not to be reinspected when new code is added, as happens in compositional analysis; on the other hand, context sensitive analysis is supported since different goals can be solved at different times for the same code fragment. Furthermore, with some limitations on analysis precision, compositional compilation can be achieved with more general non ground goals. Another advantage of AC consists in its direct relationship with Prolog, and the natural support offered by this programming language for rapid prototyping of type analysis [1].

## Intermediate code representations

Recent compiler technology provides fast algorithms for translating source code into IR (Intermediate Representation), as, for instance, SSA (Static Single Assignment) form, particularly suitable for efficient static analysis. Using SSA, and extensions such as SSI (Static Single Information), improves the precision of type analysis of local variables performed with AC [8, 9]; recently, a high-level notion of SSA [3] has been introduced to simplify the compilation scheme used by AC.

To exploit SSA in AC, union types have to be introduced to be able to compile ϕ pseudo-functions that are introduced at program merge points during the translation into IR. In this way it is possible to infer different types for each occurrence of the same local variables.

SSI can further improve the analysis by refining the type of local variables in the branches of a program; to this aim, intersection and negations types are required.

## Coinductive constraint logic programming with subtyping

One of the limitations of AC based on coinductive Logic Programming is that in the presence of recursive methods the inference engine may fail to find a regular derivation even if the program under analysis is type safe.

To overcome this problem, one can exploit either structural resolution [10] to deal with non regular derivations, or subtyping constraints [5] to employ subsumption instead of simple term unification to make derivations regular. This latter solution allows exploitation of coinductive constraint logic programming with advanced forms of subtyping with union and intersection types [2, 4]; to this aim, predicates used to generate the logic program most curry variance annotations, and a sound decision procedure for satisfaction of subtyping constraints must be provided.

## References

1. K. Y. Ahn & A. Vezzosi (2016): Executable Relational Specifications of Polymorphic Type Systems using Prolog. In: FLOPS 2016, pp. 109–125, doi:10.1007/978-3-319-29604-3_8.
2. D. Ancona & A. Corradi (2014): Sound and complete subtyping between coinductive types for object-oriented languages. In: ECOOP 2014, pp. 282–307, doi:10.1007/978-3-662-44202-9_12.
3. D. Ancona & A. Corradi (2016): A Formal Account of SSA in Java-like Languages. In: FTfJP'16, pp. 2:1–2:8, doi:10.1145/2955811.2955813.
4. D. Ancona & A. Corradi (2016): Semantic subtyping for imperative object-oriented languages. In: OOPSLA 2016, pp. 568–587, doi:10.1145/2983990.2983992.
5. D. Ancona, A. Corradi, G. Lagorio & F. Damiani (2011): Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?. In: FoVeOOS 2010, pp. 31–45, doi:10.1007/978-3-642-18070-5_3.
6. D. Ancona & A. Dovier (2015): A Theoretical Perspective of Coinductive Logic Programming. Fundamenta Informaticae 140(3-4), pp. 221–246, doi:10.3233/FI-2015-1252.
7. D. Ancona & G. Lagorio (2009): Coinductive type systems for object-oriented languages. In: ECOOP 2009 5653, pp. 2–26, doi:10.1007/978-3-642-03013-0_2.
8. D. Ancona & G. Lagorio (2011): Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theoretical Informatics and Applications 45(1), pp. 3–33, doi:10.1051/ita/2011009.
9. D. Ancona & G. Lagorio (2012): Static single information form for abstract compilation. In: IFIP TCS 2012, pp. 10–27, doi:10.1007/978-3-642-33475-7_2.
10. E. Komendantskaya & P. Johann (2015): Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic. CoRR abs/1511.07865. Available at http://arxiv.org/abs/1511.07865.
11. L. Simon, A. Bansal, A. Mallya & G. Gupta (2007): Co-Logic Programming: Extending Logic Programming with Coinduction. In: ICALP 2007, pp. 472–483, doi:10.1007/978-3-540-73420-8_42.
12. L. Simon, A. Mallya, A. Bansal & G. Gupta (2006): Coinductive Logic Programming. In: ICLP 2006, pp. 330–345, doi:10.1007/11799573_25.

# Refinement Types and Higher-Order Constrained Horn Clauses (Extended Abstract)

C.-H. Luke Ong (University of Oxford)
Steven J. Ramsay (University of Oxford)

Constrained Horn clauses have recently emerged as a very promising candidate for a logical basis for automatic program verification (especially symbolic model checking). There is evidence to suggest that many first-order verification problems which, at their heart, require finding relations satisfying some given conditions, can be posed as questions of solving systems of Horn clauses, modulo constraints expressed in some suitable background theory [1, 2]. Consequently, researchers have developed several highly efficient solvers for first-order constrained Horn clauses.

We are interested in verifying higher-order programs. Here too it seems very worthwhile to look for a unifying, logical basis for automated program verification. Furthermore, it is natural to frame the verification problem as a search for relations that meet appropriate criteria, and for these criteria to be expressed as constrained Horn clauses. However, one major difference with the foregoing work is that the relations will, in general, be of higher type. For example, consider the following higher-order program: $\begin{array}{l} \mathsf{let}\ \mathit{add}\ x\ y = x + y \\ \mathsf{let}\ \mathsf{rec}\ \mathit{iter}_0\ f\ n =\\ \quad\mathsf{if}\ n \leq 0\ \mathsf{then}\ 0\ \mathsf{else}\ f\ n\ (\mathit{iter}_0\ f\ (n - 1)) \\ \mathsf{in}\ \lambda n.\ \mathsf{assert}\ (n \leq \mathit{iter}_0\ \mathit{add}\ n) \end{array}$

The term $\mathit{iter}_0\ \mathit{add}\ n$ is the sum of the integers from $1$ to $n$ in case $n$ is non-negative and is $0$ otherwise. The program is safe just in case the assertion is never violated, i.e. the summation is not smaller than $n$. To verify safety, we must find an invariant that implies the required property. For our purposes, an invariant will be an over-approximation of the input-output graphs of the functions defined in the program.

The existence of such an invariant is specified by the set of higher-order constrained Horn clauses on the right in the unknowns $\mathit{Iter}_0 : (\mathsf{int} \to \mathsf{int} \to \mathsf{int} \to \mathsf{bool}) \to \mathsf{int} \to \mathsf{int} \to \mathsf{bool}$ and $\mathit{Add} : \mathsf{int} \to \mathsf{int} \to \mathsf{int} \to \mathsf{bool}$. $\begin{array}{l} \forall xyz.\, z = x + y \Rightarrow \mathit{Add}\ x\ y\ z \\ \forall fnr.\, n \leq 0 \wedge r = 0 \Rightarrow \mathit{Iter}_0\ f\ n\ r \\ \forall fnr.\,(\exists p.\, n > 0 \wedge \mathit{Iter}_0\ f\ (n-1)\ p \wedge f\ n\ p\ r) \Rightarrow \mathit{Iter}_0\ f\ n\ r \\ \forall nr.\, \mathit{Iter}_0\ \mathit{Add}\ n\ r \Rightarrow n \leq r \end{array}$ The first, a definite clause, constrains $\mathit{Add}$ to be an over-approximation of the addition function. The second and third, both definite clauses, constrain $\mathit{Iter}_0$ to be an over-approximation of the iteration combinator. The last, a goal clause, constrains these over-approximations to be small enough that they exclude the possibility of relating an input $n$ to a smaller output $r$. A model of these clauses in the theory of integer linear arithmetic, assigning (the characteristic function of) relations to $\mathit{Iter}_0$ and $\mathit{Add}$, is exactly such an invariant. Hence, such an assignment constitutes a witness to safety of the program. One such model is the following (expressed as terms of higher-order logic): $\begin{array}{l} \mathit{Add} \mapsto \lambda xyz.\ z = x+y \\ \mathit{Iter}_0 \mapsto \lambda fnr.\ (\forall x y.\, f\ x\ y\ z \Rightarrow 0 \leq x \Rightarrow y \leq z) \Rightarrow n \leq r \end{array}$ The aim of our work is to automate the search for such models. We take inspiration from an already successful method for higher-order program verification, namely refinement type inference [4, 3, 5, 6].

Refinement types are a way to specify invariants for higher-order programs. Their power comes from the ability to lift rich first-order theories over data to higher types using subtyping and the dependent product. We have developed a system for assigning refinement types to higher-order constrained Horn clauses. The idea is that every valid type assignment $\Gamma$ to the higher-order unknowns is a syntactic representation of a model of the definite clauses. For example, the model discussed previously can be represented by the type assignment $\Gamma_I$: $\begin{array}{l} \mathit{Add}: x\!\!: \mathsf{int} \to y\!\!: \mathsf{int} \to z\!\!: \mathsf{int} \to \mathsf{bool}\langle z = x + y \rangle \\ \mathit{Iter}_0: (x\!\!: \mathsf{int} \to y\!\!: \mathsf{int} \to z\!\!: \mathsf{int} \to \mathsf{bool}\langle 0 \leq x \Rightarrow y < z \rangle) \to n\!\!:\mathsf{int} \to r\!\!:\mathsf{int} \to \mathsf{bool}\langle n \leq r \rangle \end{array}$ The key to the enterprise is the refinement type for Booleans, $\mathsf{bool}\langle \phi \rangle$, which is parametrised by a first-order constraint formula $\phi$. The meaning of this type under a valuation $\alpha$ of its free first-order variables is the set of truth values $\{\mathsf{false}, [\![\phi]\!](\alpha)\}$ determined by evaluation of $\phi$. The dependent product and integer types are interpreted standardly, so that the first type above can be read as the set of all ternary relations on integers $x,y$ and $z$ that are false whenever $z$ is not $x + y$.

Soundness of the type system allows one to conclude that certain first-order constraint formulas can be used to approximate higher-order Horn formulas. Given goal formula $s$, from the derivability the judgement $\Gamma \vdash s : \mathsf{bool}\langle\phi\rangle$ it follows that $s \Rightarrow \phi$ in the model (represented by) $\Gamma$. Consequently, if $\Gamma$ is a valid model of the definite clauses and $s$ is the negation of the goal formula, then $\Gamma \vdash s : \mathsf{bool}\langle\mathsf{false}\rangle$ implies that the model validates the desired property. In particular, since $\Gamma_I$ is a valid type assignment for $\mathit{Add}$ and $\mathit{Iter}_0$ and since $\Gamma_I \vdash \exists nr.\,\mathit{Iter}_0\ \mathit{Add}\ n\ r \wedge n > r : \mathsf{bool}\langle \mathsf{false} \rangle$ is derivable, it follows that the constrained Horn clause problem above is solvable and hence the program is safe.

By phrasing the higher-order constrained Horn clause problem in this way, machinery already developed for refinement type inference can be adapted to automate the search for models (i.e. type assignments). This machinery actually reduces refinement type assignment to the problem of solving sets of first-order constrained Horn clauses. Consequently, in total, our work can be seen as a method for obtaining solutions of higher-order constrained Horn clause problems by solving first-order constrained Horn clause problems. An implementation of the method yields promising results.

### References

1. Tewodros A. Beyene, Corneliu Popeea & Andrey Rybalchenko (2013): Solving Existentially Quantified Horn Clauses. In: Computer Aided Verification (CAV 2013), pp. 869–882, doi:10.1007/978-3-642-39799-8_61.
2. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan & Andrey Rybalchenko (2015): Horn Clause Solvers for Program Verification. In: Fields of Logic and Computation, pp. 24–51, doi:10.1007/978-3-319-23534-9_2.
3. Naoki Kobayashi, Ryosuke Sato & Hiroshi Unno (2011): Predicate abstraction and CEGAR for higher-order model checking. In: Programming Languages Design and Implementation, PLDI'11. ACM, pp. 222–233, doi:10.1145/1993316.1993525.
4. Patrick Maxim Rondon, Ming Kawaguchi & Ranjit Jhala (2008): Liquid types. In: Programming Language Design and Implementation (PLDI 2008), pp. 159–169, doi:10.1145/1375581.1375602.
5. Niki Vazou, Alexander Bakst & Ranjit Jhala (2015): Bounded refinement types. In: International Conference on Functional Programming (ICFP 2015), pp. 48–61, doi:10.1145/2858949.2784745.
6. He Zhu & Suresh Jagannathan (2013): Compositional and Lightweight Dependent Type Inference for ML. In: Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, pp. 295–314, doi:10.1007/978-3-642-35873-9_19.

# Category Theoretic Semantics for Logic Programming: Laxness and Saturation (Extended Abstract)

John Power (University of Bath)

John Power would like to acknowledge the support of EPSRC grant EP/K028243/1 and Royal Society grant IE151369. No data was generated in the course of this project.

### Summary

Recent research on category theoretic semantics of logic programming has focused on two ideas: lax semantics ([3]) and saturated semantics ([1]). Until now, the two ideas have been presented as alternatives, but that competition is illusory, the two ideas being two views of a single, elegant body of theory, reflecting different but complementary aspects of logic programming.

Given a set of atoms $At$, one can identify a variable-free logic program $P$ built over $At$ with a $P_fP_f$-coalgebra structure on $At$, where $P_f$ is the finite powerset functor on $Set$: each atom is the head of finitely many clauses in $P$, and the body of each clause contains finitely many atoms. If $C(P_fP_f)$ is the cofree comonad on $P_fP_f$, then, given a logic program $P$ qua $P_fP_f$-coalgebra, the corresponding $C(P_fP_f)$-coalgebra structure characterises the and-or derivation trees generated by $P$.

Extending this to arbitrary programs, given a signature $\Sigma$ of function symbols, let $\mathcal{L}_{\Sigma}$ denote the Lawvere theory generated by $\Sigma$, and, given a logic program $P$ with function symbols in $\Sigma$, consider the functor category $[\mathcal{L}_{\Sigma}^{op},Set]$, extending the set $At$ of atoms in a variable-free logic program to the functor from $\mathcal{L}_{\Sigma}^{op}$ to $Set$ sending a natural number $n$ to the set $At(n)$ of atomic formulae with at most $n$ variables generated by the function symbols in $\Sigma$ and the predicate symbols in $P$. We would like to model $P$ by a $[\mathcal{L}_{\Sigma}^{op},P_fP_f]$-coalgebra $p:At\longrightarrow P_fP_fAt$ that, at $n$, takes an atomic formula $A(x_1,\ldots ,x_n)$ with at most $n$ variables, considers all substitutions of clauses in $P$ into clauses with variables among $x_1,\ldots ,x_n$ whose head agrees with $A(x_1,\ldots ,x_n)$, and gives the set of sets of atomic formulae in antecedents. However, that does not work for two reasons. The first may be illustrated as follows.

#### Example 1

ListNat (for lists of natural numbers) denotes the logic program

$1.\ \mathtt{nat(0)} \gets$

$2.\ \mathtt{nat(s(x))} \gets \mathtt{nat(x)}$

$3.\ \mathtt{list(nil)} \gets$

$4.\ \mathtt{list(cons (x, y))} \gets \mathtt{nat(x), list(y)}$

ListNat has nullary function symbols $\mathtt{0}$ and $\mathtt{nil}$. So there is a map in $\mathcal{L}_{\Sigma}$ of the form $0\rightarrow 1$ that models the symbol $0$. Naturality of $p:At\longrightarrow P_fP_fAt$ in $[\mathcal{L}_{\Sigma}^{op},Set]$ would yield commutativity of the diagram

$\begin{CD} At(1) @>p_1>> P_fP_fAt(1)\\ @VVAt(\mathsf{0})V @VVP_fP_fAt(\mathsf{0})V\\ At(0) @>p_0>> P_fP_fAt(0) \end{CD}$

But consider $\mathtt{nat(x)}\in At(1)$: there is no clause of the form $\mathtt{nat(x)}\gets \,$ in ListNat, so commutativity of the diagram would imply that there cannot be a clause in ListNat of the form $\mathtt{nat(0)}\gets \,$ either, but in fact there is one. Thus $p$ is not a map in the functor category $[\mathcal{L}_{\Sigma}^{op},Set]$.

Lax semantics addresses this by relaxing the naturality condition on $p$ to a subset condition, so that, given, for instance, a map in $\mathcal{L}_{\Sigma}$ of the form $f:0 \rightarrow 1$, the diagram need not commute, but rather the composite via $P_fP_fAt(1)$ need only yield a subset of that via $At(0)$.

In contrast, saturation semantics works as follows. Regarding $ob(\mathcal{L}_{\Sigma})$, equally $ob(\mathcal{L}_{\Sigma})^{op}$, as a discrete category with inclusion functor $I:ob(\mathcal{L}_{\Sigma})\longrightarrow \mathcal{L}_{\Sigma}$, the functor $[I,Set]:[\mathcal{L}_{\Sigma}^{op},Set]\longrightarrow [ob(\mathcal{L}_{\Sigma})^{op},Set]$ that sends $H:\mathcal{L}_{\Sigma}^{op}\longrightarrow Set$ to the composite $HI:ob(\mathcal{L}_{\Sigma})^{op} \longrightarrow Set$ has a right adjoint $R$, given by right Kan extension. So the data for $p:At\longrightarrow P_fP_fAt$ may be seen as a map in $[ob(\mathcal{L}_{\Sigma})^{op},Set]$, which, by the adjointness, corresponds to a map $\bar{p}:At\longrightarrow R(P_fP_fAtI)$ in $[\mathcal{L}_{\Sigma}^{op},Set]$, yielding saturation semantics. . In this talk, we show that the two approaches can elegantly be unified, the relationship corresponding to the relationship between theorem proving and proof search in logic programming.

The second problem mentioned above is about existential variables, which we now illustrate.

#### Example 2.

GC (for graph connectivity) denotes the logic program

$1.\ \mathtt{connected(x,x)} \gets$

$2.\ \mathtt{connected(x,y)} \gets \mathtt{edge(x,z)}, \mathtt{connected(z,y)}$

There is a variable $z$ in the tail of the second clause of GC that does not appear in its head. Such a variable is called an existential variable, the presence of which challenges the algorithmic significance of lax semantics. In describing the putative coalgebra $p:At\longrightarrow P_fP_fAt$ just before Example 1, we referred to all substitutions of clauses in $P$ into clauses with variables among $x_1,\ldots ,x_n$ whose head agrees with $A(x_1,\ldots ,x_n)$. If there are no existential variables, that amounts to term-matching, which is algorithmically efficient; but if existential variables do appear, the mere presence of a unary function symbol generates an infinity of such substitutions, creating algorithmic difficulty, which, when first introducing lax semantics, we, also Bonchi and Zanasi, avoided modelling by replacing the outer instance of $P_f$ by $P_c$, thus allowing for countably many choices. Such infiniteness militates against algorithmic efficiency, and we resolve it by refining the functor $P_fP_f$ while retaining finiteness.

This talk is based upon the paper ([2]).

1. Filippo Bonchi & Fabio Zanasi (2015): Bialgebraic Semantics for Logic Programming. In: Logical Methods in Computer Science 11(1), doi:10.2168/LMCS-11(1:14)2015.
2. Ekaterina Komendantskaya & John Power (2016): Logic programming: laxness and saturation. In: Submitted, CoRR abs/1608.07708. Available at http://arxiv.org/abs/1608.07708.
3. Ekaterina Komendantskaya, John Power & Martin Schmidt (2016): Coalgebraic logic programming: from Semantics to Implementation. In: J. Log. Comput. 26(2), pp. 745 - 783, doi:10.1093/logcom/exu026.