Defining constraints -- datasorts and stacst

[M88]

I was looking into the rock-paper-scissors example (here and here) and I found it very useful for learning how to define  predicates in the statics.

I had made an attempt something similar, but using independent datasorts as parameters.

For example:

datasort catA =
   | cA_1
   | cA_2
   | cA_3

datasort catB =
   | cB_1
   | cB_2
   | cB_3

datasort sortA =
   | sA_1 of (catA, catB)
   | sA_2
   | sA_3

// only sortA is used to define types. Eg,
abst@ype typeA(sortA)

I ran into a few issues.  I arrived at a solution, but I thought it could be cleaner.

First, I discovered that I wasn't  able to define equalities with datasorts.  Eg, {sa:sortA | sa == sA_2}.  It would typecheck, but the constraints could not be solved. I suppose this makes sense, considering the definition of ==.  Does ATS supply a way to determine equalities on datasorts?  Is there another feature that would make this unnecessary?

As an alternative, I decided to declare a static predicate, as in the rock-paper-scissors example:

stacst isCA1 : sortA -> bool

// This works, but becomes quite verbose.
praxi isCA1_praxi ():
   [
      isCA1(sA_1(cA_1,cB_1)) &&
      isCA1(sA_1(cA_1,cB_2)) &&
      isCA1(sA_1(cA_1,cB_3))
   ] void

The verbosity isn't an issue in this example, but becomes pretty unmanageable as the relationships get more complex. I would like to say, "for any catB".  I tried using universal and existential quantification, but the constraints would not solve.  I would like to avoid passing catB explicitly.

Is there a  way to reduce it to something like this:

// The constraints will not solve:

praxi isCA1_praxi ():
   [ cb: catB |
      isCA1(sA_1(cA_1,cb))
   ] void

Perhaps I am abusing datasorts -- suggestions for other approaches are welcome.

[gmhwxi]

It seems that isCA1_praxi should be declared
as follows:

praxi
isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void

[M88]

It seems that isCA1_praxi should be declared
as follows:

praxi
isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void

Yes, this makes sense -- I am looking for universal quantification.

I suppose the issue here is how it would be invoked.  Would I

still need to invoke the proof as follows?

prval () = isCA1_praxi{cB_1}()
prval () = isCA1_praxi{cB_2}()
prval () = isCA1_praxi{cB_3}()

********

After giving this some thought, I realized I could invoke the proof

within a constructor, omitting the need to explicitly specify each "catB."  

fun makeCA1 {cb:catB}() : [sa:sortA | isCA1(sa) ] typeA(sa)

What tripped me up at first is that the return value of each constructor

should specify the constraint "isCA1" if I use this approach, whereas

the former let me invoke the proofs globally.

[Hongwei Xi]

There are two styles of theorem-proving in ATS:

http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/index.html

To avoid explicit quantifier elimination performed by the following code,

prval () = isCA1_praxi{cB_1}()
prval () = isCA1_praxi{cB_2}()
prval () = isCA1_praxi{cB_3}()

you can try:

prval() = $solver_assert(isCA1_praxi)

and then use Z3 to solve the generated constraints. Doing so means that you are at the mercy

of Z3's quantifier elimination heuristics or (black) magic.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com.

[M88]

I've been experimenting with Z3 and it's proven to be very useful.  I would like to keep using the built-in constraint solver for various reasons.

Perhaps this is a novice question, but how does one establish equality within a datasort?

For example, given datasort

datasort item

  | a

  | b

  | c

How can I establish that a == a ?

I can use scase, but that is only optimal for a small number of branches.  It would be nice to use sif.

I can declare a static function like

stacst item_id  : (item) -> int

stacst item_eq : (item,item) -> bool

extern praxi item_uniq : [

   item_id(a) == 1;

   item_id(b) == 2;

   item_id(c) == 3

] void

extern praxi item_eq_praxi{a,b:item} : [

   item_eq(a,b) == (item_id(a) == item_id(b))

] void

But the constraint solver still gives me errors, because either item_eq(a,b) == (a == b) does not resolve (eg, in a sif branch), or vice-versa (eg, in nested scase).

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

[Hongwei Xi]

The built-in solver in ATS is very limited in its handling of datasorts

like the following one:

datasort item =

  | a

  | b

  | c

In practice, I try to use integers instead:

sortdef item = int

#define item_a 0

#define item_b 1

#define item_c 2

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/82adac20-edf8-4974-ad88-32455de26f16%40googlegroups.com.

[M88]

Thanks for the response -- it helped me resolve a few issues.  I could encode a few properties in the item ids, which let me replace several constraints with stadef.  I managed to get the same code working for both the native constraint solver and Z3.

It did make my error messages less pretty, but I suppose that's not much of an issue.

I did find that many problems (with the native solver) stemmed from writing code in this pattern:

// not good

sortdef sortA = int

sortdef sortB = int

stacst const1 : (sortA) -> bool 

stacst const2 : (sortB,sortA) -> bool

extern praxi const1_praxi {s:sortA} () : [

             const1(s) == ( s >= 1024 && s < 2048 )

] void

extern praxi const2_praxi {b:sortB}{a:sortA} () : [

             const2(b,a) == const1(a)

] void

The following typechecks much faster:

// ok

sortdef sortA = int

sortdef sortB = int

stadef const1 ( s:sortA) : bool = ( s >= 1024 && s < 2048  )

stacst const2 : (sortB,sortA) -> bool

// no const2_praxi needed

// const2 might be much more complex in a real example, so I  left this one

extern praxi const2_praxi {b:sortB}{a:sortA} () : [

             const2(b,a) == const1(a)

] void

I did notice that native constraint solving seems to go 2-3x faster when values are reused (eg, assigned to a variable).  Do constraints need to be solved for each variable, even if they are the same type?  I'm a bit curious as to how this works.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/82adac20-edf8-4974-ad88-32455de26f16%40googlegroups.com.

[Hongwei Xi]

The built-in constraint-solver cannot handle constants

introduced via 'stacst' very well. It was meant to only handle

integer constraints. I did a bit of hacking to allow very limited
handling of constants. If you need serious constraint-solving,

please use Z3 instead.

The built-in constraint solver uses so-called Fourier-Motzkin variable

elimination method, which is exponential time (worst-cast) and polynomial

time (probability). A variable is introduced for each non-variable expression.

If you explicitly introduce variables for expressions, the solver should work

more efficiently.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/71209c8a-4a6c-4152-9b3e-826d747a7fe2%40googlegroups.com.