Re: [TYPES] What exactly should we call syntax-directed inference rules?
Julia Belyakova <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <CAJPMfOfT_ahEMtpLJe5=SrNmkajreiuHmfXfaOcECBxs_GnAWA@mail.gmail.com> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Thanks, Frank! That's exactly it. I see there are various papers on logic, proof search, analytic vs non-analytic proof systems, which use the term but do not define it. Your 1984 paper calls analytic "resolution or mating proof systems". I wonder if there is there a classic paper/book I can refer to for the definition? -- Kind regards, Julia сб, 15 июн. 2019 г. в 09:32, Frank Pfenning <[email protected]>: > 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 > >