[m-dev.] proposal: rename the modules of the first termination analyzer
Julien Fischer
jfischer at opturion.com
Sun Aug 30 16:14:03 AEST 2026
On Sun, 30 Aug 2026 at 15:57, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>
>
>
> On Sun, 30 Aug 2026 15:44:32 +1000, Julien Fischer <jfischer at opturion.com> wrote:
> > > Actually, this raises a new question. All the termination-related modules are
> > > currently part of the transform_hlds package.
> >
> > transform_or_analyse_hlds would be more accurate, but that's a bit long.
> >
> > > Should the packages be
> > > transform_hlds.term_{osi,constr}, or just term_{osi,constr}? I vote
> > > for the latter.
> >
> > The latter involves adding two separate packages, one for each analyser?
> > I would be inclined to move both of them into a termination package.
>
> What advantage do you think that arrangement has over making both
> term_{osi,constr} top level packages?
At the moment, none. If work on termination analysis were resumed, then I would
like to see both analyses (and any future ones) more integrated than
they currently
are. (For example, if both analyses are being run and the first one
proves termination,
the second one should not attempt a termination proof etc.)
(Incidentally, have you thought about where term_norm.m will end up; it's used
by things other than the termination analysers.)
Julien.
More information about the developers
mailing list