Full Applicative Order Argument Evaluation

[rudynicolop]

trafficstars

It seems as if Full Applicative Order does not fully-evaluate all arguments before beta-reduction.

For instance, with the macros:

ID = λx. x
TRUE = λx. λy. x
OMEGA = λx. x x

I expected the sample program:

TRUE ID (OMEGA OMEGA)

to diverge under Full Applicative Order, as it does under Call-by-Value. However, it appears to terminate to ID, as it would under Full Normal Order and Call-by-Name.

Here is the example in lambdalab.

Is this behavior expected?

Thank you!

[sampsyo]

Huh, yeah, that is weird. Seems like this case should reduce the RHS instead of applying, if I'm not mistaken: https://github.com/cucapra/lambdalab/blob/742a730e73bfbc6f207859031310ec53d5d5c068/lib/reduce.ts#L249-L250

As the comment would imply: https://github.com/cucapra/lambdalab/blob/742a730e73bfbc6f207859031310ec53d5d5c068/lib/reduce.ts#L236-L237

Or perhaps I'm misunderstanding, @dsainati1?

[dsainati1]

Yea as far as I can tell (it's been a few years since I thought about this code) this is a bug. Nice catch!