[TYPES] What exactly should we call syntax-directed inference rules?

[Julia Belyakova]

Dear All,

It seems that there is a slight inconsistency in what kind of inference
rules are called "syntax-directed". Let's take subtyping rules as an
example.

(a) In TAPL, syntax-directed means that for each pair of types T and S,
there is exactly one rule with the conclusion that matches T <: S.
(b) In some papers, e.g. [1], rules are considered syntax-directed if for
each pair T and S there is a finite number of rules matching T <: S and
each of them has a finite number of (computable) premises.

The transitivity rule

    T1 <: T2  T2 <: T3
  ----------------------
         T1 <: T3

is clearly bad, and it is rejected by both definitions:
(a) The conclusion T1 <: T3 overlaps with any other subtyping rule.
(b) It is not clear how to compute T2 and there can be infinitely many of
them.

But what about subtyping of union types?

    T <: S1                  T <: S2
  ------------- UnionR1    ------------ UnionR2
   T <: S1∪S2               T <: S1∪S2

According to (a), such rules are not syntax-directed. According to (b),
they are.

The UnionR* rules are definitely worse than syntax-directed rules in the
sense of (a) because for a triple of types T, S1, S2 we have two options,
and one of them might work while the other does not. Algorithmically, this
is the source of backtracking.
However, these rules are better than the transitivity rule because their
premises are uniquely defined by syntax.

Which terminology is more generally accepted, (a) or (b)? And is there a
suitable terminology to distinguish between (a), rules like UnionR*, and
rules like transitivity?

[1] Fabian Muehlboeck and Ross Tate. 2018. Empowering union and
intersection types with integrated subtyping. Proc. ACM Program. Lang. 2,
OOPSLA, Article 112 (October 2018), 29 pages. DOI:
https://doi.org/10.1145/3276482

--
Kind regards, Julia