Are there any benefits to calculating the time complexity of an algorithm using lambda calculus? Or is there another system designed for this purpose?
Any references would be appreciated.
$\begingroup$
$\endgroup$
0
Add a comment
|
7 Answers
$\begingroup$
$\endgroup$
2
Ohad is quite right about the problems that the lambda calculus faces as a basis for talking about complexity classes. There has been a fair bit of work done on characterising complexity of reducibility in the lambda calculus, particularly around the work on labelled and optimal reductions from Lèvy's PhD thesis. Generally speaking, good cost models for the lambda calculus should not assign a constant weight to all beta reductions: intuitively, substituting a large subterm into many, differently scoped places should cost more than contracting a small K redex, and if one wants a certain amount of invariance of cost under different rewrite strategies, this becomes essential.
Two links:
- Lawall & Mairson, 1996, Optimality and inefficiency: what isn't a cost model of the lambda calculus? (.ps.gz) – Seminal survey of issues bearing on choice of cost model, and why many plausible ideas don't work.
- Dal Lago & Martini, 2008, The weak lambda calculus as a reasonable machine – Offers a cost model for the call-by-value lambda calculus, together with good discussion of the literature.
-
1$\begingroup$ Interesting references, I didn't know about these works. $\endgroup$ Commented Aug 22, 2010 at 21:21
-
1$\begingroup$ The situation has changed recently on this topic. See my answer below. $\endgroup$– MarcCommented Dec 26, 2015 at 15:53
$\begingroup$
$\endgroup$
A recent developpement on this topic: U. dal Lago and B. Accatoli proved that the length of the leftmost-outermost reduction (LOr) of a $\lambda$-term is an invariant (time) cost model for $\lambda$-calculus.
They show that Turing machines (with cost=time) and $\lambda$-terms (with cost=length of the LOr) can simulate each other with a polynomial overhead in time. So for instance the definition of the class P does not depend on which of the two computation model you use to define it.
$\begingroup$
$\endgroup$
0
There are quantitative results concerning $\lambda $-calculus, in the form of measuring the length of reductions in (typed-)lambda calculus. But this is of course far from saying anything about the complexity of algorithms (especially that the bounds obtained are fast-growing). See for example: Arnold Beckmann, Exact bounds for lengths of reductions in typed $\lambda $-calculus, Journal of Symbolic Logic 2001, 66(3): 1277-1285.
For something closer to your question, there is a current project that develops and studies a type-system (a functional programing language) which by static-analysis can determine (polynomial) run-time bounds of programs (as well as other resources used by programs). So in some sense, this might hint that there might be some advantage in using functional-programing for analyzing run-time complexity. The project homepage is here.
A possibly representative paper of this project is: Jan Hoffmann, Martin Hofmann. Amortized Resource Analysis with Polynomial Potential - A Static Inference of Polynomial Bounds for Functional Programs. In Proceedings of the 19th European Symposium on Programming (ESOP'10).link
answered Aug 21, 2010 at 22:48
$\begingroup$
$\endgroup$
There is a very interesting line of work based on linear logic, called implicit complexity theory, which characterizes various complexity classes by imposing various type disciplines on the lambda calculus. IIRC, this work began when Bellantoni and Cook, and Leivant figured out how to use the type system to bound primitive recursion to capture various complexity classes.
In general, the attraction to working with lambda calculi is that it is sometimes possible to find more extensional (ie, more mathematically tractable) characterizations of various intensional features that give models like Turing machines their power. For example, one difference between Turing machines and pure lambda calculus is that since Turing receive codes of programs, a client can manually implement timeouts, to implement dovetailing -- and hence can compute parallel-or. However, timeouts can also be modelled metrically, and Escardo has conjectured (I don't know its status) that metric space models of the lambda calculus are fully abstract for PCF + timeouts. Metric spaces are very well-studied mathematical objects, and it is very nice to be able to make use of that body of theory.
However, the difficulty of using lambda calculus is that it forces you to confront higher-order phenomena right from the starting gate. This can be very subtle, since the Church-Turing thesis fails at higher type -- natural models of computation differ at higher type, since they differ in what you are permitted to do with the representations of computations. (Parallel-or is a simple example of this phenomenon, since it exhibits a difference between LC and TMs.) Moreover, there isn't even a strict inclusion between the different models, since the contravariance of the function space means that more expressive power at one order implies less expressive power one order higher.
answered Aug 30, 2010 at 6:07
$\begingroup$
$\endgroup$
As far as I know, lambda calculus is ill suited for this purpose, as the notion of time/space complexity is hard to formulate in lambda calculus.
What is 1 unit of time complexity? A beta reduction? What about the units of space complexity? The length of the string?
Lambda calculus is more suitable for abstract manipulation of algorithms, as it is much more readily composable than Turing machines.
$\begingroup$
$\endgroup$
You could also look up calculi of explicit substitutions which break up the meta-level substitution of the lambda-calculus into a series of explicit reduction steps. This touches on Charles' point that all substitutions should not be considered the same when considering time complexity.
$\begingroup$
$\endgroup$
See Nils Anders Danielsson, Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures which is implemented as a library in Agda. The citations given in the paper also look very promising.
One key takeaway for me is that it is appropriate/useful/reasonable/semi-automatable to derive the time complexity of algorithms in the simply typed lambda calculus especially if those algorithms are easily expressible in it (i.e. purely functional) and very especially if those algorithms make essential use of, e.g., call-by-name semantics. Along with this is the probably obvious point that one does not calculate complexity just "in the lambda calculus" but in the lambda calculus under a given evaluation strategy.
