[SMT-LIB] Adding algebraic datatypes to the SMT-LIB 2 language: an initial proposal

[Jochen Hoenicke]

Hello all,

I think the proposal for recursive datatypes is fine and in the SMT-LIB
spirit: having a minimal set of syntax, relatively easy type-checking rules
and still somewhat readable formulas.  I have some questions, though:

well-definedness
---------------------

I don't understand the well-definedness rules for declare-datatypes:

 provided that each datatype δ is well defined in the following sense: for
> each constructor of δ of rank τ1 · · · τmδ either none of δ1, · · · , δn
> occurs in τ1, . . . , τm or, if one of them does, it is a well defined
> datatype.


If I understand correctly this should guarantee non-emptyness of the
datatypes, but shouldn't it only require that there is at least one
constructor that doesn't contain any delta_i or if it does only well
defined datatypes?  Also the definition is recursive; you should point out
that you want well definedness to be the least fixpoint of this recursive
definition.  If every datatype is well defined it would still satisfy this
definition (this is the largest fix point).

Do you want to prevent datatypes like

(define-datatype Paradox (c (s (Set Paradox))))

where Set could be defined by a logic to correspond to the power set type?
I would've expected something like δi may only occur top-level in τj, i.e,
τj = δi or δi does not occur in τj.

You currently also allow types like

(define-datatype Strange (par X Y) (c (s (Strange Y X)))

where c is now a function from Strange Y X to Strange X Y.   Is this
intended?  May it lead to problems?


minor typos
-------------

page 60: u_{a_i} --> u_k
page 60: contains of --> consists of
page 61: is delta is  --> if delta is

page 60: The sentence starting with if delta \in {delta1... deltan} is
strange, especially since delta is not really mentioned in the remaining
sentence.  You just want to say "if delta=deltai, k=ki, d=di are
corresponding entries in the declaration".


Regards,
  Jochen


-- 
Jochen Hoenicke,
Email: hoenicke at informatik.uni-freiburg.de  Tel: +49 761 203 8243