The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Donald,


> I have not been able to come up with a property analogous to 
> `beta_step_eval_complete` for the multi-step evaluator. Are there any 
> properties other than `beta_multistep_eval_sound` above relating 
> `beta_multistep` and `beta_multistep_eval` that successfully differentiates a 
> proper implementation of `beta_multistep_eval` from the trivial 
> implementation shown above? Any ideas would be much appreciated.

The distinguishing feature of the trivial evaluator is that it doesn't 
step, so we are looking for a property to prevent that. or in other 
words, to force an evaluator to step whenever possible.

"If the term can beta reduce, then the evaluator will step at least once."

A stronger property could make the gas more relevant, while not 
requiring the evaluator to always normalize given enough fuel.

"Given fuel n, the evaluator will make n steps, or it will reach a 
normal form."


> Or is it possible to implement the evaluator in such a way that it always 
> chooses the correct reduction steps towards a beta-normal form (if exists)?

Yes! Call-by-name evaluation is a well-known solution.

If we also add the constraint that you need to find the shortest path, 
it becomes a harder, I mean, _more interesting_ problem.

Regards,
Li-yao