<p>Counting <span class="math-container">$\beta$</span>-reductions is one kind of complexity measure for <span class="math-container">$\lambda$</span>-calculus, but a more flexible and reasonable one is cost semantics, where the operational semantics is augmented by various notions of cost. One good starting point are the
 <a href="https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php" rel="noreferrer">OPLSS 2018</a> lectures on cost semantics by Jan Hoffmann (videos and lecture materials available at the link).</p>

CC BY-SA 4.0
2018-10-23T21:03:11.617Z
2018-10-23T21:03:11.617Z
Andrej Bauer
<p>A note about space complexity.  While, as pointed out by Martin in his answer, the naive way to count time complexity turns out to work well, the definition of space complexity you suggest is easily seen to be inadequate.  Indeed, in the case of space you really want to be able to speak of sublinear complexity, e.g. you want to be able to recover the class <span class="math-container">$\mathsf L$</span> (deterministic logspace, which is to space a bit what <span class="math-container">$\mathsf P$</span> is to time), and your definition obviously does not allow you to do that: in any reduction <span class="math-container">$M\to^\ast N$</span>, your are counting <em>at least</em> the size of <span class="math-container">$M$</span>, which is linear in the input size.</p>

<p>The moral of the story is that rewriting is not suitable for counting space.  Ulrich Schöpp and Ugo Dal Lago were the first to advocate the use of the so-called <em>geometry of interaction</em> (GoI) for dealing with sublinear space complexity (cf. their ESOP 2010 paper "Functional Programming in Sublinear Space").  As far as I know, the GoI is used in one way or another in all lambda-calculus-based characterizations of sublinear space classes.  I do not want to get into what the GoI is here; let's say that it is a way of executing a lambda-term without reducing it (i.e., without firing <span class="math-container">$\beta$</span>-redexes) but by "traveling" through its syntactic tree with a certain auxiliary information.</p>

CC BY-SA 4.0
2018-10-25T06:57:11.050Z
2018-10-25T06:57:11.050Z
Damiano Mazza
<p>As you point out, the λ-calculus has a seemingly simple notion of time-complexity: just count the number of β-reduction steps. Unfortunately, things are not simple. We should ask: </p>

<pre><code> Is counting β-reduction steps a good complexity measure?
</code></pre>

<p>To answer this question, we should clarify what we mean by complexity measure in the first place. One good answer is given by the <em>Slot and van Emde Boas thesis</em>: any good complexity measure should have a polynomial relationship to the canonical notion of time-complexity defined using Turing machines. In other words, there should be a reasonable encoding tr(.) from λ-calculus terms to Turing machines, such that for each term <span class="math-container">$M$</span> of size <span class="math-container">$|M|$</span>: <span class="math-container">$M$</span> reduces to a value in <span class="math-container">$poly(|M|)$</span> exactly when <span class="math-container">$tr(M)$</span> reduces to a value in <span class="math-container">$poly(|tr(M)|)$</span>.</p>

<p>For a long time, it was unclear if this can be achieved in the λ-calculus. The main problems are the following.</p>

<ul>
<li><p>There are terms that produce normal forms in a polynomial number of
steps that are of exponential size. See (1). Even writing down the
normal forms takes exponential time. </p></li>
<li><p>The chosen reduction strategy
plays an important role, too. For example there exists a family of terms
which reduces in a polynomial number of parallel β-steps (in the
sense of optimal λ-reduction (2), but whose complexity is
non-elementary (3, 4). </p></li>
</ul>

<p>The paper (1) clarifies the issue by showing a reasonable encoding that preserves the complexity class <strong>PTIME</strong> assuming leftmost-outermost Call-By-Name reductions. The key insight appears to be that the exponential blow-up can only happen for uninteresting reasons which can be defeated by proper sharing of sub-terms.</p>

<p>Note that papers like (1) show that coarse complexity classes like <strong>PTIME</strong> coincide, whether you count β-steps, or Turing-machine steps. That does not mean lower complexity classes like <strong>O(log n)</strong> also coincide. Of course such complexity classes are also not stable under variation of Turing machine model (e.g. 1-tape vs multi-tape).</p>

<p>D. Mazza's work (5) proves the Cook-Levin theorem (-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. The key insight is this:</p>

<p><span class="math-container">$$
  \frac{\text{Boolean
circuits}}{\text{Turing machines}}=\frac{\text{affine
  $\lambda$-terms}}{\text{$\lambda$-terms}}
  $$</span></p>

<p>I don't know if the situation regarding space complexity is understood.</p>

<hr>

<ol>
<li><p>B. Accattoli, U. Dal Lago, <a href="https://arxiv.org/abs/1405.3311" rel="noreferrer">Beta Reduction is Invariant, Indeed</a>.</p></li>
<li><p>J.-J. Levy, Reductions correctes et optimales dans le lambda-calcul.</p></li>
<li><p>J. L. Lawall, H. G. Mairson, <a href="https://dl.acm.org/citation.cfm?id=232639" rel="noreferrer">Optimality and inefficiency: what isn't
a cost model of the lambda calculus</a>? </p></li>
<li><p>A. Asperti, H. Mairson,
<a href="https://www.sciencedirect.com/science/article/pii/S089054010192869X" rel="noreferrer">Parallel beta reduction is not elementary recursive</a>.</p></li>
<li><p>D. Mazza, <a href="https://www-lipn.univ-paris13.fr/~mazza/papers/ChurchCookLevin.pdf" rel="noreferrer">Church Meets Cook and Levin</a>.</p></li>
</ol>

CC BY-SA 4.0
2018-10-23T11:54:10.050Z
2018-10-23T13:23:33.743Z
2018-10-23T13:23:33.743Z
Martin Berger
<p>In complexity theory the definition of time and space complexity both reference a universal Turing machine: resp. the number of steps before halting, and the number of cells on the tape touched.</p>

<p>Given the Church-Turing thesis, it should be possible to define complexity in terms of lambda calculus as well.</p>

<p>My intuitive notion is that time complexity can be expressed as the number of β-reductions (we can define away α-conversion by using De Brujin indexes, and η is barely a reduction anyway), while space complexity can be defined as the number of symbols (λ's, DB-indexes, “apply”-symbols) in the <em>largest</em> reduction.</p>

<p>Is this correct? If so, where can I get a reference? If not, how am I mistaken?</p>

CC BY-SA 4.0
2018-10-27T08:29:13.760Z
This sounds like [implicit computational complexity](https://en.wikipedia.org/wiki/Implicit_computational_complexity)?
Ta Thanh Dinh
<time-complexity><lambda-calculus>
Equivalent formulation of complexity theory in Lambda Calculus?
Kile Kasmir Asmussen
# Equivalent formulation of complexity theory in Lambda Calculus?

(Asked by: username_0 on 2018-10-23)

In complexity theory the definition of time and space complexity both reference a universal Turing machine: resp. the number of steps before halting, and the number of cells on the tape touched.

Given the Church-Turing thesis, it should be possible to define complexity in terms of lambda calculus as well.

My intuitive notion is that time complexity can be expressed as the number of β-reductions (we can define away α-conversion by using De Brujin indexes, and η is barely a reduction anyway), while space complexity can be defined as the number of symbols (λ's, DB-indexes, “apply”-symbols) in the *largest* reduction.

Is this correct? If so, where can I get a reference? If not, how am I mistaken?

**Tags:** time-complexity, lambda-calculus
> **Comments:**
> **username_1**: This sounds like [implicit computational complexity](https://en.wikipedia.org/wiki/Implicit_computational_complexity)?  

---

## 3 answers

### Answer by username_4 on 2018-10-23. Score: 17 | Accepted answer

As you point out, the λ-calculus has a seemingly simple notion of time-complexity: just count the number of β-reduction steps. Unfortunately, things are not simple. We should ask: 
 Is counting β-reduction steps a good complexity measure?

To answer this question, we should clarify what we mean by complexity measure in the first place. One good answer is given by the Slot and van Emde Boas thesis: any good complexity measure should have a polynomial relationship to the canonical notion of time-complexity defined using Turing machines. In other words, there should be a reasonable encoding tr(.) from λ-calculus terms to Turing machines, such that for each term $M$ of size $|M|$: $M$ reduces to a value in $poly(|M|)$ exactly when $tr(M)$ reduces to a value in $poly(|tr(M)|)$.
For a long time, it was unclear if this can be achieved in the λ-calculus. The main problems are the following.

There are terms that produce normal forms in a polynomial number of
steps that are of exponential size. See (1). Even writing down the
normal forms takes exponential time. 
The chosen reduction strategy
plays an important role, too. For example there exists a family of terms
which reduces in a polynomial number of parallel β-steps (in the
sense of optimal λ-reduction (2), but whose complexity is
non-elementary (3, 4). 

The paper (1) clarifies the issue by showing a reasonable encoding that preserves the complexity class PTIME assuming leftmost-outermost Call-By-Name reductions. The key insight appears to be that the exponential blow-up can only happen for uninteresting reasons which can be defeated by proper sharing of sub-terms.
Note that papers like (1) show that coarse complexity classes like PTIME coincide, whether you count β-steps, or Turing-machine steps. That does not mean lower complexity classes like O(log n) also coincide. Of course such complexity classes are also not stable under variation of Turing machine model (e.g. 1-tape vs multi-tape).
D. Mazza's work (5) proves the Cook-Levin theorem (-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. The key insight is this:
$$
  \frac{\text{Boolean
circuits}}{\text{Turing machines}}=\frac{\text{affine
  $\lambda$-terms}}{\text{$\lambda$-terms}}
  $$
I don't know if the situation regarding space complexity is understood.


B. Accattoli, U. Dal Lago, Beta Reduction is Invariant, Indeed.
J.-J. Levy, Reductions correctes et optimales dans le lambda-calcul.
J. L. Lawall, H. G. Mairson, Optimality and inefficiency: what isn't
a cost model of the lambda calculus? 
A. Asperti, H. Mairson,
Parallel beta reduction is not elementary recursive.
D. Mazza, Church Meets Cook and Levin.


---

### Answer by username_2 on 2018-10-23. Score: 10

Counting $\beta$-reductions is one kind of complexity measure for $\lambda$-calculus, but a more flexible and reasonable one is cost semantics, where the operational semantics is augmented by various notions of cost. One good starting point are the
[OPLSS 2018](https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php) lectures on cost semantics by Jan Hoffmann (videos and lecture materials available at the link).


---

### Answer by username_3 on 2018-10-25. Score: 5

A note about space complexity. While, as pointed out by Martin in his answer, the naive way to count time complexity turns out to work well, the definition of space complexity you suggest is easily seen to be inadequate. Indeed, in the case of space you really want to be able to speak of sublinear complexity, e.g. you want to be able to recover the class $\mathsf L$ (deterministic logspace, which is to space a bit what $\mathsf P$ is to time), and your definition obviously does not allow you to do that: in any reduction $M\to^\ast N$, your are counting *at least* the size of $M$, which is linear in the input size.

The moral of the story is that rewriting is not suitable for counting space. Ulrich Schöpp and Ugo Dal Lago were the first to advocate the use of the so-called *geometry of interaction* (GoI) for dealing with sublinear space complexity (cf. their ESOP 2010 paper "Functional Programming in Sublinear Space"). As far as I know, the GoI is used in one way or another in all lambda-calculus-based characterizations of sublinear space classes. I do not want to get into what the GoI is here; let's say that it is a way of executing a lambda-term without reducing it (i.e., without firing $\beta$-redexes) but by "traveling" through its syntactic tree with a certain auxiliary information.


---

