User guide
Contents
1. _ ta DCL 1 O Ce RA ae a i b lt p DCL 2 0 10 Cry SS TE ee cee a e 3 4 DCL 3 2 ie M TR TA a Gig a d e draw drv_tree d endfig MVD The MVD macro is a generalization of Mvd that enables the specification of the alignment style of phantom inferences MVD nat 1 nat 2 str 1 str2 id 1 id 2 nat 1 index of the origin judgment nat 2 number of phantom steps str 1 left label math mode 14TFX code str 2 right label math mode ATEX code id 1 alignment style identifier 1 c or r id 2 phantom steps path style identifier 0 1 2 3 4 5 6 or _ beginfig 450 jgm 0 a jgm 1 b eeeeeeeee jgm 2 cccccc jgm 3 ddd jgm 4 eeeeeeeee nfr 0 1 MVD 4 5 F r 4 C _ Gi o nfr 1 MVD 2 2 G 1 3 3 C _ ddd nir 2 0 Ey b nfr 300 nfr 4 _ draw drv_tree endfig CCCCCC 22 Low LEVEL INFERENCE DECLARATION MACROS beginfig 460 jgm 0 textsc Size matters Part 2 jgm 1 text Here is an even longer judgment amp that I don t want to shorten either jgm 2 text This time I m pretty sure that the amp derivation tree won t fit on the page jgm 3 text It does Amazing nfr 0 O C 0 nfr 1 c 1 nftr200C0 1 nfr 3 MVD 1 G 0 ma Ty 30 D Ca a draw drv_tree endfig SIZE MATTERS PART 2 Here is an even longer judgment that I don t want to shorten either This t2. resp typeset as a a a resp resp 2 3 bxd and mvd 9 mvd A premise index nat 1 in an inference declaration can be replaced with mvd nat 1 nat 2 id so as to declare nat 2 phantom inference steps starting from the index nat 1 judgment The phantom inference steps are in tended to be drawn as a path using the path style id mvd nat 1 nat 2 id nat 1 index of the origin judgment nat 2 number of phantom steps id phantom steps path style identifier 0 1 2 3 4 5 6 or _ beginfig 170 aaa jgm 1 aaa jgm 2 bbb bbb e jgm 3 ccc jgm 4 d d nfr1Q _ bbb nfr 2 0 _ nfr 300 y nfr 4 mvd 1 2 3 2 3 C _ 3 ada ccc nfr 4 1 mvd 2 2 4 3 C _ 3 d nfr 4 1 2 mvd 3 2 6 C D draw drv_tree cec endfig aaa bbb d beginfig 180 jgm 0 textsc Size matters Part 1 jgm 1 text Here is a rather long judgment amp string concatenation that I don t want to shorten jgm 2 text Will the derivation tree fit on the page jgm 3 text It does nfr 0 O C 0 nfr 1 0 C 1 nfr20C0 1 nfr 3 mvd 1 2 3 2 C 1 draw drv_tree endfig SIZE MATTERS Part Here is a rather long judgment that I don t want to shorten Will the derivation tree fit on the page It does 10 JUDGMENT AND INFERENCE DECLARATIONS 2 4 Sub tree
3. endfig pair in a file jobname mp METAPOST generates an Encapsulated PostScript file jobname index In ad dition drv generates a TEX file jobname proof tex that contains a copy of the IATEX preamble in jobname mp and includes each jobname index pic ture file using the drv inclusion command together with some information about its text size math style and math axis As an example regarding the first figure on page 5 processing drv guide proof tex produces drv guide 110 normalsize displaystyle AFB Bre AFC B Derivation forests You may declare several derivation trees within a single figure environment Then trees are drawn from left to right in the order their roots are declared and in such a way that root judgments are horizontally aligned the distance between two trees is the same as the distance between two non interleaving premises and thus is affected by drv_scale see 3 3 beginfig 530 first tree a dcl 10 O Ces _ as b C second tree a d dcl 20 21 22 c _ d del 21 C _ b del 22 O C e s draw drv_tree endfig You can however state constraints horizontal or vertical at your option specifying the relative positioning of trees before drv_freeze is called 2To METAPOST users proof file generation does not take outputtemplate into account yet resp 30 DERIVATION FORESTS beginfig 531 first tree dcl 10 O Cc _ malts second tree a
4. 0 clr ilb Pc drv_junction_style joined drv_junction_style id id junction style identifier 0 1 or 2 fully interlacing 1 semi interlacing 2 non interlacing 0 aaaaaaaaaaaa a a aaaaaa a a a aaaaaa 13 245 4 a a a a 225 4 a a a a a a 2 5 4 a a a a a a Za 4 bb b b a a a a b b a a are horizontally 2 aaaaaaaaaaaa a a aaaaaa a a aaaaaa a x default x 1 aaaaaaaaaaaa a a aaaaaa a a aaaaaa a a 14 DRV TUNINGS 3 5 drv_alignment_style This macro sets the default way a judgment is horizontally aligned relatively to its premises drv_alignment_style id id alignment style identifier 1 c or r 1 left c centered x default x r right 1 c r aaa a aaaa aaa a a a a a a a a a a 3 6 drv_path_style drv_path_style idl id 2 id I path type identifier iln or phm iln inference lines x default style 1 x phm phantom steps paths default style 3 x id 2 path style identifier 0 1 2 3 4 5 or 6 3 7 drv_labels_position drv_labels_position id 1 id 2y id 1 label type identifier ilb p1b or d1b ilb inference labels x default position r dlb delimiter labels x default position 1 plb phantom steps labels default position 1 x id 2 position identifier 1 or r 1 left r right 4198 drv_labels_position ilb 1 r 3 8 drv_roots_p
5. 015 2g TEM DIES draw drv_tree endfig 11 Mvd The Mvd macro is an alternative for mvd that enables the attachment of labels to phantom steps paths Mvd nat 1 nat 2 str 1 str 2 idy nat 1 index of the origin judgment nat 2 number of phantom steps str 1 left label math mode J4TEX code str 2 right label math mode IATEX code id phantom steps path style identifier 0 1 2 3 4 5 6 or _ If str 1 is anon empty string then it is attached as a label to the left of the phantom steps path The same way if str 2 is a non empty string then it is attached as a label to the right of the phantom steps path Both str and str 2 may be non empty strings beginfig 210 jgm 1 aaa jgm 2 bbb aaa jgm 3 ccc nfr 10 _ ay nfr2Q CT _ nfr 3 vd 1 2 a 3 D CO SD cE draw drv_tree endfig 3 drv tunings drv tuning macros set the parameters according to which derivation trees are type set You have to call these macros outside figure environments delimited by beginfig index endfig pairs 3 1 drv_font_size tiny drv_font_size str ez t BTEX font size command E small scriptsize 4 a p footnotesize Be small l Large normalsize default x i 5 oo 4 a b Large 3 etc C 12 3 2 drv_math_style drv_math_style Cid stry DRV TUNINGS id component identifier drv jdg ilb dlb or plb drv derivatio
6. 1 B vdash D dcl 23 g 3 Blvdash C dcl 24 C h 4 C vdash D drv_root 20 t root at top overlapping jdg 10 c jdg 20 c draw drv_tree endfig The resulting figure is in Appendix D on page 34 C Radial mode beta version A few more tuning macros see 3 are available that enable the manipulation of radial trees rather than linear ones drv_radial_mode drv_radial_mode id id status identifier on or off on off x default on off Bree a ed vp KB A AEB BD AD e AFD IT Ar D LB ae AFB BED Cr ret f ae CD 32 RADIAL MODE BETA VERSION drv_scale crv drv_scale crv float crv scale identifier floaty scale value x default 1 x 0 5 1 2 4 o ee O AFC drv_azimuth drv_azimuth float float azimuth degree x default 90 x 120 90 60 B Y resid 5 e LR gt e Gre gt The azimuth of a derivation tree is that of the central point of its root judgment Notice that both drv_scale crv and drv_azimuth are irrelevant when not in radial mode User specified junction and alignment styles tricky When in radial mode drv composes derivation trees by stating angular constraints rather than horizontal ones To this end three distinguished angles are associated resp resp 33 with each component cpn namely cpn 1ng cpn cng and cpn rng that refer to the relative angles of cpn 1 cpn c and cpn r respectiv
7. endfig 6 3 User specified junction and alignment styles tricky drv composes derivation trees by stating geometrical constraints to be solved by METAPOST These constraints express how the components of a derivation tree must be arranged with respect to each other In the example about dimensions see above such a constraint could be that the vertical distance from iln 1 c to jdg 0 c has to be num_hg which could be stated in the METAPOST syntax as ypart jdg 0 c ypart iln 1 c num_hg this is not an affectation You can prevent drv from stating horizontal constraints about premises junc tion or judgments alignment by using the junction style 3 or the alignment style u resp resp 6 3 User specified junction and alignment styles tricky 27 of the NFR and NFR_opt macros see 5 1 5 2 In such cases you have to state your own constraints All the constraints related to a derivation tree must be stated before drv_freeze is called METAPOST will complain if the constraints you state are insufficient redundant or inconsistent User specified junction style The horizontal constraints you state should express how the premises of the inference have to be joined beginfig 500 jgm 0 cdot jgm 1 cdot jgm 2 text You may check that the distance amp between the two dots above is 5 cm NFR 0 O Eres iain aa Da Ja NFR 1 O Cy a aa Sra y NFR 2 0 1 1 0 0 3 _ J cau
8. a a canada Rw i 3 13 drv proof mole ss cer s Qe alow de kee os ee a Re a 3 14 drv_labels_mode 0 000 eee enue 3 13 dry verbatimtex o oia OS wo 34 oa oS A eo 4 Pictures bounding boxes and math axis 4 1 drv_freezeanddrv_tree 4a o ccs sees a he Bai ct wh a cee ote eb kts we he Rete we et AO EV IRS dle gud ee a era aaa das aaa aid 5 Low level inference declaration macros 5 1 NFR DCL and MVD aco ee ee ee ee a 22 Optional labels a eds ee Qe rt Shae ee e 5 3 User defined declaration macros tricky 6 Inside derivation trees 6 1 Components distinguished points and dimensions 6 2 dry Styled eiii a da dd PO Ge Oaa 6 3 User specified junction and alignment styles tricky References A Debugging and proofing B Derivation forests C Radial mode beta version D Gallery 11 11 12 12 13 14 14 14 15 15 15 16 17 17 18 18 18 18 19 19 20 20 22 23 24 24 26 26 27 28 29 31 33 E Standalone picture files 35 F Related packages 36 1 Usage 1 1 Structure of a METAPOST file using drv Preamble input drv verbatimtex 6 latex BIFX preamble begin document etex Figures optional drv tunings beginfig index judgment and inference declarations draw drv_tree optional extra METAPOST code endfig Postamble end For each beginfig index endfig pair in a file jobname mp META POST generates
9. an Encapsulated PostScript file jobname index 1 2 Running METAPOST You have to run at least twice mpost jobname mp once more if you use sub tree delimiters see 2 4 On the first run METAPOST collects the ATEX code generated by drv declaration macros and writes it to the file jobname delayed mp On the second run METAPOST preprocesses the IEX code in jobname delayed mp and then typesets the derivation trees If you get an error on the first run then it comes from the drv METAPOST code If you get an error on the second run then it comes from the LATEX code In both cases correct the error see Appendix A delete jobname delayed mp and run mpost jobname mp twice again a makefile can do that for you 4 JUDGMENT AND INFERENCE DECLARATIONS 1 3 BXIEX inclusion commands Encapsulated PostScript files jobname index generated by METAPOST can be included in XIX documents using the includegraphics jobname index command from the graphicx sty or graphics sty package However drv provides ways to set the baseline of derivation tree pictures see 3 9 and 4 3 Then I suggest using the following drv jobname index command which is such that the baseline of the included picture coincides with the baseline of the inclusion point usepackage graphicx makeatletter def Gin de f bp 1 relax 2 3 gdef 2 3 newsavebox graphicsbox newcommand drv 1 sbox graphicsbox includ
10. be dcl 20 21 22 C _ d d d l 21 0O C7 p del 22 O Cr a e 3 Lei relative positionning b c ypart jdg 10 c ypart jdg 22 c ad xpart iln 10 r xpart iln 20 1 draw drv_tree endfig Notice that the math axis of a forest is set according to drv_axis_reference see 3 9 relatively to the first declared root you can override this behaviour by using drv_axis see 4 3 drv_root drv_root locally overrides drv_roots_position see 3 8 enabling the ex plicit setting of the position of a root drv_root nat id nat root index id position identifier t or b t top b bottom beginfig 533 first tree dcl 10 O Cs a ne second tree a d dcl 20 21 22 h _ d bec del 21 0 Ct 3 vr gt del 22 0 0 e drv_root 20 t root at top draw drv_tree endfig Then again you can state constraints specifying the relative positioning e g the overlapping of trees before drv_freeze is called drv_left_delimiter downarrow drv_right_delimiter uparrow 31 beginfig 540 first tree jgm 10 A vdash D Nfr 10 11 14 C circ hcirc g cire f 1 dcl 11 12 13 C circ 1 A vdash C dcl 12 C 2 A vdash B dcl 13 C g 3 B vdash C dcl 14 C h 4 C vdash D second tree jgm 20 phantom A vdash D hidden judgment Nfr 20 21 22 C circ Ch cire g circ f 1 dcl 21 C E 2 A vdash B dcl 22 23 24 C circ
11. delimiters and labels Nfr The Nfr declaration macro is an alternative for nfr that enables the typeset ting of delimiters Nfr nat nat list Cstrl str2 str 3 idy nat inference index nat list list of premise indices str 1 inference label math mode IFEX code str 2 left delimiter label math mode 1I pX code str 3 right delimiter label math mode IATEX code id inference line style identifier 0 1 2 3 4 5 6 or _ If both str 2 and str 3 are the empty string then Nfr behaves exactly the same way as nfr However if str 2 is a non empty string then a delimiter is placed to the left of the sub tree ending with the index nat judgment and str 2 is attached to it as a label The same way if str 3 is a non empty string then a delimiter is placed to the right of the sub tree ending with the index nat judgment and str 3 is attached to it as a label Both str 2 and str 3 may be non empty strings You may use as a string argument to get a delimiter without a label beginfig 190 jgm 0 a jgm 1 b Hf a jgm 2 e 2 F jgm 3 d 3 Nfr 0 O CO _ d Nfr1Q c 1 2 Nfr 2 0 1 M2 E _ Nfr 3 2 03 F _ draw drv_tree endfig Dcl The Dcl declaration macro is a shorthand for jgm and Nfr in the same way as dcl is a shorthand for jgm and nfr beginfig 200 Del 0070 Ja a Del 1 0 C y y B e alg Del LO G T y 2 d Ed e d Del 3
12. drv derivation trees with METAPOST almost a user s guide Laurent M Hars laurent mehats gmail com documented version 0 97 y A T tB AFC A ATAEBAC BAC OED AMABA ARONA AT AOFD j LAOA gt D E YPF UA D gt E T A 0 A gt D gt E YtF I A O ILY FF Contents 1 Usage 3 1 1 Structure of a METAPOST file using drv 3 12 Ru nn METAPOST a co 246 024 dd ia a ws ees 3 1 3 BDI X inclusioncommands ss n esoo so sa moe gaoi 4 2 Judgment and inference declarations 4 dil TOMO AE do redee Woe ae ep ge E a ae Wiad a we a 4 22 del sog moea ea bee See a EE RES Ee Se 7 23 bed and Md sa doe bea ee kh a a Ea 8 2 4 Sub tree delimiters and labels 10 Available on CTAN You don t need to know METAPOST to use this package Feel free to improve E g by correcting the poor English Last update February 22 2011 3 drv tunings SA My Tont Size ora nara ae Eu Se are DP ee e 3 2 odry Mat Style ae i aea whore ai He e oE ye whe eS Bod Ary Scale e aai h a eed usin a 34 drv_junction style csa a ae cresents tiss 3 5 dry _alignme t style o q sa ecos ew ae e e 36 dry path style res veere raara we a Ea 37 drv labels position rsss sser breresr a we 8 3 8 drv roots POSITION gt ar bo ADE E aa eS 39 drv axis reference sesir esrs t EEEIEI CE 3 10 drv_left_delimiter and drv_right_delimiter 311 dry box mod ae ba ee a A Re ES 3 12 drv_fraction mode 6s caw ak C
13. efers to the depth of a judgment math axis relatively to the axis of an inference line above it while the latter refers to the height of a judgment math axis relatively to the axis of an inference line below it Depths are negative while heights are positive beginfig 470 dcl 0 C 0 gamma dcl 1 0 1 delta draw drv_tree endfig The picture below may look weird if you don t use scalable fonts gt a ds WEN jdg 0 hg math axis 7 AA WA A jdg 0 c jdg 0 dp num_hg EEE A L iln 1 c dendp Sw jdg 1 hg math axis M Ao uy A jdg 1 dp 26 INSIDE DERIVATION TREES 6 2 drv_styled drv_styled enables the drawing of METAPOST paths using drv path styles path drv_styled id path METAPOST path expression id path style identifier 0 1 2 3 4 5 or 6 beginfig 490 jgm 4 A vdash A jom 5 B _2 vdash B _3 jgm 6 A A multimap B _1 vdash B _4 jgm 7 A Amultimap B _0 vdash A Amultimap B _5 fr 4 O CTS _ nfr 5 O C 1 nfr 6 4 5 C multimap_ L _ nfr 7 6 C multimap_ R _ drv_freeze B draw sbj 7 2 c shifted 0 num_hg 0 sbj 7 2 c up 0 sbj 6 4 c 1 sbj 5 0 c tension 1 2 2 sbj 51 3 c 3 sbj 6 7 c 4 sbj 7 7 c down 5 sbj 7 7 c shifted 0 num_hg 5 drv_styled 2 withcolor 1 0 0 draw drv_tree
14. egraphics 1 raisebox Gin lly bp usebox graphicsbox makeatother The code for drv was suggested by Josselin Norret on the fr comp text tex Usenet group 2 Judgment and inference declarations 2 1 jgmandnfr jgm nat str list nat judgment index str list sub judgments math mode ATEX code nfr nat nat list C str id nat inference index nat list list of premise indices str inference label math mode IATEX code id inference line style identifier 0 1 2 3 4 5 6 or _ jgm nat declares a judgment which index is nat while nfr nat declares an inference which conclusion is the index nat judgment you can declare a judg ment before or after the corresponding inference no matter A premise index nat refers to the sub tree ending with the index nat judg ment A list of premise indices may be arbitrary long You may get standalone picture files e g transparent PNG for inclusion in a webpage from each jobname index file as described in Appendix E 2 1 jgmand nfr First example beginfig 110 jgm 0 Alvdash B jgm 1 B vdash C jgm 2 A vdash C nfr 0 O C f 1 nfr 1 Q Cg 1 nfr 2 0 1 C circ 1 draw drv_tree endfig Sub judgments beginfig 111 jgm 0 Alvdash B jgm 1 A vdash B nfr 0 O Cf 1 nfr 1 0 Cf 1 draw drv_tree endfig The outputs induced by jgm 0 A vdash B and ALR BEC
15. ely Radial constraints are essentially the same as vertical ones however each component comes also with a radius cpn rad and an origin point cpn org You can prevent drv from stating angular constraints about premises junction or judgments alignment by using the junction style 3 or the alignment style u of the NFR and NFR_opt macros see 5 1 5 2 Then again you have to state your own constraints As an example compare the code below with the one for figure 510 on page 27 beginfig 590 vdash jgm 0 B A Gamma vdash C sbj 0 1 jgm 1 A Gamma vdash B multimap C sbj 1 1 jgm 2 Gamma vdash A multimap B multimap C sbj 2 1 NFRopt 0 OOO _ 9 NFR_opt 1 0 C multimap_R C u 1 caution u NFR_opt 2 1 C multimap_R C u 1 caution u sbj 1 1 cng sbj 0 1 cng sbj 1 1 lng sbj 0 1 rng sbj 2 1 cng sbj 1 1 cng sbj 2 1 lng sbj 1 1 rng draw drv_tree endfig o ree O C pate on soe UA resp ph AE E TrA B Cy e TrA EBO D Gallery Here are two simple derivation trees figures 600 601 id id id id ara ltl ata ll as i a a oltl a a oltl E id te dd a olta ol Tel at lo a l l l AAA eta hostel ae lo ao1I o1 17 E id E id lo a ol 1lo a l ltl le a l lta l ltl l a g a 1l aoDel t 1 1 34 GALLERY Here are the drv version of a derivation t
16. f should be part of your TEX distribution Next you may get a standalone ps file jobname index ps by running pdftops jobname index pdf pdftops is part of the Xpdf software package Finally you may get a standalone transparent PNG file jobname index png by running convert jobname index ps jobname index png convert is part of the ImageMagick software package Notice that you can run convert on jobname index pd but then the pn6 file you get is not transparent F Related packages e bussproofs sty Samuel R Buss e mathpartir sty Didier R my e proof sty Makoto TATSUTA e prooftree sty Paul TAYLOR e the Ptree constructor from metaobj mp Denis RokGEL see 5 e semantic sty Peter M ller NEERGAARD and Arne John GLENSTRUP e trfrac sty Kevin W HAMLEN e virginialake sty Alessio GUGLIELMI Some of these are described on Peter SmITH s BIEX for Logicians webpage
17. gment and of the correspond ing inference dcl nat nat list str id str list is a shorthand for jgm nat str list nfr nat nat list beginfig 140 dcl 0 Cf 1 A vdash B dcl 1 C g 1 B vdash C dcl 2 0 1 C circ 1 A vdash C draw drv_tree endfig beginfig 141 dcl 0 C f 1 A vdash B dcl 1 0 CE 1 MAS vdash Bis draw drv_tree endfig str id AEB BEG AFC resp 8 JUDGMENT AND INFERENCE DECLARATIONS beginfig 150 dcl 0 1 5 9 C a _ OT dcl 1 2 3 4 C b _ 00 d l 2 Cc _ 000 dcl 3 Cd _ 001 dcl 4 O Ce _ 002 del 5 6 7 8 Cf _ 01 dd 6 C g _ 010 del 7 C h _ 011 dcl 8 C i _ 012 d l 9 10 11 12 C j 02 dcl 10 CUk _ 020 d l 11 CI 021 dl 12 Cm _ 022 draw drv_tree endfig c d e g h i k 1 m 000 001 002 i 010 011 ue 020 021 022 00 01 02 a 0 2 3 bxd and mvd bxd A premise index nat can be replaced with bxd nat so that the whole sub tree ending with the index nat judgment behaves as if it was enclosed within a box beginfig 160 dcl 0 1 4 Cre _ ta dcl 0 bxd 1 4 CU _ a acl 1 2 qu _ are del 2 3 Ge A _ a del 3 C _ aaaaaaa dd 4 OQO Cia aaaaa draw drv_tree endfig daaaaaaa daaaaaa daaaaaaa a a a a aaaaa a aaaaa a aaaaa
18. ime I m pretty sure that the derivation tree won t fit on the page It does Amazing 5 2 Optional labels NFR_opt The NFR_opt declaration macro is an alternative for NFR that lets you specify labels at your option NFR_opt nat nat list str list 1 lt str list 2 Cid 1 id 2 id 3 nat inference index nat list list of premise indices str list 1 list of inference labels math mode BTEX code str list 2 list of delimiter labels math mode 1XIfX code id 1 junction style identifier 0 1 2 3 or _ id 2 alignment style identifier 1 c r u or _ id 3 inference line style identifier 0 1 2 3 4 5 6 or _ The list str list 1 may contain zero one or two strings specifying inference labels If no label is specified then no label is attached to the inference line If two labels are specified then the first one is attached to the left and the second one to the right Finally if one label only is specified then it is attached either to the left or to the right of the inference line depending on the default inference labels position set by drv_labels_position see 3 7 The same way str list 2 may contain zero one or two strings specifying de limiter labels If one label only is specified then it is attached to a delimiter placed 5 3 User defined declaration macros tricky 23 either to the left or to the right of the sub tree ending with the index nat judgment depending on the default delimi
19. jgm 1 a ae AFC vdash i are the same Using the latter declaration you can manipulate sub judgments inde pendently from each other see 6 Inference line styles nfr 5 C leftarrow 6 6 nfr 6 C leftarrow _ _ draw drv_tree endfig beginfig 120 jgm 0 text none jgm 1 text simple jgm 2 text double jgm 3 text dotted jgm 4 text dashed jgm 5 text waved jgm 6 text TeX dotted jgm 7 text default nfr 0 C C leftarrow 0 0 nfr 1 0 C leftarrow 1 1 nfr 2 1 C leftarrow 2 2 nfr 3 2 C leftarrow 3 3 nfr 4 3 C leftarrow 4 4 nfr 5 4 C leftarrow 5 5 6 7 0 none l simple 2 AENA lt 3 eee AG ie ee E TEX dotted default JUDGMENT AND INFERENCE DECLARATIONS The default inference line style is set by the drv_path_style macro see 3 6 Declarations order Declarations may occur in any order beginfig 130 beginfig 131 preorder declarations postorder declarations jgm 0 0 jgm 0 000 jgm 1 00 jgm 1 001 jgm 2 000 jgm 2 002 jgm 3 001 jgm 3 00 jgm 4 002 jgm 4 010 jgm 5 01 jgm 5 011 jgm 6 010 jgm 6 012 jgm 7 011 jgm 7 01 jgm 8 012 jgm 8 020 jgm 9 02 jgm 9 021 jgm 10 020 jgm 10 022 jgm 11 021 jgm 11 02 jgm 12 022 jgm 12 0 nfr 0 1 5 9 C a _ nfr 0 a _ nfr 1 2 3 4 C b _ nfr 1 O Cb
20. lm 1 endfig 20 Low LEVEL INFERENCE DECLARATION MACROS math axis z lb 4 2 E resp resp E b Notice that drv_axis is irrelevant if you don t use the drv inclusion command 5 Low level inference declaration macros 5 1 NFR DCL and MVD NFR The NFR declaration macro is the lowest level one It enables the specifica tion of all the labels and styles of an inference NFR nat nat list str 1 str 2 str 3 str 4 id 1 id 2 id 3 nat inference index nat list list of premise indices str 1 left inference label math mode IATEX code str 2 right inference label math mode 14IpX code str 3 left delimiter label math mode I4TRX code str 4 right delimiter label math mode IX code id 1 junction style identifier 0 1 2 3 or _ fully interlacing 1 semi interlacing 2 non interlacing 3 user specified tricky see 6 3 default set by drv_junction_style see 3 4 id 2 alignment style identifier 1 c r u or _ 1 left c centered r right u user specified tricky see 6 3 default set by drv_alignment_style see 3 5 id 3 mene line style identifier 0 1 2 3 4 5 6 or _ beginfig 430 jgm 0 aa NFR 0 O Cr Eran ba ae VAM e De e 3 7 4 draw drv_tree endfig 5 1 NFR DCL and MVD 21 DCL The DCL declaration macro is a shorthand for jgm and NFR in the same way as dcl is a shorthand for jgm and nfr beginfig 440 DCL 0 O C1 a eae E
21. n trees x default style displaystyle jdg judgments x default style textstyle x ilb inference labels x default style scriptstyle x dlb delimiter labels x default style textstyle x plb phantom steps labels x default style textstyle x str ATEX math style command drv_math_style drv displaystyle textstyle scriptstyle 1 2 444 b af T E 33 c 7 drv_math_style jdg displaystyle textstyle scriptstyle 1 4 A Aj b 1 2 iel 4 Niet Ai b A Neri b 3 m 3 3 C C c drv_math_style ilb textstyle scriptstyle scriptscriptstyle 2 2 1 a b a b a 3 3 3 c c c Notice that the math style of derivation trees determines the math style of judg ments and of labels in the same way as the math style of fractions determines the math style of numerators and denominators 3 3 drv_scale drv_scale id float id scale identifier clr prm jdg or ilb clr nice explanation soon see examples prm nice explanation soon see examples jdg nice explanation soon see examples ilb nice explanation soon see examples scale value x default scale 1 x x default scale 1 x x default scale 1 x default scale 1 x float 3 4 drv_junction_style drv_scale drv_scale drv_scale drv_scale 3 4 This macro sets the default way the premises of an inference 0 a a prm 0 aa a jgm 0 aa a
22. nfr 2 O C c _ nfr 2 O Cc _ 3 nir 3 Cd nfe 3 0 1 2 Cd 3 nfr 4 O Ce _ nfr40 Ce nir 5 6 73 8 CL JS nftr50Cf _ nfr 6 O C g _ nfr 6 O g _ nfr 7 O Ch nfr 7 4 5 6 C h _ nfr 8 O Ci nfr 8 O Ci 5 nfr 9 10 11 12 C j _ nfr 9 O Cj _ 3 nfr 10 C k _ nfr 10 CK _ nfr 11 O I _ nfr 11 8 9 10 1 _ nfr 12 O Cm _ nfr 12 G 75 TD Came Y draw drv_tree draw drv_tree endfig endfig c d e g h i k 1 m 000 001 002 A 010 011 Oe 020 021 Of 00 01 02 p 130 0 a b c e f g i j k 000 001 002 010 011 012 020 021 022 00 01 02 m 131 0 2 2 del Code for the title page derivation tree beginfig 100 jgm 0 Gamma Delta Theta Pi Upsilon vdash F jgm 1 Pi vdash A to D to E jgm 2 Gamma Delta Theta A to D to E Upsilon vdash F jgm 3 Gamma Delta Theta vdash A to D jgm 4 A Gamma Delta Theta vdash D jgm 5 A Gamma Delta vdash B wedge C jgm 6 A Gamma vdash B jgm 7 Delta vdash C jgm 8 B wedge C Theta vdash D jgm 9 E Upsilon vdash F nfr 0 1 2 C text cut 1 nfr 10 C pi 4 nfr 2 3 9 C to_L 1 nfr 3 4 to_R 1 nfr 4 5 8 C text cut 1 nfr 5 6 7 C wedge_R 1 nfr 6 C gamma 2 nfr 7 O C delta 1 nfr 8 theta 3 nfr 9 O C upsilon 2 draw drv_tree endfig 2 2 dcl dcl enables the simultaneous declarations of a jud
23. osition 15 Setting a default position for delimiter labels thus for delimiters and for phantom steps labels may be useful in conjunction with declaration macros taking optional label arguments see 5 2 3 8 drv_roots_position drv_roots_position id a aaa a id position identifier t or b P a a a t top b bottom default x 3 9 drv_axis_reference The baseline of derivation tree pictures is set in such a way that their math axis co incides either with the axis of their root inference line or with the math axis of their root judgment according to the default behaviour set by drv_axis_reference drv_axis_reference id id reference identifier iln or jdg iln root inference line axis x default jdg root judgment math axis aa math axis a Notice that drv_axis_reference is irrelevant if you don t use the drv inclusion command see 1 3 3 10 drv_left_delimiter and drv_right_delimiter drv_left_delimiter str str left delimiter math mode TEX code C i Ibrace default x langle etc 16 DRV TUNINGS drv_right_delimiter str str right delimiter math mode IATEX code 2e J rbrace x default x rangle gt etc drv_left_delimiter n e 1floor n A n iB iB iB El c d El c d E c d F f f drv_right_delimiter rangle uparrow man ae 2 IB LB Ex ec d Ex c d Ex c d f f f 3 11 drv_box_mode When in bo
24. ree found in 4 p 57 and an alternative for it figures 610 611 11 Rr r2 To AL AL 1 Ara Pri A AR F rn Arn Ar II PO qrqV r Ara Nd NON y p p GVO VE GV ri Ar Ga 1 2 PAQV ri Ar P PAQGVMAN EAVMAN o PAV ri Ar2 F PA GV 11 A r2 11 IF A 12 12 SS fh Hp Id ran 4 Ce eal rT ATr2 72 AR YT Ato r Aro Id qy r Ar2 qq UR i 1 VR qrqv r Ar ANTENA qV ri Arz qV 11 Ar2 PHP ALi AL gt PAV 1 Arz p PAGVMAN EGVMIAN o PAV Ti Ar2 Ft PAV ri A 12 Here are overlapping trees with opposite directions figure 540 code on page 30 ho go f AEC CFD AFD AHB B D o hogjof 35 Here is the drv version of a derivation tree found in 5 p 86 figure 620 I Ih n T BHA T CHA RENCIA F B CA o IaB GAAN mix 1 Ils Il Ils I B C A Ih ey T BA PEBVGA I t B C A mix y TT Va Ta T B A A T CHA Yt BVCN A AA ay i Tra I TA F C A A A Al TA LT F A A igs Ta Ta I Ta I E A A A A4 A A3 a contrg contrg Tra IT F A A Here are the drv versions of derivation trees found in 6 p 50 figures 630 631 E Standalone picture files Given a PostScript file jobname index generated by METAPOST you may get a standalone por file with embedded fonts jobname index pdf by running mptopdf jobname index 36 RELATED PACKAGES mptopd
25. tatus identifier on or off on off x default on off i i 4 i y dal ME AFA Pe 241A BF h A A BEB gt 34 Br A gt E A BrtA oB Red numbers resp dots refer to judgment indices resp central points see 6 1 while blue numbers resp dots refer to sub judgment indices resp central points see 6 1 18 PICTURES BOUNDING BOXES AND MATH AXIS 3 14 drv_labels_mode This macro turns the typesetting of labels on or off whether labels are specified or not drv_labels_mode id 1 id 2 id 1 label type identifier ilb p1b or d1b ilb inference labels default status on dlb delimiter labels x default status on plb phantom steps labels default status on x id 2 status identifier on or off 3 15 drv_verbatimtex This macro enables the use of IATEX material that is not intended to be typeset e g renewcommand statements by adding a METAPOST verbatimtex etex block to jobname delayed mp drv_verbatimtex str str IEX material 4 Pictures bounding boxes and math axis 4 1 drv_freeze and drv_tree drv composes derivation trees with respect to judgment and inference declarations only once the drv_freeze macro is called This is usually done by drv_tree which is a macro that returns a picture You may however call drv_freeze your self if you have no need for the whole derivation tree picture that drv_tree would otherwise return Section 6 1 illustrates such a situation drv composes derivation
26. ter labels position set by drv_labels_position As an example nfr nat nat list str id behaves exactly the same way as NFR_opt nat nat list Cstr O E _ d DCL_opt The DCL_opt declaration macro is a shorthand for jgm and NFR_opt in the same way as DCL is a shorthand for jgm and NFR MVD_opt The MVD_opt macro is an alternative for MVD that lets you specify labels at your option MVD_opt nat 1 nat 2y C str list Cid 1 id 2Y nat 1 index of the origin judgment nat 2 number of phantom steps str list list of labels math mode ISTRX code id 1 alignment style identifier 1 c or r id 2 phantom steps path style identifier 0 1 2 3 4 5 6 or _ The list str list may contain zero one or two strings specifying labels If one label only is specified then it is attached either to the left or to the right of the phantom steps path depending on the default phantom steps labels position set by drv_labels_position see 3 7 5 3 User defined declaration macros tricky Here are the METAPOST headers for NFR MVD NFR_opt and MVD_opt NFR text PRM expr lilb rilb ldlb rdlb suffix jsty asty isty MVD expr num lplb rplb suffix asty psty NFR_opt text PRM text ILB text DLB suffix jsty asty isty MVD_opt expr num text PLB suffix asty psty in the header of a macro indicates that this macro expects a numeric argument referred to as Q in its bod
27. tion 3 xpart jdg 1 c xpart jdg 0 c 5cm draw drv_tree endfig You may check that the distance between the two dots above is 5 cm User specified alignment style The horizontal constraints you state should ex press how the inferred judgment has to be aligned with respect to its premises beginfig 510 vdash jgm 0 B A Gamma vdash C sbj 0 1 jgm 1 A Gamma vdash B multimap C sbj 1 1 jgm 2 Gamma vdash A multimap B multimap C sbj 2 1 DL L NFR_opt 0 0 OO _ 0 NFR_opt 1 0 C multimap_R C u 1 caution u NFR_opt 2 1 C multimap_R C u 1 caution u xpart sbj 1 1 c xpart sbj 0 1 c xpart sbj 1 1 l xpart sbj 0 1 r xpart sbj 2 1 c xpart sbj 1 1 c xpart sbj 2 1 l xpart sbj 1 1 r draw drv_tree endfig BA FC B A T EC ATEBZE ATEB gt C R resp R TrA gt B gt C TrA gt B gt C 46 47 48 49 50 51 52 53 54 55 56 57 58 28 DEBUGGING AND PROOFING References 1 John D Hossy A User s Manual for METAPOST 2009 2 Bogus aw JackowsK1 Appendix G illuminated TUGboat 27 1 83 90 2006 3 Donald E Knura The T Xbook Addison Wesley 1984 4 Greg RestaLL Proof Theory and Philosophy Book in progress 2006 5 Denis RoeceL The MetaObj tutorial and reference manual 2002 6 Lutz STRASSBURGER Proof Nets and the Identity of Proofs INRIA 2006 A Debugging and proofing Debugging Recall that you ha
28. trees essentially according to the algorithm for com posing fractions described in Appendix G of the TRXbook see 2 3 In particular drv uses fontdimen parameters so that the derivation tree pictures it generates should integrate smoothly within any document whatever the fonts you use As an example compare the following fractions the first one is composed by drv while the second one is composed by the standard frac command 22 resp resp resp 4 2 drv_bbox 19 4 2 drv_bbox drv_bbox nat nat sub tree root index drv_bbox nat returns a METAPOST closed path see 1 Section 4 stand ing for the bounding box of the sub tree ending with the index nat judgment drv_bbox calls drv_freeze if necessary beginfig 410 dcl 0 C1 5 C _ a dcl 0 bxd 1 5 C _ a del 1 2 3 4 C _ pres del 2 0 gt AE O al dela O e dels O E fill drv_bbox 1 withcolor 255 230 205 255 rgb color draw drv_tree endfig 4 3 drv_axis drv_axis locally overrides drv_axis_reference see 3 9 enabling the ex plicit setting of the math axis of a tree once it has been drawn drv_axis id nat id reference type identifier iln jdg or dlm iln inference line axis jdg judgment math axis dlm delimiter axis nat reference index beginfig 420 Del 0 C Ce MME ag _ ars Del 1 0 Ch EF 0 LD b draw drv_tree drv_axis iln 0 drv_axis jdg 1 drv_axis d
29. ve to run mpost jobname mp at least twice once more if you use sub tree delimiters If you get an error on the first run then it comes from the drv METAPOST code If you get an error on the second run then it comes from the IATEX code Error on the first run METAPOST behaves essentially as TEX BTEX when it finds and error see 1 Debugging It stops explains the error in some way look for the line starting with an exclamation mark shows some lines of context and asks you what to do next answer h to get some help or x to terminate the run If you re lucky the error comes from an inconsistency that drv can detect In such a case the explanation should be quite understandable beginfig 520 METAPOST error message jgm 0 ANvdash B jgm 1 B vdash C drv fig 520 0 has been used jgm 2 A vdash C already as a premise index for jgm 3 C vdash D inference declaration 2 jgm 4 A vdash D error context nfr 0 O C _ 1 56 nfr 4 0 3 circ 1 nfr 1 0 C a nfr 2 0 1 circ _ nfr 3 C h _ nfr 4 0 3 C circ _ draw drv_tree endfig 29 Error on the second run METAPOST fails to preprocess the ATEX code in jobname delayed mp and suggests that you see mpxerr log which is a reg ular ATEX log file This file shows you which part of the TEX code is faulty but unfortunately not where to find it in Gobname mp Proofing Recall that for each beginfig index
30. x mode derivation trees are typeset in such a way that all sub trees behave as if they were enclosed within boxes that is as if all premise indices were prefixed with bxd see 2 3 drv_box_mode id id status identifier on or off on off x default on typeset as off daaaaaa aaaaaaa aaaaaaa a a a aaaaa a aaaaa a aaaaa a 3 12 drv_fraction_mode 17 3 12 drv_fraction_mode drv typesets derivation trees in such a way that the distance from the axis of an inference line to the math axis of a judgment above it is always the same num_hg see 6 1 the distance from the axis of an inference line to the math axis of a judgment below it is always the same den_dp see 6 1 When in fraction mode if roots are at bottom then the height of leaf judgments above which there is no inference line is ignored the depth of root judgments is always ignored if roots are at top then the depth of leaf judgments below which there is no inference line is ignored the height of root judgments is always ignored This mode may cause overlaps when used in conjunction with interlacing junction styles 0 and 1 drv_fraction_mode id id status identifier on or off on x default off on off typeset as An a AT B BA IILE BAC AVtB BAC ATrB BAtC AIrB BAC m cut A T AKC A T AKC A T AKC ee re FR LAPAS PAKIS E CALASC 3 13 drv_proof_mode drv_proof_mode id id s
31. y text expr and suffix specify argument types see 1 Section 10 You may use NFR MVD NFR_opt and MVD_opt to define your own declaration macros As an example here are possible definitions for Nfr and Mvd vardef Nfr text PRM expr ilb ldlb rdlb suffix isty NFR_opt 0 PRM ilb ldlb rdlb _ _ isty enddef vardef Mvd expr num lplb rplb suffix psty MVD Q num lplb rplb _ psty Mvd returns an index no enddef 24 INSIDE DERIVATION TREES 6 Inside derivation trees 6 1 Components distinguished points and dimensions Components Once drv_freeze has been called all the components of a deriva tion tree are accessible independently from each other Given an inference in dex nat you can access the inference components provided they were declared via the following indentifiers judgment jdg nat sub judgments sbj nat nat inference line iln nat left inference label 1_ilb nat right inference label r_ilb nat left delimiter 1_dlm nat left delimiter label 1_dlb nat right delimiter r_dlm nat right delimiter label r_dlb nat phantom steps path phm nat left phantom steps label 1_plb nat right phantom steps label 1_plb nat The sub judgment index nat ranges from 0 to the number of sub judgments mi nus 1 beginfig 470 components O Oe 8 gO BEL GE COC I A Bh TN DCL 7 GD 6 2 Gy O 2 OC My hy en Se DY drv_free
32. ze usually called by drv_tree draw jdg 5 judgment A draw sbj 6 0 withcolor 3 0 0 3 sub judgment B draw sbj 6 1 withcolor 2 0 0 3 sub judgment C draw iln 6 withcolor 0 4 0 4 inference line draw 1_ilb 6 withcolor 0 3 0 4 left inference label 1 draw r_ilb 6 withcolor 0 2 0 4 right inference label 2 draw 1_dlm 6 withcolor 0 0 3 3 left delimiter draw 1_dlb 6 withcolor 0 0 2 3 left delimiter label 3 draw r_dlm 6 withcolor 3 0 3 3 right delimiter draw r_dlb 6 withcolor 2 0 2 3 right delimiter label 4 draw phm 6 withcolor 0 3 3 4 phantom steps path draw l_plb 6 withcolor 0 2 2 4 left phantom steps label 5 draw r_plb 6 withcolor 0 1 1 4 right phantom steps label 6 draw jdg 7 judgment D draw iln 7 inference line endfig 6 1 Components distinguished points and dimensions 25 Distinguished points Three distinguished points are associated with each com ponent cpn namely cpn 1 cpn c and cpn r that lie respectively to the left at the center and to the right of the component math axis components central points 3 4 0 2 2 4 s Doge ji 5 6 3 6 D 5 Dimensions Two dimensions are associated with each component cpn a depth cpn dp and a height cpn hg that both are relative to the component math axis Two overall dimensions are associated with each derivation tree den_dp and num_hg The former r
Download Pdf Manuals
Related Search