[ 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 <[email protected]> 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 <[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 >> >> -- 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
