Re: Defining constraints -- datasorts and stacst

2018-04-08 Thread 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.



On Sat, Apr 7, 2018 at 9:09 PM, M88  wrote:

>
> 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.
>
>
> On Saturday, April 7, 2018 at 12:25:05 AM UTC-4, M88 wrote:
>>>
>>>
>>> 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.
>>>
>>>
>>> --
> 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+unsubscr...@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
> 
> .
>

-- 
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+unsubscr...@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 

Re: Defining constraints -- datasorts and stacst

2018-04-07 Thread 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.


On Saturday, April 7, 2018 at 12:25:05 AM UTC-4, M88 wrote:
>>
>>
>> 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.
>>
>>
>>

-- 
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+unsubscr...@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.


Re: Defining constraints -- datasorts and stacst

2018-04-07 Thread gmhwxi

It seems that isCA1_praxi should be declared
as follows:

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

On Saturday, April 7, 2018 at 12:25:05 AM UTC-4, M88 wrote:
>
>
> 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.
>
>
>

-- 
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+unsubscr...@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/ab0f7c98-e2a9-4dda-9427-2016555f66c3%40googlegroups.com.


Defining constraints -- datasorts and stacst

2018-04-06 Thread 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.


-- 
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+unsubscr...@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/2aa9d070-e9bb-461d-974e-c0bb3ecb6ce5%40googlegroups.com.