dedekind::sets::Pred< K > Struct Template Reference

A relational predicate built at run time: comparisons of terms and their connectives; defined after the binding below. More...

Collaboration diagram for dedekind::sets::Pred< K >:

Public Types
enum class	Kind {   Cmp , And , Or , Top ,   Bottom , Exists , Forall }
using	is_rel_predicate = void

Public Member Functions
constexpr bool	quantifier () const
	Whether this node is ∃ or ∀.
constexpr Pred	subst (unsigned variable, const Term< K > &with) const
	The predicate with the variable variable replaced by the term with in every atom.
template<typename F>
constexpr Pred	map_slots (const F &f) const
	Every slot of every atom replaced at once (Term::map_slots).
constexpr Pred	negated () const
	!p, in negation normal form.
template<typename P>
constexpr bool	operator() (const P &x) const

Static Public Member Functions
static constexpr Pred	exists (std::size_t sort, unsigned slot, Pred body)
	∃π_slot ∈ sort. body.
static constexpr Pred	forall (std::size_t sort, unsigned slot, Pred body)
	∀π_slot ∈ sort. body, dual to exists.
static constexpr Pred	bound_like (const Pred &q, Pred body)
	The quantifier of q over a new body.
static constexpr Pred	cmp (Rel r, Term< K > x, Term< K > y)
	The atom x r y.
static constexpr Pred	conj (Pred x, Pred y)
	x ∧ y.
static constexpr Pred	disj (Pred x, Pred y)
	x ∨ y.
static constexpr Pred	top ()
	⊤ and ⊥, the Boolean algebra's constants: a decided atom written back (0 == 0 is ⊤), free of any sort.
static constexpr Pred	bottom ()

Public Attributes
Kind	kind {Kind::Cmp}
Rel	rel {}
std::shared_ptr< const Term< K > >	a
std::shared_ptr< const Term< K > >	b
std::shared_ptr< const Pred >	p
std::shared_ptr< const Pred >	q
std::size_t	sort {}
unsigned	slot {}

Detailed Description

template<typename K>
struct dedekind::sets::Pred< K >

A relational predicate built at run time: comparisons of terms and their connectives; defined after the binding below.

A relational predicate built at run time: a comparison of two terms, their conjunctions and disjunctions, and the quantifiers ∃ / ∀ over a column of a row. Negation is pushed to the comparisons as it is built (De Morgan; ∃ and ∀ swap), so there is no Not node.

Template Parameters

K	the constants' type.

A quantifier binds the next slot: at points of width n it binds π_{n+1}, of the sort it names, and its body is read at the row extended by that column. Sibling quantifiers therefore bind the same slot in separate scopes and never need renaming apart; a nested one binds π_{n+2}. This is the run-time twin of sets:quantifier's exists / forall, and the ∃ of a relational composition (relational:rows).

Template Parameters

K	the constants' type.

Member Function Documentation

bound_like()

template<typename K>

constexpr Pred dedekind::sets::Pred< K >::bound_like ( const Pred< K > & q, Pred< K > body )

inlinestaticconstexpr

The quantifier of q over a new body.

Parameters

q	a quantifier node.
body	its new body.

cmp()

template<typename K>

constexpr Pred dedekind::sets::Pred< K >::cmp ( Rel r, Term< K > x, Term< K > y )

inlinestaticconstexpr

The atom x r y.

Parameters

r	the comparison.
x,y	the terms.

Returns

the predicate.

conj()

template<typename K>

constexpr Pred dedekind::sets::Pred< K >::conj ( Pred< K > x, Pred< K > y )

inlinestaticconstexpr

x ∧ y.

Parameters

x,y	the predicates.

Returns

the meet.

disj()

template<typename K>

constexpr Pred dedekind::sets::Pred< K >::disj ( Pred< K > x, Pred< K > y )

inlinestaticconstexpr

x ∨ y.

Parameters

x,y	the predicates.

Returns

the join.

exists()

template<typename K>

constexpr Pred dedekind::sets::Pred< K >::exists ( std::size_t sort, unsigned slot, Pred< K > body )

inlinestaticconstexpr

∃π_slot ∈ sort. body.

Parameters

sort	the bound column's sort.
slot	the bound slot, the next past the points' width.
body	the predicate, on the row extended by that column.

map_slots()

template<typename K>

template<typename F>

Pred dedekind::sets::Pred< K >::map_slots ( const F & f ) const

inlineconstexpr

Every slot of every atom replaced at once (Term::map_slots).

Parameters

f	a slot to its replacement.

operator()()

template<typename K>

template<typename P>

bool dedekind::sets::Pred< K >::operator() ( const P & x ) const

inlineconstexpr

Parameters

x	the point (a pair, or a carrier value for an atom on π).

subst()

template<typename K>

Pred dedekind::sets::Pred< K >::subst ( unsigned variable, const Term< K > & with ) const

inlineconstexpr

The predicate with the variable variable replaced by the term with in every atom.

Parameters

variable	the slot.
with	its replacement.

Returns

the substituted predicate.

---

The documentation for this struct was generated from the following file:

• src/main/modules/dedekind/sets/terms.cppm