Skip to first unread message

Dec 10, 2015, 5:16:07 PM12/10/15

to ats-lang-users

ATS has predicates which looks like the usual predicates; and has what it names propositions, which seems not the same as usual propositions and are more proofs.

So far, is that OK to say ATS proposition are not propositions after the usual meaning?

At least, these two pages say, it there are variables and/or quantifiers, then this is not a proposition, that's a predicate.

Moreover ATS propositions are never false, they are always true, or can't exist at all, which is not a surprise, as ATS propositions are proof in the form of definitions, with `absprop` or in the form of inductive definitions with `dataprop` (which is not exactly the same as an axiomatic proof, an inductive definition is a safer assertion).

Unlike a boolean expression or a predicate which may evaluates to either `true` or `false`, a proof may only evaluates into a kind of `true` or not at all, which may be understood this other way: there is no false of type `prop`, the evaluation of a proof either “returns” a kind of true or fails (by the way, is it OK to say Prolog clauses evaluation are proofs?… as too, it never returns a real `false` neither, just fails).

`stacst True: prop // Makes sense, OK?`

stacst False: prop // Does not make sens, isn't it?

An `absprop` and/or a `dataprop`, introduce a function-like thing returning something of sort `prop`. May be it's a function just because there may be variable in the proven statement.

`absprop F(int) // int -> prop`

stadef g: prop = F 0 // Check it's indeed int -> prop

Side note: I don't understand why I can's write `absprop F int` and the parentheses are required.

Type definition may be based on predicates, but not proof (or at least, not directly):

`absprop F(int) // int -> prop`

// typedef t = [i: int; F i] int(i) **ILLEGAL**

There are multiple ways of understanding things. One of these way, is to come to a thing with prior expectations about how things should be. That may be nice, but may not help when trying to understand something which does not match at all or not exactly these prior ideas. May be that's why I'm progressing so slowly in understanding ATS enough to be at ease with it.

One of my prior expectations when I accosted ATS lands, was the relation between a type and a proof (also between a type and a function). But in ATS, a function may function returns a proof of some proposition along to a value of a type, both distinct (the proof is not part of the type of the value returned).

I wanted to try to relate both. Based on the above, I first came to this:

`stadef h: prop -> bool = (lam p => true) // Assume a prop is a proof`

Assuming a proof, either is true or does not exist (because it failed), and also assuming a `prop` is a proof, then the above should be sound. Is it?

`typedef t = [i: int; h(F i)] int(i) // Does it mean what I think it means?`

If it really means what I think, then I may have progressed a bit in matching ATS and my mind.

At least, this simple declaration is not rejected:

`val a: t = 0`

(posting… hope I have not left too much typo errors)

Dec 10, 2015, 5:41:19 PM12/10/15

to 'Yannick Duchêne' via ats-lang-users

'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> skribis:

set of axioms. :)

A disproof can be done with ‘case ... =/=>’ so I am not sure a ‘false

proposition’ can’t exist. I’ve used it for reductio ad absurdum.

> Moreover ATS propositions are never false, they are always true, or can't

> exist at all, which is not a surprise, as ATS propositions are proof in the

> form of definitions, with `absprop` or in the form of inductive definitions

> with `dataprop` (which is not exactly the same as an axiomatic proof, an

> inductive definition is a safer assertion).

Maybe you just need to be more creative in creating an inconsistent
> exist at all, which is not a surprise, as ATS propositions are proof in the

> form of definitions, with `absprop` or in the form of inductive definitions

> with `dataprop` (which is not exactly the same as an axiomatic proof, an

> inductive definition is a safer assertion).

set of axioms. :)

A disproof can be done with ‘case ... =/=>’ so I am not sure a ‘false

proposition’ can’t exist. I’ve used it for reductio ad absurdum.

Dec 10, 2015, 5:51:25 PM12/10/15

to ats-lang-users

A 'prop' in ATS is for classifying types for proofs

(and 'type' is for classifying types for (run-time) values).

You could have

stacst False: prop

What you should not introduce is

prfun False_elim : {a:prop} False -> a // False implies everything

Because you can prove very thing if False_elim is available.

Here is an encoding of propositional logic in ATS:

http://www.cs.bu.edu/~hwxi/academic/courses/CS520/Fall15/code/lecture-09-21/prop-logic.dats

You can see clearly that 'False' is indeed encoded.

Dec 10, 2015, 6:01:57 PM12/10/15

to ats-lang-users

Le jeudi 10 décembre 2015 23:41:19 UTC+1, Barry Schwartz a écrit :

Maybe you just need to be more creative in creating an inconsistent

set of axioms. :)

A disproof can be done with ‘case ... =/=>’ so I am not sure a ‘false

proposition’ can’t exist. I’ve used it for reductio ad absurdum.

So this is not sound:

`stadef h: prop -> bool = (lam p => true)`

?

And I can't use it in predicates without introducing inconsistencies?

Dec 10, 2015, 6:06:53 PM12/10/15

to ats-lang-users

Le jeudi 10 décembre 2015 23:51:25 UTC+1, gmhwxi a écrit :

Here is an encoding of propositional logic in ATS:

http://www.cs.bu.edu/~hwxi/academic/courses/CS520/Fall15/code/lecture-09-21/prop-logic.dats

You can see clearly that 'False' is indeed encoded.

Already seen some long time ago, but not studied. I will study it and see if it help.

Dec 10, 2015, 6:13:43 PM12/10/15

to ats-lang-users

Le jeudi 10 décembre 2015 23:41:19 UTC+1, Barry Schwartz a écrit :

Maybe you just need to be more creative in creating an inconsistent

set of axioms. :)

A disproof can be done with ‘case ... =/=>’ so I am not sure a ‘false

proposition’ can’t exist. I’ve used it for reductio ad absurdum.

To be back on that point, I was saying this can't happen with the assertions generated by an inductive definition.

Dec 10, 2015, 9:35:44 PM12/10/15

to ats-lang-users

Hope this can shed a bit light.

Let me use an example to explain the relation and difference

between the impredicative sort 'prop' and the predicative sort

'bool'.

dataprop

FACT(int, int) =

| FACTbas(0, 1)

| {n:pos}{r1:int}

FACTind(n, n*r1) of FACT(n-1, r1)

The above dataprop essentially introduces the following constants:

######

FACT: (int, int) -> prop

FACTbas: () -> FACT(0, 1)

FACTind:

{n:pos}{r1:int} FACT(n-1, r1) -> FACT(n, n*r1)

######

There exists a constant 'fact' corresponding to 'FACT':

fact: (int, int) -> bool

and the following first-order formulas are true:

######

(1)

fact(0, 1) = true

(2)

{n:pos}{r1:int}

fact(n-1, r1)=true implies fact(n, n*r1)=true

######

If there exists a closed value of the prop FACT(n, r), then

fact(n, r)=true holds. Another way to put it, if FACT(n, r) is

provable, then fact(n, r) is true.

Note that the existence of 'fact' is implied by the so-called

fixed-pointed theorem. Usually, 'fact' is taken to be the least

relation satisfying (1) and (2). So we know 'fact(0, 0)=false'

holds. However, the statement that there is no closed value of

the prop FACT(0, 0) is not provable inside ATS (Godel's incompleteness

result).

Let me use an example to explain the relation and difference

between the impredicative sort 'prop' and the predicative sort

'bool'.

dataprop

FACT(int, int) =

| FACTbas(0, 1)

| {n:pos}{r1:int}

FACTind(n, n*r1) of FACT(n-1, r1)

The above dataprop essentially introduces the following constants:

######

FACT: (int, int) -> prop

FACTbas: () -> FACT(0, 1)

FACTind:

{n:pos}{r1:int} FACT(n-1, r1) -> FACT(n, n*r1)

######

There exists a constant 'fact' corresponding to 'FACT':

fact: (int, int) -> bool

and the following first-order formulas are true:

######

(1)

fact(0, 1) = true

(2)

{n:pos}{r1:int}

fact(n-1, r1)=true implies fact(n, n*r1)=true

######

If there exists a closed value of the prop FACT(n, r), then

fact(n, r)=true holds. Another way to put it, if FACT(n, r) is

provable, then fact(n, r) is true.

Note that the existence of 'fact' is implied by the so-called

fixed-pointed theorem. Usually, 'fact' is taken to be the least

relation satisfying (1) and (2). So we know 'fact(0, 0)=false'

holds. However, the statement that there is no closed value of

the prop FACT(0, 0) is not provable inside ATS (Godel's incompleteness

result).

Dec 10, 2015, 10:20:39 PM12/10/15

to ats-lang-users

Le vendredi 11 décembre 2015 03:35:44 UTC+1, gmhwxi a écrit :

Hope this can shed a bit light.

Let me use an example to explain the relation and difference

between **the impredicative sort 'prop' and the predicative sort

'bool'**.

Interesting to see this question came back here :)

dataprop

FACT(int, int) =

| FACTbas(0, 1)

| {n:pos}{r1:int}

FACTind(n, n*r1) of FACT(n-1, r1)

The above dataprop essentially introduces the following constants:

######

FACT: (int, int) -> prop

FACTbas: () -> FACT(0, 1)

FACTind:

{n:pos}{r1:int} FACT(n-1, r1) -> FACT(n, n*r1)

######

There exists a constant 'fact' corresponding to 'FACT':

fact: (int, int) -> bool

and the following first-order formulas are true:

######

(1)

fact(0, 1) = true

(2)

{n:pos}{r1:int}

fact(n-1, r1)=true implies fact(n, n*r1)=true

######

This looks like what I had in mind, and that's why I though this was like it can only evaluates to a kind of true, or else fail, so no kind of `false`.

If there exists a closed value of the prop FACT(n, r), then

fact(n, r)=true holds. Another way to put it, if FACT(n, r) is

provable, then fact(n, r) is true.

What is a closed value? Is it related to function closure?

Note that the existence of 'fact' is implied by the so-called

fixed-pointed theorem. Usually, 'fact' is taken to be the least

relation satisfying (1) and (2). So we know 'fact(0, 0)=false'

holds. However, the statement that there is no closed value of

the prop FACT(0, 0) is not provable inside ATS (Godel's incompleteness

result).

I'm not a Godel theorem guru (just have an intuitive understanding of it), but I would say FACT does not assert there can't be any FACT(0,0), it just assert what it states to be true, and says nothing about the rest. Is it OK to say that?

A bit out of topic while not too much and may be nice for some ones, I just checked proofs can be type-annotated to make them explicit about their “content”.

I checked this example:

`dataprop SUM(int, int) =`

| SUMBase(0, 0)

| {x, y:int} SUMInd(x + 1, y + x + 1) of SUM(x, y)

fun sum {x:int; x >= 0} (a: int x): [y:int] (SUM(x, y) | int y) =

if a = 0 then (SUMBase | 0)

else let

val (pf1 | s) = sum(a - 1)

prval pf2 = SUMInd pf1

in (pf2 | s + a)

end

Can be rewritten in this more explicit way:

`dataprop SUM(int, int) =`

| SUMBase(0, 0)

| {x, y:int} SUMInd(x + 1, y + x + 1) of SUM(x, y)

fun sum {x:int; x >= 0} (a: int x): [y:int] (SUM(x, y) | int y) =

if a = 0 then (SUMBase:SUM(0, 0) | 0)

else let

val [y:int] (pf1:SUM(x - 1, y) | s:int y) = sum(a - 1)

prval pf2:SUM(x, y + x) = SUMInd pf1

in (pf2 | s + a)

end

Dec 10, 2015, 10:33:18 PM12/10/15

to ats-lang-users

A closed value is just a value that contains no free variables.

If you can prove something, then the proof you have must be a closed

value (as no dangling hypotheses are allowed).

Yes, the dataprop definition for FACT only tells you what can be

proven; it does not say anything about what cannot be proven. On the

other hand, the relation 'fact' corresponding to 'FACT' is a set, and we

know that either (0, 0) is in 'fact' or it is not in 'fact'.

If you can prove something, then the proof you have must be a closed

value (as no dangling hypotheses are allowed).

Yes, the dataprop definition for FACT only tells you what can be

proven; it does not say anything about what cannot be proven. On the

other hand, the relation 'fact' corresponding to 'FACT' is a set, and we

know that either (0, 0) is in 'fact' or it is not in 'fact'.

On Thursday, December 10, 2015 at 5:16:07 PM UTC-5, Yannick Duchêne wrote:

Dec 10, 2015, 11:13:58 PM12/10/15

to ats-lang-users

Le vendredi 11 décembre 2015 04:33:18 UTC+1, gmhwxi a écrit :

Yes, the dataprop definition for FACT only tells you what can be

proven; it does not say anything about what cannot be proven. On the

other hand, the relation 'fact' corresponding to 'FACT' is a set, and we

know that either (0, 0) is in 'fact' or it is not in 'fact'.

If I understand correctly, this may be all of what we know, because we may don't know how to compute it: we know it's either true or false, we know when it's true as FACT says how to compute it, and may not know when it's false, as FACT does not say how to compute it.

Another related wording question. Here is something I just wrote in my notes (which I hope a future day may become a kind of book):

#####

`dataprop P(int) =`

| Q(0) of () // Asserts Q(0) from ()

| Q(0) // Asserts Q(0) from nothing (same as above)

| R(1) of P(0) // Asserts R(1), that is P(1) from P(0)

| {i:int; i == 1} R(i) of P(0) // Same, with explicit constraint

| {i:int; i == 1} R(i) of [j: int; j == 0] P(j) // Even more.

This holds:

* `P: int -> prop`

* `Q: unit -> prop`

* `R: prop -> prop`

More precisely:

* `Q: unit -> P(0):prop`

* `R: P(0):prop -> P(1):prop`

I have two other wording questions.

About the argument `R` gets, what would be the proper expression to qualify it: a subset, a subtype or a constrained type or any of the three?

About `Q` and `R`, how to name it: is “proof of P” the only expression or is “clause” appropriate too?

Also, as the argument to `R` is both of type `prop` (type, at the static level) and can only get something returned by `P`, then `P` is both a function and a type. Is it OK to say it this way? (if that's OK, I will underline and put a stress on it… I like the idea of functions implying types)

Dec 11, 2015, 12:10:01 AM12/11/15

to ats-lang-users

P: int -> prop

So P is called a prop constructor (for construction props). P is usually not

called a function. P itself is not a prop; P(i) is a prop if i is of the sort int.

Note that prop should not be confused with concepts like proposition, predicates, etc.

To me, prop may be thought of as the collection of formulas that are assigned boolean

values in models.

Q: () -> P(0) // this is very different from writing: unit -> prop

Q is not a prop; the type of Q is a prop. Often Q is called a proof constructor

(as it is used to construct proofs).

R: P(0) -> P(1) // again, this is very different from prop -> prop

R is also a proof constructor; the argument of R is often called a proof.

So P is called a prop constructor (for construction props). P is usually not

called a function. P itself is not a prop; P(i) is a prop if i is of the sort int.

Note that prop should not be confused with concepts like proposition, predicates, etc.

To me, prop may be thought of as the collection of formulas that are assigned boolean

values in models.

Q: () -> P(0) // this is very different from writing: unit -> prop

Q is not a prop; the type of Q is a prop. Often Q is called a proof constructor

(as it is used to construct proofs).

R: P(0) -> P(1) // again, this is very different from prop -> prop

R is also a proof constructor; the argument of R is often called a proof.

Dec 11, 2015, 12:48:16 AM12/11/15

to ats-lang-users

Le vendredi 11 décembre 2015 06:10:01 UTC+1, gmhwxi a écrit :

Q: () -> P(0) // this is very different from writing: unit -> prop

Indeed, my apologies, I was silly (red-face):

`propdef p:prop = P(0) // OK and in the static.`

prval q:P(0) = Q // OK and in the dynamic, however erased by the compiler.

The type of `Q` is `P(0)` which is of sort `prop`.

[…] the argument of R is often called a proof.

So one must be able to say prop = proof. That makes sense, if P is not a prop constructor, not a prop.

That's OK, modulo my previous errors, everything is clear.

Your lights really lit :-P

Dec 11, 2015, 12:50:34 AM12/11/15

to ats-lang-users

Le vendredi 11 décembre 2015 06:48:16 UTC+1, Yannick Duchêne a écrit :

That makes sense, if P is not a prop constructor, not a prop.

Sorry, typo. I wanted to say “That makes sense, if P **is a prop** constructor, not a prop.”

Dec 11, 2015, 12:56:38 AM12/11/15

to ats-lan...@googlegroups.com

Yes, I think you have got it!

Just in case others read these messages, I would like to say this:--

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-user...@googlegroups.com.

To post to this group, send email to ats-lan...@googlegroups.com.

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

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/e038b307-4288-4cd6-ab5a-fa4e5d2f9d2d%40googlegroups.com.

Dec 11, 2015, 1:17:50 AM12/11/15

to ats-lang-users

Le vendredi 11 décembre 2015 06:56:38 UTC+1, gmhwxi a écrit :

A prop is like a type; a value classified by a prop is often called a proof,which is dynamic but erased by the compiler. So while proofs are dynamic,there is no proof construction at run-time.

A funny thing about the dynamic aspect…

As said before:

`prval q:P(0) = Q`

And this too! :

`val q:P(0) = Q`

Just like one would write:

`val a:int = 0`

Even more funny:

`prval a:int = 0`

So a question comes: how much differently `prval` and `val` are handled? Is this only syntactic sugar or is there more?

Dec 11, 2015, 1:26:05 AM12/11/15

to ats-lan...@googlegroups.com

val ... // not erased

prval ... // erased after type-checking

prval ... // erased after type-checking

If you do

val q:P(0) = Q

Then the compiler should complain later as 'Q' is not available.

Try to compile the following code and see what happens:

prval a: int = 0

val b = a + 1

The generated C code contains PMVerr(...), which should point

you to the source of the error: no definition for 'a'.

--

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-user...@googlegroups.com.

To post to this group, send email to ats-lan...@googlegroups.com.

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

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/37f08799-c612-4dc6-a6e3-92c444e565f8%40googlegroups.com.

Jun 29, 2018, 7:50:19 PM6/29/18

to ats-lang-users

Le vendredi 11 décembre 2015 06:56:38 UTC+1, gmhwxi a écrit :

Yes, I think you have got it!Just in case others read these messages, I would like to say this:A prop is like a type; a value classified by a prop is often called a proof,which is dynamic but erased by the compiler. So while proofs are dynamic,there is no proof construction at run-time.

[…]

More than that, it seems the prop sort spans overs (or can holds?) the type and t@ype sorts all together.

If one can have this:

stadef t:t@ype = int

One can also have this, it type‑checks:

stadef t:prop = int

Similarly with the `type` sort:

stadef t:type = string

This type‑checks too:

stadef t:prop = string

Given this:

stadef t:prop = int

extern fn f(): t

Then the return type of f is of sort t@ype. The original sort is retrieved back. That’s why I wrote above in parentheses, “(or can holds?)”

Since given this:

stacst t:prop

This, is not valid:

extern fn f(): t // Does not type‑check

But this, is valid and returns something of sort prop:

extern prfn g(): t

Not only the prop sort spans overs t@ype and type, but also over a unique world of its own.

In the above, `view` may be substituted for `prop` and it would be the same.

This makes sens, as a there can be a proof to walk hand‑in‑hand with any result type (in the dynamic), gives a view of it, although it does not interfere with it and is like in a parallel world. This relation between prop (or view) and the others sorts, calls for some meditation.

Hope I did not say anything too much silly or naive.

Jun 30, 2018, 7:37:03 AM6/30/18

to ats-lan...@googlegroups.com

Currently, we have the following subsort relation:

prop < t@ype < type

view < view@type < viewtype

view < prop

viewt@ype < t@ype

viewtype < type

--

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/9568a1dd-a7c3-4da5-ae9a-2c3219c2a697%40googlegroups.com.

Jun 30, 2018, 8:08:04 AM6/30/18

to ats-lang-users

Le samedi 30 juin 2018 13:37:03 UTC+2, gmhwxi a écrit :

Currently, we have the following subsort relation:prop < t@ype < typeview < view@type < viewtypeview < propviewt@ype < t@ypeviewtype < type

This list is a treasure. For t@ype < type and view < prop it looks obvious. For the others, I will need further more meditation :-p (especially the relation between prop and type is finally the other way)

Jul 2, 2018, 4:37:55 PM7/2/18

to ats-lang-users

Proofs so much belong to the dynamic, there is even a `prvar` (var, not val!)

Jul 26, 2018, 11:07:32 AM7/26/18

to ats-lang-users

Le samedi 30 juin 2018 13:37:03 UTC+2, gmhwxi a écrit :

Currently, we have the following subsort relation:prop < t@ype < typeview < view@type < viewtypeview < propviewt@ype < t@ypeviewtype < type

I’m confused again. I would rather read it the other way it is written. Ex. type < t@ype instead of type < t@ype, that is, a boxed type is a special case of boxed type.

Here is a test where the commented line needs to be uncommented only one at a time.

abstype abt

abst@ype aft

datatype bt = C

typedef ft = int

// absimpl abt = bt // Obviously.

// absimpl abt = ft // Flat type can’t implement abstract boxed type.

// absimpl aft = bt // Boxed type can implement abstract flat type.

// absimpl aft = ft // Obviously.

If a boxed type can implement an abstract flat type, this means a flat type is a special case of boxed type, just like a recursive function can implement a non‑recursive function because a non‑recursive function is a special case of (more general) recursive function.

In fewer word, boxed types are more general than flat types (except that there is no algebraic flat type).

Or am I wrong ?

If I’m not, then `prop < t@ype` should be read as “t@ype is a special case of prop”

Note for readers: `absimpl` is synonymous with `assume`, I just prefer `absimpl` which better says what it is.

Jul 26, 2018, 11:09:03 AM7/26/18

to ats-lang-users

Le jeudi 26 juillet 2018 17:07:32 UTC+2, Yannick Duchêne a écrit :

I’m confused again. I would rather read it the other way it is written. Ex. type < t@ype instead of type < t@ype, that is, a boxed type is a special case of boxed type.

Oh non, a typo. Please read “a flat type is a special case of boxed type”.

Jul 26, 2018, 11:26:31 AM7/26/18

to ats-lang-users

Le jeudi 26 juillet 2018 17:07:32 UTC+2, Yannick Duchêne a écrit :

Le samedi 30 juin 2018 13:37:03 UTC+2, gmhwxi a écrit :

Currently, we have the following subsort relation:prop < t@ype < type

[…][…]

In fewer word, boxed types are more general than flat types (except that there is no algebraic flat type).Or am I wrong ?

[…]

Yes, I was wrong, I messed‑up, sorry. t@ype < type indeed clearly means boxed types are more general than flat types.

My apologies for the disturbance.

Jul 26, 2018, 6:12:00 PM7/26/18

to ats-lan...@googlegroups.com

Here is a simple way to see it:

'type' is of size 1 and 't@ype' is of unknown size.

If the code works for `t@ype`, then it should also work

for 'type`.

--

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/a6654183-1402-412f-b71e-b52c6596102c%40googlegroups.com.

Reply all

Reply to author

Forward

0 new messages