Comparing algorithms (L) and (L+)
There is a sense in which algorithm (L) preserves the structure or shape of the input term when it abstracts a variable from it. This is very useful if you are interested in multi-variate abstraction. Although algorithm (L+) does not have this property, it usually produces shorter abstracts than (L). It is, therefore, more suited to uni-variate abstraction.
Try some examples yourself to see how these two algorithms compare.
© Antoni Diller (28 May 2013)