Wording and interpretation: propositions, predicates and types

[Yannick Duchêne]

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?

http://ece.uprm.edu/~jseguel/ltoc2.pdf

https://www.quora.com/What-is-the-precise-difference-between-propositional-and-predicate-logic

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)

[Barry Schwartz]

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

> 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
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.

[gmhwxi]

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.

[Yannick Duchêne]

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?

 

[Yannick Duchêne]

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.

[Yannick Duchêne]

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. 

[gmhwxi]

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).

[Yannick Duchêne]

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:

http://fr.slideshare.net/mirrorren/ats-programming

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

[gmhwxi]

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'.

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

[Yannick Duchêne]

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)

[gmhwxi]

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.

[Yannick Duchêne]

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

[Yannick Duchêne]

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.”

[Hongwei Xi]

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.

--
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.

[Yannick Duchêne]

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?

[Hongwei Xi]

val ... // not erased
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.

[Yannick Duchêne]

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.

[Hongwei Xi]

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.

[Yannick Duchêne]

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

Currently, we have the following subsort relation:

prop < t@ype < type

view < view@type < viewtype

view < prop

viewt@ype < t@ype

viewtype < 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)

[Yannick Duchêne]

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

[Yannick Duchêne]

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

Currently, we have the following subsort relation:

prop < t@ype < type

view < view@type < viewtype

view < prop

viewt@ype < t@ype

viewtype < 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.

[Yannick Duchêne]

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”.

[Yannick Duchêne]

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. 

[Hongwei Xi]

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.