Exported

Returns whether PRef pr in context $lp$ is bound in the PDRS gp, where:

pdrsBoundRef pr lp gp iff

There exists a context pv, such that

1. pv is accessible from the introduction site of pr (lp); and
2. pv is accessible from the interpretation site of pr (p); and
3. together with the PDRSRef of pr (r), pv forms a PRef that is introduced in some universe in gp.

Returns whether PRef pr1 introduced in local PDRS lp is bound by projected referent pr2 in PDRS pdrs, where:

boundByPRef pr1 lp1 pr2 pdrs iff

1. pr1 and pr2 share the same referent; and
2. pr2 is part of some universe in pdrs (i.e., can bind referents); and
3. The interpretation site of pr2 is accessible from both the introduction and interpretation site of pr1.

Returns whether a referent is bound by some other referent than itself.

Returns whether pv is a free projection variable in PDRS p, where:

pdrsIsFreePVar pv p iff

• context pv is accessible from the global context, or
• there is no context v that is accessible from pv and also from the global context.

Returns whether a pointer p in local PDRS lp is bound by a label in the global PDRS gp, where:

pdrsBoundPVar p lp gp iff

• p is equal to the label of either lp or gp; or
• there exists a PDRS p with label pv, such that p is a subPDRS of gp and p is accessible from lp.

Note the correspondence to drsBoundRef.

Returns the list of all free PRefs in a PDRS

Returns the list of all free PVars in a PDRS lp, which is a subPDRS of global PDRS gp