from MRS Prolog to Maude for rewriting

teste.maude

fmod ATT is
 pr QID .
 
 sort Att .
 sort Constraint .

 op attrval : String Qid -> Att .
 op attrval : String String -> Att .
 
 op qeq : Qid Qid -> Constraint .
endfm

view Att from TRIV to ATT is
  sort Elt to Att .
endv

view Constraint from TRIV to ATT is
  sort Elt to Constraint .
endv

fmod EP is
  inc LIST{Att} * ( op (__) to (_,_) ) .

  sort EP .
  sort Atts .

  op [_] : List{Att} -> Atts .
  op rel : String Qid Atts -> EP .
endfm

view EP from TRIV to EP is
  sort Elt to EP .
endv

fmod MRS is
  inc LIST{Constraint} * ( op (__) to (_,_) ) .
  inc LIST{EP} * ( op (__) to (_,_) ) .

  sort EPs Mrs Constraints HCons .

  op [_] : List{EP} -> EPs .
  op [_] : List{Constraint} -> Constraints .

  op hcons : Constraints -> HCons .

  op psoa : Qid Qid EPs HCons -> Mrs .

endfm


*** rewriting module congruence. we can specify patterns over subterms.

mod TEST is
 inc MRS .

 vars V0 V1 V2 V3 : Qid .

 rl rel("compound",V0,
        [attrval("ARG0",V1),
         attrval("ARG1",V2),
         attrval("ARG2",V3)]) =>
    rel("EQUAL",V0,
        [attrval("ARG0",V1),
         attrval("ARG1",V2),
         attrval("ARG2",V3)]) .

endm

*** for testing, from Prolog output:
***   - [x] variables to Qid
***   - [x] 'string' to "string"
***   - [ ] need to extend the prolog notation to the attributes of vars


rew psoa('h0,'e2,
  [rel("person",'h4,
       [attrval("ARG0",'x3)]),
   rel("_some_q",'h5,
       [attrval("ARG0",'x3),
        attrval("RSTR",'h6),
        attrval("BODY",'h7)]),
   rel("_live_v_1",'h4,
       [attrval("ARG0",'e8),
        attrval("ARG1",'x3)]),
   rel("_in_p_dir",'h4,
       [attrval("ARG0",'e9),
        attrval("ARG1",'e8),
        attrval("ARG2",'x10)]),
   rel("proper_q",'h11,
       [attrval("ARG0",'x10),
        attrval("RSTR",'h12),
        attrval("BODY",'h13)]),
   rel("compound",'h14,
       [attrval("ARG0",'e15),
        attrval("ARG1",'x10),
        attrval("ARG2",'x16)]),
   rel("proper_q",'h17,
       [attrval("ARG0",'x16),
        attrval("RSTR",'h18),
        attrval("BODY",'h19)]),
   rel("named",'h20,
       [attrval("ARG0",'x16),
        attrval("CARG","Dreadbury")]),
   rel("named",'h14,
       [attrval("ARG0",'x10),
        attrval("CARG","Mansion")]),
   rel("_kill_v_1",'h1,
       [attrval("ARG0",'e2),
        attrval("ARG1",'x3),
        attrval("ARG2",'x23)]),
   rel("proper_q",'h24,
       [attrval("ARG0",'x23),
        attrval("RSTR",'h25),
        attrval("BODY",'h26)]),
   rel("compound",'h27,
       [attrval("ARG0",'e28),
        attrval("ARG1",'x23),
        attrval("ARG2",'x29)]),
   rel("proper_q",'h30,
       [attrval("ARG0",'x29),
        attrval("RSTR",'h31),
        attrval("BODY",'h32)]),
   rel("named",'h33,
       [attrval("ARG0",'x29),
        attrval("CARG","Aunt")]),
   rel("named",'h27,
       [attrval("ARG0",'x23),
        attrval("CARG","Agatha")])],
  hcons([qeq('h0,'h1),qeq('h6,'h4),qeq('h12,'h14),qeq('h18,'h20),qeq('h25,'h27),qeq('h31,'h33)])) .


eof

***(

 under specific condition, the underspecified compound relation can be refined to
 equality. If the HEAD is a proper noun,

  'aunt Mary'
  ~> aunt(x) /\ Mary = z /\ compound(e,x,z)
  ~> aunt(x) /\ Mary = z /\ x = z
  ~> aunt(x) /\ Mary = x
)

?h0: proper_q[ARG0 ?x1, RSTR ?H11]
?h1: compound[ARG1 ?x1, ARG2 ?x2]
?h1: ?p1[ARG0 ?x1]
?h2: ?p2[ARG0 ?x2]
?H11 > ?H1 
=>

?h0: proper_q[ARG0 ?x1, RSTR ?H11]
?h1: EQUAL[ARG1 ?x1, ARG2 ?x2]
?h1: ?p1[ARG0 ?x1]
?h2: ?p2[ARG0 ?x2]
?H11 > ?H1 

eof

mod TEST is
 inc MRS .

 vars V1 V2 H24 H27 H33 X23 X29 : Qid .
 vars ES1 : List{EP} .
 var AS1 AS2 AS3 : Atts .
 var HS : HCons .
 vars S1 S2 : String .

 rl
   rel("proper_q", H24, [AS1 attrval("ARG0", X23)])
   rel("compound", H27, [AS2 attrval("ARG1", X23) attrval("ARG2", X29)])
   rel(S1,         H33, [AS3 attrval("ARG0", X29)])
   rel("named",    H27, [attrval("ARG0", X23) attrval("CARG",S2)])
  => 
   rel("proper_q", H24, [AS1 attrval("ARG0", X23)])
   rel("EQUAL",    H27, [AS2 attrval("ARG1", X23) attrval("ARG2", X29)])
   rel(S1,         H33, [AS3 attrval("ARG0", X29)])
   rel("named",    H27, [attrval("ARG0", X23) attrval("CARG",S2)]) .

endm


eof

***(

 I can make the lists, bags (soups). I can make the ARG? and CARG
 predefined constants and simplify the notation of AttrVal.

 I can make qeq an infix operator. I can add more constraits on the
 shape of the MRS. I can remove the second EP of the compound that
 does not restrict the rule.

 a proper noun need always to be a "named"?

 EQUAL in the relations for further transformation or we can have an
 extra components in the MRS for logical equalities. Or an extra
 constraint besides qeq such as leq.

)

  psoa(V1, V2, [ES1 
   rel("proper_q", H1, AS1 ARG0 X23 RSTR H22)
   rel("compound", H2, AS2 ARG1 X23 ARG2 X29)
   rel("named",    H2, ARG0 X23 CARG S2)
  ], H22 qeq H2 HS) =>

  psoa(V1, V2, [ES1 
   rel("proper_q", H1, AS1 ARG0 X23 RSTR H22)
   rel("EQUAL",    H2, AS2 ARG1 X23 ARG2 X29)
   rel("named",    H2, ARG0 X23 CARG S2)
  ], H22 qeq H2 HS)

alternatives:

1. https://github.com/eyereasoner/eye
2. https://xsb.sourceforge.net/index.html and prolog, both have retract/assert https://www.swi-prolog.org/pldoc/man?predicate=retract/1