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

[Julia Belyakova]

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 <fp at cs.cmu.edu>:

> 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 <julbinb at gmail.com> 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
>
>