<p>I'm studying the substitution algorithms of lambda calculus. I think now I understand how they work, but I couldn't find any materials about their time complexity yet.</p>
<p>This is what I've thought about each algorithm so far.</p>
<ol>
<li><p>dumb substitution(Just recursively finding variables to substitute)</p>
<p>I think it's O((avg of the number of terms in each abstraction) * (maximum abstraction level) ^ 2) in pathological cases.</p>
</li>
<li><p>normalization by evaluation</p>
<p>I think it's O(the number of terms), which is linear. But I'm not sure that it really is with consideration of operations in the host language. In my thoughts, the host language needs to manage context for each abstraction and this task might not be free.</p>
</li>
<li><p>explicit substitution.</p>
<p>I checked simple cases and they were linear. But I feel hard to find the pathological cases. Can someone give me some examples?</p>
</li>
</ol>

CC BY-SA 4.0
2020-09-22T05:16:48.347Z
I think NBE might be beyond any complexity class. You can evaluate any MLTT term with NBE, including applications of the Ackerman function, so you're already beyond primitive recursion.
Joey Eremondi
CC BY-SA 4.0
2020-09-22T05:27:54.123Z
@jmite Thank you for pointing that out. I forgot there are total recursive functions. If I edit my question to no regarding recursive functions, then will this question be valid?
user42215
<lambda-calculus><functional-programming>
What is the time complexity of substitution algorithms(normalization by evaluation, explicit subtitution)?
user42215
# What is the time complexity of substitution algorithms(normalization by evaluation, explicit subtitution)?

(Asked by: username_0 on 2020-09-21)

I'm studying the substitution algorithms of lambda calculus. I think now I understand how they work, but I couldn't find any materials about their time complexity yet.

This is what I've thought about each algorithm so far.

1. dumb substitution(Just recursively finding variables to substitute)

   I think it's O((avg of the number of terms in each abstraction) \* (maximum abstraction level) ^ 2) in pathological cases.
2. normalization by evaluation

   I think it's O(the number of terms), which is linear. But I'm not sure that it really is with consideration of operations in the host language. In my thoughts, the host language needs to manage context for each abstraction and this task might not be free.
3. explicit substitution.

   I checked simple cases and they were linear. But I feel hard to find the pathological cases. Can someone give me some examples?

**Tags:** lambda-calculus, functional-programming
> **Comments:**
> **username_1**: I think NBE might be beyond any complexity class. You can evaluate any MLTT term with NBE, including applications of the Ackerman function, so you're already beyond primitive recursion.  
> **username_0**: @jmite Thank you for pointing that out. I forgot there are total recursive functions. If I edit my question to no regarding recursive functions, then will this question be valid?  

---

## 0 answers

