[Agda] Deriving Maximum Segment Sum

[Shin-Cheng Mu]

Dear friends,

(My previous message was blocked due to large attachments,
  therefore I am posting again with URLs instead. )

One of my students was practising with Logic.ChainReasoning and
tried to prove the foldr-fusion rule, which he learnt from a
course on functional program derivation, using maximum segment
sum (MSS) as an example.

Seeing his proof, I am curious to know how much program derivation
I can do in Agda, and decided to try coding in the entire
derivation of MSS in Agda. I thought I could do it over the
weekend but it ended up taking the entire week. Anyway, here
it is!

As a reminder, given a list of (possibly negative) numbers,
the MSS is about computing the maximum sum among all its
consecutive segments. There exists a linear-time algorithm
whose derivation is mostly mechanical, making it a favourite
example. Attached are 5 Agda modules:

   o MSS.agda : the main program importing all the sub-modules.

   o ListProperties.agda :
       some properties I need about lists, such as fold fusion,
       concat . map (map f) = map f . concat, etc.
       Later in the development I realised that I should switch
       to non-empty lists, so not all of the properties here are
       used.

   o List+.agda :
       The function "max" returning the maximum element can
       either be defined on non-empty lists only, or return
       minus infinity when given an empty list. I chose the
       former approach, and defined non-empty lists and
       some of its properties in this file.

   o Derivation.agda :
       the main derivation of MSS. I tried to use a dependent
       pair to represent a "derivation", as seen in the definitions
       of "scanr" and "mss".

       The derivation is parameterised over any numerical
       data and operators + and ^ such that + is associative,
       and a + (b ^ c) = (a ^ b) + (a ^ c).

       The reason of this parameterisation, however, was that I
       did not know how to prove the properties above, until a
       smart student showed me the proof.

   o IntRNG.agda :
       proofs that Data.Int actually satisfy the properties above.
       (Not quite complete yet.)

Hope they would be of interest to some people.

sincerely,
Shin

URLs to the files:

http://www.iis.sinica.edu.tw/~scm/sw/2007/agda-mss/MSS.agda
http://www.iis.sinica.edu.tw/~scm/sw/2007/agda-mss/ListProperties.agda
http://www.iis.sinica.edu.tw/~scm/sw/2007/agda-mss/List+.agda
http://www.iis.sinica.edu.tw/~scm/sw/2007/agda-mss/Derivation.agda
http://www.iis.sinica.edu.tw/~scm/sw/2007/agda-mss/IntRNG.agda