Programming language supporting infinitary rewriting of regular term graphs? 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
[2] Yves Bertot, Ekaterina Komendantskaya (2008)
Inductive and Coinductive Components of Corecursive Functions in Coq
Yes, Prolog. 

The specification of unification in the Prolog standard omits the occurs check, and as a result variables range over rational trees. Additionally,  many Prolog (such as SWI Prolog and YAP) implementations support tabling, which permits defining and using coinductively defined predicates.