next up previous contents
Next: Non-proprietary DATR implementations Up: No Title Previous: DATR theorems syncnode.theo

Semantics trace for syncnode.dtr

"Lamm:<semantics>"-Lamm:<>,<semantics>=Cnoun_er-um.
 [1,0,1] ->  Cnoun_er-um ... ^ <semantics> by III
"Lamm:<semantics>"-Cnoun_er-um:<>,<semantics>=Cnoun_um.
  [2,0,1] ->  Cnoun_um ... ^ <semantics> by III
"Lamm:<semantics>"-Cnoun_um:<>,<semantics>=Cnoun.
   [3,0,1] ->  Cnoun ... ^ <semantics> by III
"Lamm:<semantics>"-Cnoun:<>,<semantics>=Noun.
    [4,0,1] ->  Noun ... ^ <semantics> by III
"Lamm:<semantics>"-Noun:<semantics>,<>=<sem quant> ( <sem root> ).
     [5,0,1] ->  <sem quant> ^ <> by IV
     [5,1,1] ->  sem by I
     [5,1,2] ->  quant by I
"Lamm:<semantics>"-Noun:<sem quant>,<>=lambda [ "<sem arg>" ].
      [6,0,1] ->  lambda by I
      [6,0,2] ->  [ by I
      [6,0,3] ->  "<sem arg>" ^ <> by VII
      [6,1,1] ->  sem by I
      [6,1,2] ->  arg by I
"Lamm:<sem arg>"-Lamm:<>,<sem arg>=Cnoun_er-um.
       [7,0,1] ->  Cnoun_er-um ... ^ <sem arg> by III
"Lamm:<sem arg>"-Cnoun_er-um:<>,<sem arg>=Cnoun_um.
        [8,0,1] ->  Cnoun_um ... ^ <sem arg> by III
"Lamm:<sem arg>"-Cnoun_um:<>,<sem arg>=Cnoun.
         [9,0,1] ->  Cnoun ... ^ <sem arg> by III
"Lamm:<sem arg>"-Cnoun:<>,<sem arg>=Noun.
          [10,0,1] ->  Noun ... ^ <sem arg> by III
"Lamm:<sem arg>"-Noun:<sem arg>,<>=x.
           [11,0,1] ->  x by I
      [6,0,4] ->  ] by I
     [5,0,2] ->  ( by I
     [5,0,3] ->  <sem root> ^ <> by IV
     [5,1,1] ->  sem by I
     [5,1,2] ->  root by I
"Lamm:<semantics>"-Noun:<sem root>,<>="<root sem pred>" [ "<sem arg>" ].
      [6,0,1] ->  "<root sem pred>" ^ <> by VII
      [6,1,1] ->  root by I
      [6,1,2] ->  sem by I
      [6,1,3] ->  pred by I
"Lamm:<root sem pred>"-Lamm:<root sem pred>,<>=baby_ovine.
       [7,0,1] ->  baby_ovine by I
      [6,0,2] ->  [ by I
      [6,0,3] ->  "<sem arg>" ^ <> by VII
      [6,1,1] ->  sem by I
      [6,1,2] ->  arg by I
"Lamm:<sem arg>"-Lamm:<>,<sem arg>=Cnoun_er-um.
       [7,0,1] ->  Cnoun_er-um ... ^ <sem arg> by III
"Lamm:<sem arg>"-Cnoun_er-um:<>,<sem arg>=Cnoun_um.
        [8,0,1] ->  Cnoun_um ... ^ <sem arg> by III
"Lamm:<sem arg>"-Cnoun_um:<>,<sem arg>=Cnoun.
         [9,0,1] ->  Cnoun ... ^ <sem arg> by III
"Lamm:<sem arg>"-Cnoun:<>,<sem arg>=Noun.
          [10,0,1] ->  Noun ... ^ <sem arg> by III
"Lamm:<sem arg>"-Noun:<sem arg>,<>=x.
           [11,0,1] ->  x by I
      [6,0,4] ->  ] by I
     [5,0,4] ->  ) by I
Lamm:<semantics> = lambda [ x ] ( baby_ovine [ x ] ).



Dafydd Gibbon
Sat Jan 6 20:59:29 MET 1996