1

Closed

Feature request: codatatypes (datatypes without occurs check)

description

Hi,

We are using Z3 to prove properties of Haskell programs in our tool HipSpec. We would obviously like to use Z3 datatypes to model Haskell datatypes. The trouble is that Z3's datatypes are algebraic while Haskell's are coalgebraic. That is, in Haskell you can have an infinite value like n = Succ n, while with Z3 datatypes you cannot.

As far as I can tell, the only thing stopping us from using Z3 datatypes is the "occurs check", which rules out cyclic terms like n = Succ n. Without the occurs check, I think Z3 datatypes would be agnostic about whether they are data or codata. So I would like a way to switch off the occurs check for a particular datatype, or else somehow declare it as codata (which would have the same effect).

Nick
Closed Jun 6, 2013 at 8:23 PM by leodemoura
Thanks for requesting the feature, but we don't have plans to support it in the near future. We can continue the discussion in the "Discussions Tab"

comments

leodemoura wrote Apr 9, 2013 at 11:11 PM

We can use the following hack to disable the occurs check.
Comment line 348
   if (occurs_check(node))
in the file src/smt/theory_datatype.cpp

We will probably also have to modify the model construction. Method:
model_value_proc * theory_datatype::mk_value(enode * n, model_generator & mg)
The problem is that it assumes there are no cycles.

Another issue is that Z3 will refuse datatype definitions that are not well founded.
The well founded test is implemented at line 289 at src/ast/datatype_decl_plugin.cpp

This kind of hack may be a temporary solution, but if we really want codatatypes, we should implement them as a separate theory.

nick8325 wrote Apr 10, 2013 at 3:01 PM

Ah! So it is harder than I realised.

NikolajBjorner wrote Jun 2, 2013 at 7:31 PM

There is another twist to co-datatypes: equality. A reasonable semantics is that two structures that are observationally equal (bisimilar) are equal. So for example if l1 and l2 are (infinite) lists and
head(l1) = head(l2) = 1 and tail(l1) = l1 and tail(l2) = l2, then l1 = l2.