Question about ATS paper

[Hiroshi Sakurai]

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.

[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 :)

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

[Hiroshi Sakurai]

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:

[Hongwei Xi]

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.

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

[Yannick Duchêne]

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.

[gmhwxi]

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.

[Hiroshi Sakurai]

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:

[gmhwxi]

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.

[Yannick Duchêne]

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? 

[gmhwxi]

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.

[Hiroshi Sakurai]

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: