Natural numbers division

[Chotu_S]

How does division of natural numbers work ?

For example I want a function that takes any natural number “n” and return
a natural number “n / 2” (i.e positive integer quotient ) .

Thanks

[Chotu_S]

Thanks Brandon,

I’ll take a look inside the integers,sats .

But how do you compile following function :

fun div_by_2 {n:nat} ( n : int (n) ) : [m : nat ] int (m) = n/2

(* or *)

fun ddiv_by_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2 ] int (m) = n/2On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker brandon...@gmail.comwrote:

But it seems that, as in C, this is the default behavior (so my suggestion
above may not be necessary):

val n7 = 7
val n8 = 8

val n3 = n7/2
val () = println!(n3)
val () = assertloc (n3 = 3)
val n4 = n8/2
val () = println!(n4)
val () = assertloc (n4 = 4)

[gmhwxi]

Or you can use ‘half’.

In practice, if I don’t know a function in the ATS library
that does what ‘div_by_2’ is expected to do, then I will implement it:

fun div_by_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:

This g1int_ndiv(n,2) seems to work , it is defined in integers.sats file
.

Thanks

On Sat, Feb 1, 2014 at 7:43 PM, chotu s <cho...@gmail.com <javascript:>>wrote:

Thanks Brandon,

I’ll take a look inside the integers,sats .

But how do you compile following function :

fun div_by_2 {n:nat} ( n : int (n) ) : [m : nat ] int (m) = n/2

(* or *)

fun ddiv_by_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2 ] int (m) =
n/2

On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker <brand...@gmail.com<javascript:> wrote:

But it seems that, as in C, this is the default behavior (so my
suggestion above may not be necessary):

val n7 = 7
val n8 = 8

val n3 = n7/2
val () = println!(n3)
val () = assertloc (n3 = 3)
val n4 = n8/2
val () = println!(n4)
val () = assertloc (n4 = 4)

[Chotu_S]

This g1int_ndiv(n,2) seems to work , it is defined in integers.sats file .

ThanksOn Sat, Feb 1, 2014 at 7:43 PM, chotu s chot...@gmail.com wrote:

Thanks Brandon,

I’ll take a look inside the integers,sats .

But how do you compile following function :

fun div_by_2 {n:nat} ( n : int (n) ) : [m : nat ] int (m) = n/2

(* or *)

fun ddiv_by_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2 ] int (m) = n/2

On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker brandon...@gmail.comwrote:

But it seems that, as in C, this is the default behavior (so my
suggestion above may not be necessary):

val n7 = 7
val n8 = 8

val n3 = n7/2
val () = println!(n3)
val () = assertloc (n3 = 3)
val n4 = n8/2
val () = println!(n4)
val () = assertloc (n4 = 4)

[Brandon_Barker]

But it seems that, as in C, this is the default behavior (so my suggestion
above may not be necessary):

val n7 = 7
val n8 = 8

val n3 = n7/2
val () = println!(n3)
val () = assertloc (n3 = 3)
val n4 = n8/2
val () = println!(n4)
val () = assertloc (n4 = 4)

[Brandon_Barker]

You may want to check out prelude/SATS/integer.sats for this sort of
thing (search for “div”). prelude_integer.dats has some related
examples.
Brandon Barker
brandon…@gmail.comOn Sat, Feb 1, 2014 at 7:07 AM, chotu s chot...@gmail.com wrote:

How does division of natural numbers work ?

For example I want a function that takes any natural number “n” and return
a natural number “n / 2” (i.e positive integer quotient ) .

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.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/03a04197-a32a-49eb-97fa-bd94509cbcfb%40googlegroups.com.

[Chotu_S]

I agree with you , but I need to practice using such tool and I plan to do
so for most part of this year for small set of code only.

Also I don’t start code with dependent types but later after I get a
working code do I try convert to dependent types.

I just wanted to convert some contracts into ATS for quick sort algorithm ,
it was just a mechanical process(not a pragmatic one). So I eventually
managed to get some of it converted , the code is given here : qs.datshttps://bitbucket.org/chotu/ats-explore/src/0dce1c05b6007fc876e4703c4c1c7d42a7048f2d/r1d1qs/qs.dats?at=master

I’ll try to convert other contracts/invariants for this code to ATS as I
get more familiar/practice with ATS .

I did not struggle with ATS , but with my stupidity and silly mistakes
(for example change in order of args . incorrect spec , etc).

I must say that I now starting to like ATS , most of the stuff is intuitive
I believe

ThanksOn Saturday, February 1, 2014 9:11:34 PM UTC+5:30, gmhwxi wrote:

I just want to add a note that reflects my current view of program
verification:

First and foremost, program verification is the thought process that
justifies to oneself why
one’s code is correct (in a general and broad sense). Using tools (e.g.,
typecheckers, theorem-provers)
to ensure the correctness of this thought process is a secondary issue.
This view is largely based
on the way in which people construct mathematical proofs.

On Saturday, February 1, 2014 10:25:49 AM UTC-5, gmhwxi wrote:

Or you can use ‘half’.

In practice, if I don’t know a function in the ATS library
that does what ‘div_by_2’ is expected to do, then I will implement it:

fun div_by_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)

On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:

This g1int_ndiv(n,2) seems to work , it is defined in integers.sats file
.

Thanks

On Sat, Feb 1, 2014 at 7:43 PM, chotu s cho...@gmail.com wrote:

Thanks Brandon,

I’ll take a look inside the integers,sats .

But how do you compile following function :

fun div_by_2 {n:nat} ( n : int (n) ) : [m : nat ] int (m) = n/2

(* or *)

fun ddiv_by_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2 ] int (m) =
n/2

On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker brand...@gmail.comwrote:

But it seems that, as in C, this is the default behavior (so my
suggestion above may not be necessary):

val n7 = 7
val n8 = 8

val n3 = n7/2
val () = println!(n3)
val () = assertloc (n3 = 3)
val n4 = n8/2
val () = println!(n4)
val () = assertloc (n4 = 4)

[gmhwxi]

I just want to add a note that reflects my current view of program
verification:

First and foremost, program verification is the thought process that
justifies to oneself why
one’s code is correct (in a general and broad sense). Using tools (e.g.,
typecheckers, theorem-provers)
to ensure the correctness of this thought process is a secondary issue.
This view is largely based
on the way in which people construct mathematical proofs.On Saturday, February 1, 2014 10:25:49 AM UTC-5, gmhwxi wrote:

Or you can use ‘half’.

In practice, if I don’t know a function in the ATS library
that does what ‘div_by_2’ is expected to do, then I will implement it:

fun div_by_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)

On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:

This g1int_ndiv(n,2) seems to work , it is defined in integers.sats file
.

Thanks

On Sat, Feb 1, 2014 at 7:43 PM, chotu s cho...@gmail.com wrote:

Thanks Brandon,

I’ll take a look inside the integers,sats .

But how do you compile following function :

fun div_by_2 {n:nat} ( n : int (n) ) : [m : nat ] int (m) = n/2

(* or *)

fun ddiv_by_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2 ] int (m) =
n/2

On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker brand...@gmail.comwrote:

But it seems that, as in C, this is the default behavior (so my
suggestion above may not be necessary):

val n7 = 7
val n8 = 8

val n3 = n7/2
val () = println!(n3)
val () = assertloc (n3 = 3)
val n4 = n8/2
val () = println!(n4)
val () = assertloc (n4 = 4)

[gmhwxi]

Good to know that you like it

In my note, I mainly meant:

1. one should have a good understanding what kind of proof is expected when
   trying to construct it in ATS
2. Do not be shy away from using unsafe casting ($UN.cast…): Get a proof
   first and worry about casting later.On Sunday, February 2, 2014 5:05:08 AM UTC-5, chotu s wrote:

I agree with you , but I need to practice using such tool and I plan to do
so for most part of this year for small set of code only.

Also I don’t start code with dependent types but later after I get a
working code do I try convert to dependent types.

I just wanted to convert some contracts into ATS for quick sort algorithm
, it was just a mechanical process(not a pragmatic one). So I eventually
managed to get some of it converted , the code is given here : qs.datshttps://bitbucket.org/chotu/ats-explore/src/0dce1c05b6007fc876e4703c4c1c7d42a7048f2d/r1d1qs/qs.dats?at=master

I’ll try to convert other contracts/invariants for this code to ATS as I
get more familiar/practice with ATS .

I did not struggle with ATS , but with my stupidity and silly mistakes
(for example change in order of args . incorrect spec , etc).

I must say that I now starting to like ATS , most of the stuff is
intuitive I believe

Thanks

On Saturday, February 1, 2014 9:11:34 PM UTC+5:30, gmhwxi wrote:

I just want to add a note that reflects my current view of program
verification:

First and foremost, program verification is the thought process that
justifies to oneself why
one’s code is correct (in a general and broad sense). Using tools (e.g.,
typecheckers, theorem-provers)
to ensure the correctness of this thought process is a secondary issue.
This view is largely based
on the way in which people construct mathematical proofs.

On Saturday, February 1, 2014 10:25:49 AM UTC-5, gmhwxi wrote:

Or you can use ‘half’.

In practice, if I don’t know a function in the ATS library
that does what ‘div_by_2’ is expected to do, then I will implement it:

fun div_by_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)

On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:

This g1int_ndiv(n,2) seems to work , it is defined in integers.sats
file .

Thanks

On Sat, Feb 1, 2014 at 7:43 PM, chotu s cho...@gmail.com wrote:

Thanks Brandon,

I’ll take a look inside the integers,sats .

But how do you compile following function :

fun div_by_2 {n:nat} ( n : int (n) ) : [m : nat ] int (m) = n/2

(* or *)

fun ddiv_by_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2 ] int (m)
= n/2

On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker brand...@gmail.comwrote:

But it seems that, as in C, this is the default behavior (so my
suggestion above may not be necessary):

val n7 = 7
val n8 = 8

val n3 = n7/2
val () = println!(n3)
val () = assertloc (n3 = 3)
val n4 = n8/2
val () = println!(n4)
val () = assertloc (n4 = 4)