16.3.5 Encoding Dominance Constraints

We encode a dominance constraint as a functional procedure which inputs a list [N1 N2 ... Nk] of nodes, one for each variable in the input constraint (the graph). Recall that each node comes as a record of set variables. The functional procedure encoding a dominance constraint imposes the right set constraints on these set variables, i.e. those which encode the dominance constraint.

Consider the dominance constraint which is typical for a scope ambiguity with two quantifiers.

We are interested in all solutions of this constraints where no variables are identified. This reflects that quantifiers should not be identified. It is slightly stronger than saying that nodes with distinct labels should not be identified.

Using the DC module, it would be expressed as a record which contains the number of variables and a procedure which inputs a list of nodes and creates set constraints for these nodes and the dominance constraint.

<DomConExample>=

local  
   proc {DomCon [N1 N2 N3 N4 N5]}
      {DC.daughters N1 [N2]}
      {DC.dominates N2 N5}
      {DC.daughters N3 [N4]}
      {DC.dominates N4 N5}
      {ForAll [N1#N2 N1#N3 N1#N4 N1#N5  
               N2#N3 N2#N4 N2#N5  
               N3#N4 N3#N5
               N4#N5]
       proc{$ N#M}
          {DC.notEqual N M}
       end}
   end 
in  
   DomConExample = 'unit'(domCon:DomCon
                          vars:5)
end