cuex/semilattice.h: Expression Support for Semilattices
[cuex: Expressions]


#define cuex_joinlattice_bottom   cuex_meetlattice_top
#define cuex_joinlattice_join   cuex_meetlattice_meet
#define cuex_joinlattice_semimeet   cuex_meetlattice_semijoin
#define cuex_joinlattice_geq   cuex_meetlattice_leq
#define cuex_joinlattice_leq   cuex_meetlattice_geq
#define cuex_joinlattice_order(opr, x, y)   cuex_meetlattice_order(opr, y, x)


cuoo_type_t cuex_semilattice_type (void)
cuex_t cuex_meetlattice_top (cuex_meta_t meet)
cuex_t cuex_meetlattice_meet (cuex_meta_t meet, cuex_t x, cuex_t y)
cuex_t cuex_meetlattice_semijoin (cuex_meta_t meet, cuex_t x, cuex_t y)
cu_bool_t cuex_meetlattice_leq (cuex_meta_t meet, cuex_t x, cuex_t y)
cu_order_t cuex_meetlattice_order (cuex_meta_t meet, cuex_t x, cuex_t y)


cuoo_type_t cuexP_semilattice_type

Detailed Description

This provides expressions in a canonical form according to the three axioms of semilattices. Assuming a meet-semilattice, these are

We also assume an identity element ⊤ (top) which fulfils x ∧ ⊤ = x for any x. For join-semilattices, replace ∧ with ∨ (join) and ⊤ with ⊥ (bottom).

Since the operator is stored in the lattice structures, the same functions can be used for both meet- or join-semilattices, as well as other semi-lattice like terms. To avoid confusion while reading client code, separate naming schemes for meet and join semi-lattices are implemented by using #define aliases for the latter.

Elements are considered equal if they are pointer-equal. Since expressions are hash-consed, this gives structural equality. Terms are atomic with respect to a ∧-semilattice if their top-level node is not a ∧ operation.

There is no special treatment of variables.

Function Documentation

cu_bool_t cuex_meetlattice_leq ( cuex_meta_t  meet,
cuex_t  x,
cuex_t  y 

True iff x = xy.

cuex_t cuex_meetlattice_meet ( cuex_meta_t  meet,
cuex_t  x,
cuex_t  y 

For a ∧-semilattice where meet = ∧, returns xy in a canonical form with respect top-level ∧-terms of x and y.

cu_order_t cuex_meetlattice_order ( cuex_meta_t  meet,
cuex_t  x,
cuex_t  y 

Returns the most precise ordering predicate for x and y.

cuex_t cuex_meetlattice_semijoin ( cuex_meta_t  meet,
cuex_t  x,
cuex_t  y 

This computes xy where ∨ is the dual of ∧ = meet, under the assumption that ab = ⊤ for any two distinct atomic terms a and b.

cuex_t cuex_meetlattice_top ( cuex_meta_t  meet  ) 

Returns the top element of the ∧-semilattice, where ∧ = meet. This is also the identity element.

Generated 2009-11-23 for culibs-0.25 using Doxygen. Maintained by Petter Urkedal.