The lambda-calculus rule (lambda (x) (g x)) <=> g (where g has exactly 1 argument [the only case in the pure lambda calculus]) is called 'axiom eta', and is independent of axiom alpha (variable renaming) and axiom beta (function application through variable binding).
Your 'B)' does both eta & beta, while 'A)' does just substitution
At 01:24 PM 6/12/2013, Stavros Macrakis wrote:
>Robert,
>
>I think the two possible behaviors are:
>
>A) subst( lambda([x],g(x)), 'f , f(q) ) => lambda([x],g(x))(q)
>
>B) subst( lambda([x],g(x)), 'f , f(q) ) => g(q)
>
>(B) is the current behavior. It seems wrong in principle, because the transformation lambda([x],g(x))(q) => g(q) is performed by evaluation, not by simplification; that is, '(lambda([x],g(x))(q)) does not simplify to g(q).
>
>Another example of how (B) is inconsistent with other cases of subst:
>
> subst( print , 'f , f(23) ) => print(23) <<< does not print because it does not eval
> subst( lambda([x],print(x)), 'f, f(23) ) => 23 <<< prints and returns 23 because it does eval
>
>However, (B) is a handy idiom, which Barton in particular is very fond of....
>
> -s
>
>On Wed, Jun 12, 2013 at 3:14 PM, Robert Dodier <robert.dodier at gmail.com> wrote:
>On Wed, Jun 12, 2013 at 12:07 PM, Barton Willis <willisb at unk.edu> wrote:
>
>> If the substitute a lambda form for a function idiom stops working
>> as I want it to, that's OK. I'll just write my own substitute :)
>
>How do you want it to work?
>
>For what it's worth, there isn't any proposal to disallow such a
>substitution -- only that simplification of the result
>should not evaluate the lambda expression. So presumably
>evaluating the result should give the same result as one gets
>from subst(lambda ...) now.
>
>best
>
>Robert Dodier