Functional Logic Programming with Generalized Circular Coinduction

TL;DR

This paper introduces a method to extend functional logic programming, specifically Curry, to handle coinductive reasoning using regular terms, with adapted semantics and demonstrated examples.

Contribution

It presents a novel approach to incorporate coinductive reasoning into Curry by adapting data structures and semantics for regular terms.

Findings

Effective coinductive reasoning demonstrated with examples

Operational semantics successfully adapted for coinduction

Potential applications in reasoning on infinite data structures

Abstract

We propose a method to adapt functional logic programming to deal with reasoning on coinductively interpreted programs as well as on inductively interpreted programs. In order to do so, we consider a class of objects interesting for this coinductive interpretation, namely regular terms. We show how the usual data structures can be adapted to capture these objects. We adapt the operational semantics of Curry to interpret programs coinductively. We illustrate this method with several examples that show the working of our method and several cases in which it could be useful. Finally, we suggest how the declarative semantics can be adapted suitably.