🚀 go-pugleaf

dat@ukc.ac.uk (D.A.Turner) writes:

> There  is  no  special  difficulty  in
>reasoning   about  the  *time*  complexity  of  programs  written  in  a
>non-strict  functional  language.   One  can  derive  from  the  program
>equations   for  functions  fi  say,  similar  equations  for  Tfi,  the
>time-to-execute of function fi. There is quite  a  nice  discussion  of
>this,   with   some   examples,  in  chapter  6  of  Bird  and  Wadler's
>"Introduction to Functional Programming".

I think there is some "special difficulty" in reasoning about the time
complexity of non-strict programs, and that B + W have chosen to
de-emphasise these problems.  The "similar equations for Tfi" given by B+W are
entirely context sensitive. For example, the statement (Ch 6 p138) that
	T_reverse = O (n^2) 
(the time to compute the naive reversal of a list is order n-squared)
depends entirely on the assumption that the entire list is computed. 

For example, given a definition  of the form 
 f3 x = f1 (f2 x) 
with your/B&W's "similar equations" for Tf1 and Tf2, it is *not* the case that
 Tf3 x = (Tf2 x) + (Tf1 (f2 x)) 
because of 
(i) lazy evaluation, which makes the cost of evaluating f2 dependent
on its consumer f1, and
(ii) higher order functions, which can make the time to evaluate f1
dependent on more than just the (extensional) value of (f2 x), in the case
that (f2 x) is a function (and similarly for f2 if x is of function type).

As a simple example (of (i)), take f2 = reverse and f1 = head. It should not be
too hard to see that the time to evaluate f3 is linear in the length
of its argument.

Nonetheless, I still agree with the second point:

>On the other  hand  reasoning  about  the  *space*  complexity  of  such
>programs seems to be much more difficult.

Dave.

----------------------------------------------------------

For anyone who might be interested, issues (i) and (ii) are considered
in some detail in my thesis. Here are some other related references,
some of which were mentioned recently in this group.

(My stuff is available by anonymous ftp from directory papers/Sands
at theory.doc.ic.ac.uk)

@phdthesis{Bjerner:PhD,
    author = "B. Bjerner",
    title = "Time Complexity of Programs in Type Theory",
    school = "Chalmers University of Technology",
    year = 1989 }

@inproceedings{Bjerner:Holmstrom:Compositional,
    author = {B. Bjerner and S. Holmstr\"om},
    title = "A compositional approach to time analysis of first order lazy 
                functional programs",
    booktitle = "Functional {P}rogramming {L}anguages and {C}omputer {A}rchitecture, conference proceedings",
    publisher = {ACM press},
    year =          {1989}
        }

@inproceedings{Metayer:Analysis,
        author = "{LeM\'etayer}, D.",
        title = "Analysis of Functional Programs by Program Transformation",
        booktitle = "Second France--Japan Artificial Intelligence and Computer
                 Science Symposium",
        month = "",
        publisher = "North--Holland",
        year = 1988}

@inproceedings{Sands:GFPW,
        author =        "D. Sands",
        title =         "Complexity Analysis for a Lazy Higher-Order Language",
        booktitle =     
{Proceedings of  Glasgow Workshop on Functional Programming },
        publisher =     {Springer Verlag},
        series =        {Workshop Series},
        month =         {August},
        year =          {1989},
        }

@PhDThesis{Sands:PhD,
  author =      "D. Sands",
  title =       "Calculi for Time Analysis of Functional Programs",
  school =      "Imperial College",
  year =        "1990",
  month =       "September",
  OPTnote =     ""
}

@InProceedings{Sands:FSTandTCS,
  author =      "D. Sands",
  title =       "Time Analysis, Cost Equivalence and Program Refinement",
  booktitle =   "Proceedings of the Eleventh Conference on Foundations
                 of Software Technology and Theoretical Computer Science",
  year =        "1991",
  pages =       "25--39",
  publisher =   "Springer-Verlag",
  number =      "560",
  series =      "{L}{N}{C}{S}",
   month =       "December"
}

@inproceedings{Wadler:Strictness:Time,
    author = "P. Wadler",
    title = "Strictness Analysis Aids Time Analysis",
    booktitle = "15th ACM Symposium on Principals of Programming Languages",
    month = "January",
    year = 1988}



--