Trying Project Euler in ATS

[gmhwxi]

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

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!

[gmhwxi]

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

[gmhwxi]

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.

[gmhwxi]

FYI.

I wrote a README available here:

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

[Brandon Barker]

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.

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

--

Brandon Barker
brandon...@gmail.com

[Hongwei Xi]

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

I don't remember encountering any for all these (10?) years.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrXs_Qux4K6SL22en-uOnXeJM1MzZ89eKjZKecqwM5j6w%40mail.gmail.com.

[gmhwxi]

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