Full Applicative Order Argument Evaluation

[rudynicolop]

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:

lambdalab/lib/reduce.ts

Lines 249 to 250 in 742a730

	let [expr, substs] = subst(e.e1.body.copy(), e.e2.copy(), e.e1.vbl);
	return [expr, new StepInfo(true, e.e1, e.e2, e.e1.vbl, null, substs)];

As the comment would imply:

lambdalab/lib/reduce.ts

Lines 236 to 237 in 742a730

	// As call-by-name, but with an attempt to reduce the rhs iff there
	// is nothing to reduce or subsitute on the left

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!