1
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ 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. $\endgroup$
    – Joey Eremondi
    Sep 22, 2020 at 5:16
  • $\begingroup$ @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? $\endgroup$
    – user42215
    Sep 22, 2020 at 5:27

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.