Wording and interpretation: propositions, predicates and types

Google Group
1

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)

2

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)

3

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.On Thursday, December 10, 2015 at 11:13:58 PM UTC-5, Yannick Duchêne wrote:

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)

4

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).On Thursday, December 10, 2015 at 5:16:07 PM UTC-5, Yannick Duchêne wrote:

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)

5

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.

6

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:

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)

7

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?

8

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’.On Fri, Dec 11, 2015 at 1:17 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

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?

–
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
https://groups.google.com/d/msgid/ats-lang-users/37f08799-c612-4dc6-a6e3-92c444e565f8%40googlegroups.com?utm_medium=email&utm_source=footer
.

9

Maybe you just need to be more creative in creating an inconsistent
set of axioms. :slight_smile:

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.

10

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

11

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 :slight_smile:

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

12

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.*On Fri, Dec 11, 2015 at 12:48 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

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 :stuck_out_tongue:

–
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
https://groups.google.com/d/msgid/ats-lang-users/e038b307-4288-4cd6-ab5a-fa4e5d2f9d2d%40googlegroups.com?utm_medium=email&utm_source=footer
.

13

Maybe you just need to be more creative in creating an inconsistent
set of axioms. :slight_smile:

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?

14

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.On Thursday, December 10, 2015 at 5:41:19 PM UTC-5, Barry Schwartz wrote:

‘Yannick Duchêne’ via ats-lang-users <ats-l...@googlegroups.com
<javascript:>> 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. :slight_smile:

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.

15

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 :stuck_out_tongue: