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

Mon Jun 17 18:38:01 EDT 2019

Dear Fabian and Ross,

Thanks for the clarification!

Also, I wonder if the rule

     NF(t) <: t'
    -------------
       t <: t'

can be considered analytic. Strictly speaking, a normal form is not a
subformula, though the premise of the rule is completely determined by the
conclusion, which seems to be in the analytic spirit.

--
Kind regards, Julia

пн, 17 июн. 2019 г. в 17:21, Fabian Muehlboeck <fabianm at cs.cornell.edu>:

> Hi all,
> A complication is that our system neither requires nor produces
> syntax-directed or analytic systems (according to the definitions you have
> provided). Julia, from what we know of what you are working on, it is
> likely your system also satisfies neither definition. The problem is that
> the types in the premises are not necessarily subterms of the types (or
> their instances) in the conclusion, a point of flexibility that seems very
> important for achieving the kinds of expressiveness we (both) want. All we
> assume/provide is that any conclusion has a (computable) finite number of
> applicable rules (with metavariables instantiated) and that those rules
> have a (computable) finite number of premises. Importantly, not having the
> subformula property means that in general proof search is not necessarily
> terminating (even with cycle detection), so we need another property of the
> system to ensure decidability (the same goes for non-analytic
> syntax-directed systems, as TAPL notes), which we called well-foundedness.
> It would be great to have standard terms for these notions. Unfortunately,
> we could not find them ourselves, and so we generalized existing terms.
> Frank (or anyone else on the list), do you happen to know the precise terms
> that describe these two concepts that make proof search a decision
> procedure?
>
> Thanks
>
> Fabian and Ross
>
>
> -----Original Message-----
> From: Types-list <types-list-bounces at LISTS.SEAS.UPENN.EDU> On Behalf Of
> Frank Pfenning
> Sent: Monday, June 17, 2019 09:37
> To: Julia Belyakova <julbinb at gmail.com>
> Cc: Types list <types-list at lists.seas.upenn.edu>
> Subject: Re: [TYPES] What exactly should we call syntax-directed inference
> rules?
>
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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
>
>