Question about ATS paper

Google Group
1

Nice to meet you. All.
My name is Hiroshi Sakurai.
I am programmer in Tokyo Japanese.
ATS is very great language and fun.
I am sorry my english is poor.

I am reading ATS paper now.

http://www.ats-lang.org/MYDATA/ATS-types03.pdf

I am understand before Fig 2. Regularity Rules.

but I could not understand Fig.2.

Would you teach me Definition.1 more detail or another information, please?

thanks.

2

Thank you.
I am very honored your reply.
I’m grateful for your useful advice because I was quite addicted.
I will carefully read the DML of paper.
Thanks for your future support as well.

2014年12月19日金曜日 11時55分25秒 UTC+9 gmhwxi:

3

It is difficult.

⊤ : [] => bool
⊤ : [] => bool

----------------(reg-true)
Σ; P⃗ |=S ⊤

I think this is define ⊤ operator.

P⃗ is set of propositions under Σ.
⊤ is true proposition.

I think P⃗ include ⊤ true proposition.

but, I don’t know this rule.

----------------(reg-false)
Σ; P⃗,⊥ |=S P

I think ⊥ is false proposition.
P⃗ (set of propositions under Σ) plus ⊥(false proposition) constraint
relation P(proposition)?
Why this expression is not follow expression?

----------------(reg-false)
Σ; P⃗ |=S ⊥

2014年12月20日土曜日 16時34分09秒 UTC+9 Hiroshi Sakurai:

4

There is a little subtlety here.

In ATS, the constraint relation is about subtyping: T1 <= T2 does not imply
T2 <= T1.
In DML, the constraint relation is about equality on type indexes: I1 = I2
implies I2 = I1.On Sunday, December 21, 2014 4:21:24 PM UTC-5, Hiroshi Sakurai wrote:

Thank you very mach.
I understand this mean and this part of DML paper.
And I understand Define 1.

I found different of DML and ATS.
Why did you delete reg-eq-symm rule ?

2014年12月21日日曜日 2時30分04秒 UTC+9 gmhwxi:

Sigma; PP, false |= P

simply means that falsehood implies any proposition.

Sigma; PP |= false

means falsehood can be derived. This is not what we need.

On Sat, Dec 20, 2014 at 12:22 PM, Hiroshi Sakurai saku...@gmail.com wrote:

It is difficult.

⊤ : => bool
⊤ : => bool

----------------(reg-true)
Σ; P⃗ |=S ⊤

I think this is define ⊤ operator.

P⃗ is set of propositions under Σ.
⊤ is true proposition.

I think P⃗ include ⊤ true proposition.

but, I don’t know this rule.

----------------(reg-false)
Σ; P⃗,⊥ |=S P

I think ⊥ is false proposition.
P⃗ (set of propositions under Σ) plus ⊥(false proposition) constraint
relation P(proposition)?
Why this expression is not follow expression?

----------------(reg-false)
Σ; P⃗ |=S ⊥

2014年12月20日土曜日 16時34分09秒 UTC+9 Hiroshi Sakurai:

Thank you.
I am very honored your reply.
I’m grateful for your useful advice because I was quite addicted.
I will carefully read the DML of paper.
Thanks for your future support as well.

2014年12月19日金曜日 11時55分25秒 UTC+9 gmhwxi:

Thanks for your interest in ATS!

The paper you mentioned below is an abstract.
I suggest that you read the following one first:

http://www.ats-lang.org/Papers.html#Dependent_ML

which is a lot easier to access.

Definition 1 introduces an abstract constraint relation. The regularity
conditions in Figure 2 are a bit like axioms: Only a constraint
relation
that satisfies these conditions is considered “regular”. For instance,
we may consider a type of geometry “regular” if we can only draw one
line passing through a given point that is parallel to another given
line.

Hope this helps :slight_smile:

On Thursday, December 18, 2014 5:33:28 AM UTC-5, Hiroshi Sakurai wrote:

Nice to meet you. All.
My name is Hiroshi Sakurai.
I am programmer in Tokyo Japanese.
ATS is very great language and fun.
I am sorry my english is poor.

I am reading ATS paper now.

http://www.ats-lang.org/MYDATA/ATS-types03.pdf

I am understand before Fig 2. Regularity Rules.

but I could not understand Fig.2.

Would you teach me Definition.1 more detail or another information,
please?

thanks.

–
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...@googlegroups.com.
To post to this group, send email to ats-l...@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/e5b49771-28d1-4af5-acca-e841c9b4ea16%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/e5b49771-28d1-4af5-acca-e841c9b4ea16%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

What’s wrong with the extended abstract? I wanted to print it (I do not
have an ebook reader yet) to read it comfortably during the coming days,
and choose this one because it is shorter than others. That’s the reason
why I would like to know.Le vendredi 19 décembre 2014 03:55:25 UTC+1, gmhwxi a écrit :

Thanks for your interest in ATS!

The paper you mentioned below is an abstract.
I suggest that you read the following one first:

http://www.ats-lang.org/Papers.html#Dependent_ML

which is a lot easier to access.

6

In DML, we have I1 = I2 implies int(I1) = int(I2)

In ATS, there are no rules for deciding whether int(I1) <= int(I2).

There are endless possibilities. For instance:

  1. I1 = I2 implies int(I1) <= int(I2) if we interpret int(I) as the
    singleton type for I
  2. I1 <= I2 implies int(I1) <= int(I2) if we interpret int(I) as the type
    for all the integers <= I
  3. I1 >= I2 implies int(I1) <= int(I2) if we interpret int(I) as the type
    for all the integers >= I

In ATS/Positiats, (1) is chosen.On Monday, December 22, 2014 9:18:17 AM UTC-5, Yannick Duchêne wrote:

Le dimanche 21 décembre 2014 22:37:17 UTC+1, gmhwxi a écrit :

There is a little subtlety here.

In ATS, the constraint relation is about subtyping: T1 <= T2 does not
imply T2 <= T1.
In DML, the constraint relation is about equality on type indexes: I1 =
I2 implies I2 = I1.

Doesn’t the latter also applies to ATS?

7

Thank you very mach.
I understand this mean and this part of DML paper.
And I understand Define 1.

I found different of DML and ATS.
Why did you delete reg-eq-symm rule ?

2014年12月21日日曜日 2時30分04秒 UTC+9 gmhwxi:

8

Oh, nothing is wrong with the abstract.

It is a bit of the so-called Bourbaki-style. Math books written in
Bourbaki-style
can be challenging for beginners but they are really good for those who are
able
to appreciate them.On Saturday, December 20, 2014 6:45:11 PM UTC-5, Yannick Duchêne wrote:

What’s wrong with the extended abstract? I wanted to print it (I do not
have an ebook reader yet) to read it comfortably during the coming days,
and choose this one because it is shorter than others. That’s the reason
why I would like to know.

Le vendredi 19 décembre 2014 03:55:25 UTC+1, gmhwxi a écrit :

Thanks for your interest in ATS!

The paper you mentioned below is an abstract.
I suggest that you read the following one first:

http://www.ats-lang.org/Papers.html#Dependent_ML

which is a lot easier to access.

9

Sigma; PP, false |= P

simply means that falsehood implies any proposition.

Sigma; PP |= false

means falsehood can be derived. This is not what we need.On Sat, Dec 20, 2014 at 12:22 PM, Hiroshi Sakurai sakur...@gmail.com wrote:

It is difficult.

⊤ : => bool
⊤ : => bool

----------------(reg-true)
Σ; P⃗ |=S ⊤

I think this is define ⊤ operator.

P⃗ is set of propositions under Σ.
⊤ is true proposition.

I think P⃗ include ⊤ true proposition.

but, I don’t know this rule.

----------------(reg-false)
Σ; P⃗,⊥ |=S P

I think ⊥ is false proposition.
P⃗ (set of propositions under Σ) plus ⊥(false proposition) constraint
relation P(proposition)?
Why this expression is not follow expression?

----------------(reg-false)
Σ; P⃗ |=S ⊥

2014年12月20日土曜日 16時34分09秒 UTC+9 Hiroshi Sakurai:

Thank you.
I am very honored your reply.
I’m grateful for your useful advice because I was quite addicted.
I will carefully read the DML of paper.
Thanks for your future support as well.

2014年12月19日金曜日 11時55分25秒 UTC+9 gmhwxi:

Thanks for your interest in ATS!

The paper you mentioned below is an abstract.
I suggest that you read the following one first:

http://www.ats-lang.org/Papers.html#Dependent_ML

which is a lot easier to access.

Definition 1 introduces an abstract constraint relation. The regularity
conditions in Figure 2 are a bit like axioms: Only a constraint relation
that satisfies these conditions is considered “regular”. For instance,
we may consider a type of geometry “regular” if we can only draw one
line passing through a given point that is parallel to another given
line.

Hope this helps :slight_smile:

On Thursday, December 18, 2014 5:33:28 AM UTC-5, Hiroshi Sakurai wrote:

Nice to meet you. All.
My name is Hiroshi Sakurai.
I am programmer in Tokyo Japanese.
ATS is very great language and fun.
I am sorry my english is poor.

I am reading ATS paper now.

http://www.ats-lang.org/MYDATA/ATS-types03.pdf

I am understand before Fig 2. Regularity Rules.

but I could not understand Fig.2.

Would you teach me Definition.1 more detail or another information,
please?

thanks.

–
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/e5b49771-28d1-4af5-acca-e841c9b4ea16%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/e5b49771-28d1-4af5-acca-e841c9b4ea16%40googlegroups.com?utm_medium=email&utm_source=footer
.

10

I understand this meaning that ATS deleted reg-eq-symm rule because added
subtyping.
I am reading Figure 5 of Dynamics now.
Academic paper is difficult but interesting !
My pace is very slow but continue.
thank you.
2014年12月23日火曜日 5時25分19秒 UTC+9 gmhwxi:

11

There is a little subtlety here.

In ATS, the constraint relation is about subtyping: T1 <= T2 does not
imply T2 <= T1.
In DML, the constraint relation is about equality on type indexes: I1 = I2
implies I2 = I1.

Doesn’t the latter also applies to ATS?

12

Thanks for your interest in ATS!

The paper you mentioned below is an abstract.
I suggest that you read the following one first:

http://www.ats-lang.org/Papers.html#Dependent_ML

which is a lot easier to access.

Definition 1 introduces an abstract constraint relation. The regularity
conditions in Figure 2 are a bit like axioms: Only a constraint relation
that satisfies these conditions is considered “regular”. For instance,
we may consider a type of geometry “regular” if we can only draw one
line passing through a given point that is parallel to another given line.

Hope this helps :)On Thursday, December 18, 2014 5:33:28 AM UTC-5, Hiroshi Sakurai wrote:

Nice to meet you. All.
My name is Hiroshi Sakurai.
I am programmer in Tokyo Japanese.
ATS is very great language and fun.
I am sorry my english is poor.

I am reading ATS paper now.

http://www.ats-lang.org/MYDATA/ATS-types03.pdf

I am understand before Fig 2. Regularity Rules.

but I could not understand Fig.2.

Would you teach me Definition.1 more detail or another information,
please?

thanks.