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.
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.
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.
I checked simple cases and they were linear. But I feel hard to find the pathological cases. Can someone give me some examples?