[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
In the proof theory tradition, rules like those you quote for unions are called *analytic*. It means not only that there are a finite number of possibilities, but they are composed of subformulas of the conclusion. So, like Pierce, I would tend to reserve *syntax-directed* for the stronger property that the rule selection is determined unambiguously by the syntax, since we already have a perfectly good term for the weaker property. - Frank On Fri, Jun 14, 2019 at 7:16 PM Julia Belyakova <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > 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 > -- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 http://www.cs.cmu.edu/~fp +1 412 268-6343 GHC 6017
