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

[Frank Pfenning]

I am not a historian, but the classic paper I would cite is Gentzen's 1935
paper that introduced both natural deduction and the sequent calculus.
Cut-free sequent proofs have the subformula property and are therefore
analytic, although I don't think that Gentzen actually used the term.
In natural deduction, I think Prawitz 1965 was the first one to explicitly
characterizes the normal forms (which are the analytic natural deductions).

The Stanford Encyclopedia of Philosophy (*The Analytic/Synthetic
Distinction* <https://plato.stanford.edu/entries/analytic-synthetic/>)
credits Kant 1781 who defines the term and elaborates.  Martin-Löf 1994
elaborates on what this should mean in type theory in his paper
*Analytic and Synthetic Judgements in Type Theory
<https://link.springer.com/chapter/10.1007/978-94-011-0834-8_5>.*

  - Frank

On Mon, Jun 17, 2019 at 6:03 AM Julia Belyakova <julbinb at gmail.com> wrote:

> 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
>>
>>

-- 
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