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

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

<p><a href="http://arxiv.org/abs/1405.3311" rel="noreferrer">http://arxiv.org/abs/1405.3311</a></p>

CC BY-SA 3.0
2015-12-24T13:37:34.677Z
2017-01-05T03:07:13.337Z
2017-01-05T03:07:13.337Z
Marc
<p>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, <em>Journal of Symbolic Logic</em> 2001, 66(3): 1277-1285.</p>

<p>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 <a href="http://raml.tcs.ifi.lmu.de/">here</a>.</p>

<p>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 <em>Proceedings of the 19th European Symposium on Programming</em> (ESOP'10).<a href="http://www2.tcs.ifi.lmu.de/~hoffmann/papers/aapoly_extended.pdf">link</a></p>

CC BY-SA 2.5
2010-08-21T22:48:40.560Z
2010-08-21T22:48:40.560Z
Iddo Tzameret
<p>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. </p>

<p>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 <em>very</em> well-studied mathematical objects, and it is very nice to be able to make use of that body of theory.</p>

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

CC BY-SA 2.5
2010-08-30T06:07:04.693Z
2010-08-30T06:07:04.693Z
Neel Krishnaswami
<p>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. </p>

<p>What is 1 unit of time complexity? A beta reduction? What about the units of space complexity? The length of the string?</p>

<p>Lambda calculus is more suitable for abstract manipulation of algorithms, as it is much more readily composable than Turing machines.</p>

CC BY-SA 2.5
2010-08-21T21:44:38.303Z
2010-08-21T21:44:38.303Z
Ohad Kammar
<p>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.</p>

CC BY-SA 2.5
2010-08-23T20:39:02.540Z
2010-08-23T20:39:02.540Z
Dominic Mulligan
<p>See Nils Anders Danielsson, <a href="http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.html" rel="noreferrer">Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures</a> which is implemented as a library in Agda. The citations given in the paper also look very promising.</p>

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

CC BY-SA 2.5
2010-08-27T14:07:30.517Z
2010-08-27T14:07:30.517Z
sclv
<p>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.</p>

<p>Two links:</p>

<ol>
<li>Lawall &amp; Mairson, 1996, <a href="http://www.diku.dk/hjemmesider/ansatte/julia/icfp96.ps.gz">Optimality and inefficiency: what isn't a cost model of the lambda calculus? (.ps.gz)</a> – Seminal survey of issues bearing on choice of cost model, and why many plausible ideas don't work.</li>
<li>Dal Lago &amp; Martini, 2008, <a href="https://www.di.unito.it/~deligu/CDR60_TCS/Martini.pdf">The weak lambda calculus as a reasonable machine</a> – Offers a cost model for the call-by-value lambda calculus, together with good discussion of the literature.</li>
</ol>

CC BY-SA 3.0
2015-12-26T15:53:51.910Z
The situation has changed recently on this topic. See my answer below.
Marc
CC BY-SA 2.5
2010-08-22T21:21:32.500Z
Interesting references, I didn't know about these works.
Iddo Tzameret
CC BY-SA 3.0
2010-08-22T21:10:03.883Z
2016-05-31T11:03:31.497Z
2016-05-31T11:03:31.497Z
Charles Stewart
<p>Are there any benefits to calculating the time complexity of an algorithm using lambda calculus?  Or is there another system designed for this purpose?</p>

<p>Any references would be appreciated.</p>

<lambda-calculus><pl.programming-languages><time-complexity>
Using lambda calculus to derive time complexity?
Shane
# Using lambda calculus to derive time complexity?

(Asked by: username_0 on 2010-08-21)

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.

**Tags:** lambda-calculus, pl.programming-languages, time-complexity

---

## 7 answers

### Answer by username_7 on 2010-08-22. Score: 21 | Accepted answer

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:

1. Lawall & Mairson, 1996, [Optimality and inefficiency: what isn't a cost model of the lambda calculus? (.ps.gz)](http://www.diku.dk/hjemmesider/ansatte/julia/icfp96.ps.gz) – Seminal survey of issues bearing on choice of cost model, and why many plausible ideas don't work.
2. Dal Lago & Martini, 2008, [The weak lambda calculus as a reasonable machine](https://www.di.unito.it/~deligu/CDR60_TCS/Martini.pdf) – Offers a cost model for the call-by-value lambda calculus, together with good discussion of the literature.

> **Comments:**
> **username_2**: Interesting references, I didn't know about these works.  
> **username_1**: The situation has changed recently on this topic. See my answer below.  

---

### Answer by username_1 on 2015-12-24. Score: 23

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.

<http://arxiv.org/abs/1405.3311>


---

### Answer by username_2 on 2010-08-21. Score: 22

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](http://raml.tcs.ifi.lmu.de/).

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](http://www2.tcs.ifi.lmu.de/~hoffmann/papers/aapoly_extended.pdf)


---

### Answer by username_3 on 2010-08-30. Score: 18

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.


---

### Answer by username_4 on 2010-08-21. Score: 12

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.


---

### Answer by username_5 on 2010-08-23. Score: 7

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.


---

### Answer by username_6 on 2010-08-27. Score: 7

See Nils Anders Danielsson, [Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures](http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.html) 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.


---

