[m-users.] Determinism issue with parser

[Zoltan Somogyi]

2021-07-05 01:21 GMT+10:00 "Volker Wysk" <post at volker-wysk.de>:
> I've built a big parser for my project, too. It should always produce one
> solution; it can't fail. But the compiler can't infer that it is
> deterministic, for many parts of it. (That would be undecidable.) 
> 
> So I've resigned to this state of affairs. I just collect all the (exactly
> one) solutions with solutions/2 and produce an error message in case there
> should be more than one, which would be a bug in my parser.

That works, but I would consider it fragile. The reason is that convincing
someone (the next maintainer of the parser, perhaps) that there will be
exactly one overall solution requires a single correctness argument over
the entire code, and humans are not very reliable as reasoning machines;
the longer the argument, the higher the probability of error.

I would instead add disambiguation code to the places in the parser
than can introduce (as far as the compiler is concerned) the possibility
of nondeterminism. You can you can see why there is no such possibility;
I would try  to make the compiler that too. In most cases, this is not too hard,
at least in my experience.

This approach replaces a single bug, global correctness argument with lots of
small, local correctness arguments, which can be understood, documented,
and if need be fixed, much more easily. Modularity in correctness arguments,
if you will.

Zoltan.