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

[ 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