The Maximum Length of Mu-Reduction in Lambda Mu-Calculus

摘要

This paper gives the exact number of the maximum length of mu-reduction and permutative conversions for an untyped term in lambda mu-calculus with disjunction. This number is described by using induction on the number of symbols in a term. It is also shown that leftmost short reduction and innermost null reduction produce the longest reduction sequence.