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 <abysgr...@gmail.com> 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
>>> <https://groups.google.com/forum/#!topic/ats-lang-users/YcdEzhJdJzs>
>>> and here
>>> <https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test25.dats>)
>>> 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
>>> <https://maps.google.com/?q=cA_1+%C2%A0%C2%A0+%7C+cA_2&entry=gmail&source=g>
>>> | cA_2
>>> <https://maps.google.com/?q=cA_1+%C2%A0%C2%A0+%7C+cA_2&entry=gmail&source=g>
>>> | 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
>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,cB_1)) &&
>>> isCA1(sA_1(cA_1
>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,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
> <https://groups.google.com/d/msgid/ats-lang-users/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAPPSPLoWyy3ubtUNAbK0v_EUwYj-mTJ%3DTnKR%2BUVeyn1kJJnC7A%40mail.gmail.com.
