Trying Project Euler in ATS

Google Group
1

Here is the link to Project Euler:

https://projecteuler.net

In the past, I found it quite interesting to solve in ATS some of the
problems published
at Project Euler. This can also be particularly effective for teaching
oneself various concepts
of program verification.

I have just set up the following ATS-project:

I hope that the ATS community will have a considerably significant amount
of interest in this
so that this effort can continue in a meaningful way.

Let me take the first problem (https://projecteuler.net/problem=1) as an
example:

If we list all the natural numbers below 10 that are multiples of 3 or 5,
we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:

This specification has been implemented in the following file:

In general, a problem can have multiple specifications and each
specification can have multiple solutions
(that is, implementations).

I hope that people interested in this will contribute both specifications
and solutions. As a community, we
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If you
contribute, please send your code to
this list or to me directly.

The following link leads to a solution to the first problem that can be
type-checked using Patsopt-as-a-service
(Patsoptaas):

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats

The following link leads to a variant of the above solution that can be
tested (that is, run) using Patsopt-as-a-service:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats

Cheers!

2

P1 is not very interesting. P16 is a very good one.
The specification I gave for P16 is not yet a full specification.

Solving math puzzles in ATS can be a very effective way to learn dependent
types
and programming with theorem-proving. It can help one quickly grow familiar
with type-checking
and type-error messages.

Doing something “useful” or “realistic” is always very hard at the
beginning.
Before one can play Chopin or Brahms, one probably needs to play “Twinkle,
twinkle, little star” :)On Friday, January 16, 2015 at 1:34:05 AM UTC-5, Brandon Barker wrote:

This does seem like a good way to learn ATS/LF, but at the risk of
sounding obtuse, after staring at the specification of P1 a while, I have
to wonder if it would be necessary to write an implementation to prove my
specification ;). I think Knuth has an applicable quote here, so it can’t
hurt at least. The typechecker can only prove coherency, not that I haven’t
proved something else, after all.

Then again, proving something by accident unintentionally may be rare as
well.

All that said, I guess as is pointed out in the ATS book, you probably get
used to these recursive proofs after a while.

On Wed, Jan 14, 2015 at 11:34 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

FYI.

I wrote a README available here:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER

On Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:

FYI.

Problem 16

2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.

What is the sum of the digits of the number 2^1000?

Here is the specification for this problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P16/P16.sats

Note that the specification in P16.sats is not yet a “full”
specification. If there is some interest, we could
do one later.

On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:

FYI.

Even Fibonacci numbers

Problem 2

Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will
be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms.

Here is the specification for the second problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P2/P2.sats

Any solutions/implementations :slight_smile:

On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:

Here is the link to Project Euler:

https://projecteuler.net

In the past, I found it quite interesting to solve in ATS some of the
problems published
at Project Euler. This can also be particularly effective for teaching
oneself various concepts
of program verification.

I have just set up the following ATS-project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/
master/projects/MEDIUM/PEULER

I hope that the ATS community will have a considerably significant
amount of interest in this
so that this effort can continue in a meaningful way.

Let me take the first problem (#1 Multiples of $3$ or $5$ - Project Euler) as
an example:

If we list all the natural numbers below 10 that are multiples of 3 or
5, we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:
https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P1/P1.sats

This specification has been implemented in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats

In general, a problem can have multiple specifications and each
specification can have multiple solutions
(that is, implementations).

I hope that people interested in this will contribute both
specifications and solutions. As a community, we
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If
you contribute, please send your code to
this list or to me directly.

The following link leads to a solution to the first problem that can
be type-checked using Patsopt-as-a-service
(Patsoptaas):

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_
serve.php?mycode_url=https://raw.githubusercontent.com/
githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/
P1//P1-hwxi.dats

The following link leads to a variant of the above solution that can
be tested (that is, run) using Patsopt-as-a-service:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_
serve.php?mycode_url=https://raw.githubusercontent.com/
githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/
P1/JS/P1-hwxi.dats

Cheers!

–
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 <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
Brandon Barker
brand...@gmail.com <javascript:>

3

FYI.

I wrote a README available here:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULEROn Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:

FYI.

Problem 16

2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.

What is the sum of the digits of the number 2^1000?

Here is the specification for this problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P16/P16.sats

Note that the specification in P16.sats is not yet a “full” specification.
If there is some interest, we could
do one later.

On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:

FYI.

Even Fibonacci numbers

Problem 2

Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms.

Here is the specification for the second problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P2/P2.sats

Any solutions/implementations :slight_smile:

On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:

Here is the link to Project Euler:

https://projecteuler.net

In the past, I found it quite interesting to solve in ATS some of the
problems published
at Project Euler. This can also be particularly effective for teaching
oneself various concepts
of program verification.

I have just set up the following ATS-project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER

I hope that the ATS community will have a considerably significant
amount of interest in this
so that this effort can continue in a meaningful way.

Let me take the first problem (#1 Multiples of $3$ or $5$ - Project Euler) as
an example:

If we list all the natural numbers below 10 that are multiples of 3 or 5
, we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats

This specification has been implemented in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats

In general, a problem can have multiple specifications and each
specification can have multiple solutions
(that is, implementations).

I hope that people interested in this will contribute both
specifications and solutions. As a community, we
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If you
contribute, please send your code to
this list or to me directly.

The following link leads to a solution to the first problem that can be
type-checked using Patsopt-as-a-service
(Patsoptaas):

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats

The following link leads to a variant of the above solution that can be
tested (that is, run) using Patsopt-as-a-service:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats

Cheers!

4

This does seem like a good way to learn ATS/LF, but at the risk of sounding
obtuse, after staring at the specification of P1 a while, I have to wonder
if it would be necessary to write an implementation to prove my
specification ;). I think Knuth has an applicable quote here, so it can’t
hurt at least. The typechecker can only prove coherency, not that I haven’t
proved something else, after all.

Then again, proving something by accident unintentionally may be rare as
well.

All that said, I guess as is pointed out in the ATS book, you probably get
used to these recursive proofs after a while.On Wed, Jan 14, 2015 at 11:34 PM, gmhwxi gmh...@gmail.com wrote:

FYI.

I wrote a README available here:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER

On Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:

FYI.

Problem 16

2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.

What is the sum of the digits of the number 2^1000?

Here is the specification for this problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P16/P16.sats

Note that the specification in P16.sats is not yet a “full”
specification. If there is some interest, we could
do one later.

On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:

FYI.

Even Fibonacci numbers

Problem 2

Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will be
:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms.

Here is the specification for the second problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P2/P2.sats

Any solutions/implementations :slight_smile:

On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:

Here is the link to Project Euler:

https://projecteuler.net

In the past, I found it quite interesting to solve in ATS some of the
problems published
at Project Euler. This can also be particularly effective for teaching
oneself various concepts
of program verification.

I have just set up the following ATS-project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/
master/projects/MEDIUM/PEULER

I hope that the ATS community will have a considerably significant
amount of interest in this
so that this effort can continue in a meaningful way.

Let me take the first problem (#1 Multiples of $3$ or $5$ - Project Euler) as
an example:

If we list all the natural numbers below 10 that are multiples of 3 or
5, we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:
https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P1/P1.sats

This specification has been implemented in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats

In general, a problem can have multiple specifications and each
specification can have multiple solutions
(that is, implementations).

I hope that people interested in this will contribute both
specifications and solutions. As a community, we
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If you
contribute, please send your code to
this list or to me directly.

The following link leads to a solution to the first problem that can be
type-checked using Patsopt-as-a-service
(Patsoptaas):

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_
serve.php?mycode_url=https://raw.githubusercontent.com/
githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/
P1//P1-hwxi.dats

The following link leads to a variant of the above solution that can be
tested (that is, run) using Patsopt-as-a-service:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_
serve.php?mycode_url=https://raw.githubusercontent.com/
githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/
P1/JS/P1-hwxi.dats

Cheers!

–
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/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

5

Then again, proving something by accident unintentionally may be rare as
well.

I don’t remember encountering any for all these (10?) years.On Fri, Jan 16, 2015 at 1:33 AM, Brandon Barker brandon...@gmail.com wrote:

This does seem like a good way to learn ATS/LF, but at the risk of
sounding obtuse, after staring at the specification of P1 a while, I have
to wonder if it would be necessary to write an implementation to prove my
specification ;). I think Knuth has an applicable quote here, so it can’t
hurt at least. The typechecker can only prove coherency, not that I haven’t
proved something else, after all.

Then again, proving something by accident unintentionally may be rare as
well.

All that said, I guess as is pointed out in the ATS book, you probably get
used to these recursive proofs after a while.

On Wed, Jan 14, 2015 at 11:34 PM, gmhwxi gmh...@gmail.com wrote:

FYI.

I wrote a README available here:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER

On Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:

FYI.

Problem 16

2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.

What is the sum of the digits of the number 2^1000?

Here is the specification for this problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P16/P16.sats

Note that the specification in P16.sats is not yet a “full”
specification. If there is some interest, we could
do one later.

On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:

FYI.

Even Fibonacci numbers

Problem 2

Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will
be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms.

Here is the specification for the second problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P2/P2.sats

Any solutions/implementations :slight_smile:

On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:

Here is the link to Project Euler:

https://projecteuler.net

In the past, I found it quite interesting to solve in ATS some of the
problems published
at Project Euler. This can also be particularly effective for teaching
oneself various concepts
of program verification.

I have just set up the following ATS-project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/
master/projects/MEDIUM/PEULER

I hope that the ATS community will have a considerably significant
amount of interest in this
so that this effort can continue in a meaningful way.

Let me take the first problem (#1 Multiples of $3$ or $5$ - Project Euler) as
an example:

If we list all the natural numbers below 10 that are multiples of 3 or
5, we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:
https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P1/P1.sats

This specification has been implemented in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/
master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats

In general, a problem can have multiple specifications and each
specification can have multiple solutions
(that is, implementations).

I hope that people interested in this will contribute both
specifications and solutions. As a community, we
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If
you contribute, please send your code to
this list or to me directly.

The following link leads to a solution to the first problem that can
be type-checked using Patsopt-as-a-service
(Patsoptaas):

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_
serve.php?mycode_url=https://raw.githubusercontent.com/
githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/
P1//P1-hwxi.dats

The following link leads to a variant of the above solution that can
be tested (that is, run) using Patsopt-as-a-service:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_
serve.php?mycode_url=https://raw.githubusercontent.com/
githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/
P1/JS/P1-hwxi.dats

Cheers!

–
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/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
Brandon Barker
brandon...@gmail.com

–
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/CAORbNRrXs_Qux4K6SL22en-uOnXeJM1MzZ89eKjZKecqwM5j6w%40mail.gmail.com
https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrXs_Qux4K6SL22en-uOnXeJM1MzZ89eKjZKecqwM5j6w%40mail.gmail.com?utm_medium=email&utm_source=footer
.

6

FYI.

Even Fibonacci numbers

Problem 2

Each new term in the Fibonacci sequence is generated by adding the previous
two terms. By starting with 1 and 2, the first 10 terms will be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms.

Here is the specification for the second problem:

Any solutions/implementations :)On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:

Here is the link to Project Euler:

https://projecteuler.net

In the past, I found it quite interesting to solve in ATS some of the
problems published
at Project Euler. This can also be particularly effective for teaching
oneself various concepts
of program verification.

I have just set up the following ATS-project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER

I hope that the ATS community will have a considerably significant amount
of interest in this
so that this effort can continue in a meaningful way.

Let me take the first problem (#1 Multiples of $3$ or $5$ - Project Euler) as an
example:

If we list all the natural numbers below 10 that are multiples of 3 or 5,
we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats

This specification has been implemented in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats

In general, a problem can have multiple specifications and each
specification can have multiple solutions
(that is, implementations).

I hope that people interested in this will contribute both specifications
and solutions. As a community, we
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If you
contribute, please send your code to
this list or to me directly.

The following link leads to a solution to the first problem that can be
type-checked using Patsopt-as-a-service
(Patsoptaas):

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats

The following link leads to a variant of the above solution that can be
tested (that is, run) using Patsopt-as-a-service:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats

Cheers!

7

FYI.

Problem 16

2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.

What is the sum of the digits of the number 2^1000?

Here is the specification for this problem:

Note that the specification in P16.sats is not yet a “full” specification.
If there is some interest, we could
do one later.On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:

FYI.

Even Fibonacci numbers

Problem 2

Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms.

Here is the specification for the second problem:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P2/P2.sats

Any solutions/implementations :slight_smile:

On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:

Here is the link to Project Euler:

https://projecteuler.net

In the past, I found it quite interesting to solve in ATS some of the
problems published
at Project Euler. This can also be particularly effective for teaching
oneself various concepts
of program verification.

I have just set up the following ATS-project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER

I hope that the ATS community will have a considerably significant amount
of interest in this
so that this effort can continue in a meaningful way.

Let me take the first problem (#1 Multiples of $3$ or $5$ - Project Euler) as an
example:

If we list all the natural numbers below 10 that are multiples of 3 or 5,
we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats

This specification has been implemented in the following file:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats

In general, a problem can have multiple specifications and each
specification can have multiple solutions
(that is, implementations).

I hope that people interested in this will contribute both specifications
and solutions. As a community, we
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If you
contribute, please send your code to
this list or to me directly.

The following link leads to a solution to the first problem that can be
type-checked using Patsopt-as-a-service
(Patsoptaas):

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats

The following link leads to a variant of the above solution that can be
tested (that is, run) using Patsopt-as-a-service:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats

Cheers!