<p>Yes, <a href="https://en.wikipedia.org/wiki/Prolog" rel="nofollow noreferrer">Prolog</a>.</p>
<p>The specification of unification in the Prolog standard omits the <a href="https://en.wikipedia.org/wiki/Occurs_check" rel="nofollow noreferrer"><em>occurs check</em></a>, and as a result <a href="https://dtai.cs.kuleuven.be/projects/ALP/newsletter/archive_93_96/net/impl/occur.html#:%7E:text=Another%20point%20that,to%20rational%20trees." rel="nofollow noreferrer">when this spec is properly implemented</a> variables range over rational trees. Additionally,  many Prolog (such as <a href="http://www.swi-prolog.org/" rel="nofollow noreferrer">SWI Prolog</a> and <a href="https://www.dcc.fc.up.pt/%7Evsc/Yap/" rel="nofollow noreferrer">YAP</a>) implementations support <a href="https://en.wikipedia.org/wiki/Prolog#Tabling" rel="nofollow noreferrer"><em>tabling</em></a>, which permits defining and using coinductively defined predicates.</p>

CC BY-SA 4.0
2017-02-21T10:15:50.117Z
2021-09-14T15:53:58.330Z
2021-09-14T15:53:58.330Z
Neel Krishnaswami
<p>Do any practical programming languages support term graph rewriting of infinite but regular terms? For example the toy language CoCaml [1] supports computations on infinite regular streams. Coq supports coinduction [2] but not infinitary rewriting, as far as I can tell. By "infinite regular term graph", I mean those inhabitants of coalgebraic datatypes that can be defined in terms of finitely many equations. </p>

<ul>
<li>[1] Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva (2017)
<a href="https://www.cs.cornell.edu/~kozen/papers/cocaml.pdf" rel="noreferrer">CoCaml: Functional Programming with Regular Coinductive Types</a></li>
<li>[2] Yves Bertot, Ekaterina Komendantskaya (2008)
<a href="https://hal.inria.fr/inria-00277075v1/document" rel="noreferrer">Inductive and Coinductive Components of Corecursive Functions in Coq</a></li>
</ul>

<functional-programming><term-rewriting-systems>
Programming language supporting infinitary rewriting of regular term graphs?
fritzo
# Programming language supporting infinitary rewriting of regular term graphs?

(Asked by: username_0 on 2017-02-21)

Do any practical programming languages support term graph rewriting of infinite but regular terms? For example the toy language CoCaml [1] supports computations on infinite regular streams. Coq supports coinduction [2] but not infinitary rewriting, as far as I can tell. By "infinite regular term graph", I mean those inhabitants of coalgebraic datatypes that can be defined in terms of finitely many equations.

* [1] Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva (2017)
  [CoCaml: Functional Programming with Regular Coinductive Types](https://www.cs.cornell.edu/~kozen/papers/cocaml.pdf)
* [2] Yves Bertot, Ekaterina Komendantskaya (2008)
  [Inductive and Coinductive Components of Corecursive Functions in Coq](https://hal.inria.fr/inria-00277075v1/document)

**Tags:** functional-programming, term-rewriting-systems


---

## 1 answers

### Answer by username_1 on 2017-02-21. Score: 8

Yes, [Prolog](https://en.wikipedia.org/wiki/Prolog).

The specification of unification in the Prolog standard omits the [*occurs check*](https://en.wikipedia.org/wiki/Occurs_check), and as a result [when this spec is properly implemented](https://dtai.cs.kuleuven.be/projects/ALP/newsletter/archive_93_96/net/impl/occur.html#:%7E:text=Another%20point%20that,to%20rational%20trees.) variables range over rational trees. Additionally, many Prolog (such as [SWI Prolog](http://www.swi-prolog.org/) and [YAP](https://www.dcc.fc.up.pt/%7Evsc/Yap/)) implementations support [*tabling*](https://en.wikipedia.org/wiki/Prolog#Tabling), which permits defining and using coinductively defined predicates.


---

