jupyter: jupytext: text_representation: extension: .md format_name: markdown format_version: '1.3' jupytext_version: 1.16.7 kernelspec: display_name: Logtalk language: logtalk name: logtalk_kernel ---

<!--

This file is part of Logtalk https://logtalk.org/ SPDX-FileCopyrightText: 1998-2025 Paulo Moura <pmoura@logtalk.org> SPDX-License-Identifier: Apache-2.0

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -->

coinduction

This example requires a recent version of CxProlog, ECLiPSE, SICStus Prolog, SWI-Prolog, XVM, or YAP as the backend Prolog compiler. XVM requires starting with the `--enable-occurs-check` command-line option.

Note that Logtalk support for coinduction is still experimental. The two major issues are lack of robust Prolog support for cyclic terms and lack of support for tabling of cyclic terms. The first issue prevents using of some backend Prolog compilers. The second issue may prevent some coinductive predicates to behave as (theoretically) expected.

This folder contains several examples of coinductive predicates, adapted from the coinduction papers and from the Feliks Kluzniak's DRA meta-interpreter.

The unit tests are currently disabled when using CxProlog or ECLiPSE as the backend compiler. Although some tests pass, all tests calling bagof/3 don't terminate until all available memory is exhausted due to the fragile support for rational terms in these two Prolog compilers.

For more information see:

@inproceedings{1778186,
        author = {Gupta, Gopal and Bansal, Ajay and Min, Richard and Simon, Luke and Mallya, Ajay},
        title = {Coinductive logic programming and its applications},
        booktitle = {Proceedings of the 23rd International Conference on Logic programming (ICLP)},
        year = {2007},
        isbn = {3-540-74608-0, 978-3-540-74608-9},
        pages = {27--44},
        location = {Porto, Portugal},
        publisher = {Springer-Verlag},
        address = {Berlin, Heidelberg},
}

@inproceedings{
        author = {Neda Saeedloei and Gopal Gupta},
        title = {Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R)},
        booktitle = {Proceedings of the 19th Workshop on Logic-based methods in Programming Environments (WLPE)},
        year = {2009},
        location = {Pasadena, California, USA}
}

@inproceedings{saeedloei_et_al:LIPIcs:2010:2599,
        author ={Neda Saeedloei and Gopal Gupta},
        title = {Timed Definite Clause Omega-Grammars},
        booktitle ={Technical Communications of the 26th International Conference on Logic Programming},
        pages = {212--221},
        series = {Leibniz International Proceedings in Informatics (LIPIcs)},
        isbn = {978-3-939897-17-0},
        issn = {1868-8969},
        year = {2010},
        volume = {7},
        editor = {Manuel Hermenegildo and Torsten Schaub},
        publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
        address = {Dagstuhl, Germany},
        URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2599},
        doi = {http://dx.doi.org/10.4230/LIPIcs.ICLP.2010.212},
        annote = {Keywords: Constraint Logic Programming over reals, Co-induction, Context-Free Grammars, Omega-Grammars}
}

@inproceedings{AnconaSAC12,
        author = {Ancona, D.},
        title = {Regular corecursion in {P}rolog},
        booktitle = {A{CM} {S}ymposium on {A}pplied {C}omputing ({SAC} 2012)},
        ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaSAC12.pdf},
        keywords = {coinduction,corecursion},
        year = 2012
}

@inproceedings{pmoura13b,
        author = {Paulo Moura},
        title = "{A Portable and Efficient Implementation of Coinductive Logic Programming}",
        booktitle = {Proceedings of the Fifteenth International Symposium on Practical Aspects of Declarative Languages},
        editor = "Kostis Sagonas",
        series = "Lecture Notes in Computer Science",
        pages = {77-92},
        volume = "7752",
        year = {2013},
        publisher = "Springer-Verlag",
        address = "Berlin Heidelberg",
        doi = {10.1007/978-3-642-45284-0_6},
        url = {http://dx.doi.org/10.1007/978-3-642-45284-0_6}
}

Warning: Some of the queries below will hang when running from a notebook due to issues printing bindings with rational terms.

Print Logtalk, Prolog backend, and kernel versions (if running as a notebook):

%versions

When using XVM as the backend, ensure that the unify_applies_occurs_check is set to true:

(current_prolog_flag(dialect, xvm) -> set_prolog_flag(unify_applies_occurs_check,true); true).

Start by loading the example:

logtalk_load(coinduction(loader)).

An elementary coinductive predicate:

simple::p.

Similar:

simple::p(hoho).

simple::p(hoho, X).

The following goal is true for any cyclic list containing only ones:

L = [1| L], binary::p(L).

Same for any cyclic list containing only zeros:

L = [0| L], binary::p(L).

Or a repetition of a pattern of ones and zeros:

L = [1,0,1| L], binary::p(L).

But not all solutions can be returned:

%%table
binary::p(X).

Infinite streams example:

%%table
streams::nat_stream([0, s(0), s(s(0))| T]).

X = [0, 1, 1, 0| X], streams::bit_stream(X).

Filtering odd numbers from a list:

L = [0, s(0), s(s(0))| L], filter::filter(L, F).

Using the Sieve of Eratosthenes to find prime numbers:

sieve::primes(20, P).

List membership example:

X = [1, 2, 3| X], lists::comember(2, X).

X = [1, 2, 3, 1, 2, 3], \+ lists::comember(2, X).

%%table
X = [1, 2, 3| X], lists::comember(Y, X).

X = [0, s(0), s(s(0))], \+ lists::comember(s(0), X).

X = [0, s(0), s(s(0))| X], lists::comember(s(0), X).

List append example:

Y = [4,5,6| Y], lists::append([1,2,3], Y, Z).

X = [1,2,3| X], Y = [3,4| Y], lists::append(X, Y, Z).

%%table
Z = [1,2| Z], lists::append(X, Y, Z).

List non-membership example:

X = [1,2,3], \+ lists::absent(2, X).

X = [1,2,3], \+ lists::absent(4, X).

X = [1,2,3| X], lists::absent(4, X).

X = [1,2,3| X], \+ lists::absent(2, X).

Sorting example:

X = [1-2,2-3,1-4|X], sorting::keysort(X, L).

X = [1-2,2-3|Y], Y = [1-4|Y], sorting::keysort(X, L).

Omega-automaton example:

%%table
automaton::automaton(s0, X).

Module 4 counter example:

counter::verify.

Nested automata example:

%%table
nested::state(s0, X), lists::absent(s2, X).

Timed automata example:

%%table
train::driver(s0, s0, s0, X, R).

Timed automata coroutining example:

cotrain::comain(A, B, C).

cotrain::test_max(M, N, R).

Finding the cyclic paths in graphs:

%%table
cp1::path(a, Path).

%%table
cp2::path(a, Path).

cp3::path(a, Path, 3).
Path = [a|_S1], % where
    _S1 = [b, c, a|_S1] ;
false.
-->

Testing for bipartite graphs (vertex adjacency lists must be ordered):

```logtalk
A = v(a, [F]), B = v(b, [F, G]), C = v(c, [H, I]), D = v(d, [G]), E = v(e, [F, I]), F = v(f, [A, B]), G = v(g, [B, D]), H = v(h, [C]), I = v(i, [C, E]), graph::bipartite(A).