Forlan Manual

The SymRel Module

Synopsis

signature SYM_REL
structure SymRel :> SYM_REL

This module provides operations on finite relations on Forlan symbols, i.e., values of type sym_rel = (Sym.sym, Sym.sym)Rel.rel that are standard in the sense that they are compatible with Set.comparePair(Sym.compare, Sym.compare). All values of type sym_rel will implicitly be assumed/required to be standard.

Interface

type sym_rel = (Sym.sym, Sym.sym) Rel.rel
val comparePair : (Sym.sym * Sym.sym) Sort.total_ordering
val memb : (Sym.sym * Sym.sym) * sym_rel -> bool
val fromList : (Sym.sym * Sym.sym) list -> sym_rel
val compare : sym_rel Sort.total_ordering
val subset : sym_rel * sym_rel -> bool
val equal : sym_rel * sym_rel -> bool
val map : ('a -> Sym.sym * Sym.sym) -> 'a Set.set -> sym_rel
val mapFromList : ('a -> Sym.sym * Sym.sym) -> 'a list -> sym_rel
val union : sym_rel * sym_rel -> sym_rel
val genUnion : sym_rel list -> sym_rel
val inter : sym_rel * sym_rel -> sym_rel
val genInter : sym_rel list -> sym_rel
val minus : sym_rel * sym_rel -> sym_rel
val domain : sym_rel -> Sym.sym Set.set
val range : sym_rel -> Sym.sym Set.set
val relationFromTo : sym_rel * Sym.sym Set.set * Sym.sym Set.set -> bool
val relationOn : sym_rel * Sym.sym Set.set -> bool
val apply : sym_rel * Sym.sym Set.set -> Sym.sym Set.set
val reflexive : sym_rel * Sym.sym Set.set -> bool
val symmetric : sym_rel -> bool
val antisymmetric : sym_rel -> bool
val transitive : sym_rel -> bool
val total : sym_rel * Sym.sym Set.set -> bool
val inverse : sym_rel -> sym_rel
val reflexiveClosure : sym_rel * Sym.sym Set.set -> sym_rel
val transitiveClosure : sym_rel -> sym_rel
val reflexiveTransitiveClosure : sym_rel * Sym.sym Set.set -> sym_rel
val symmetricClosure : sym_rel -> sym_rel
val transitiveSymmetricClosure : sym_rel -> sym_rel
val reflexiveTransitiveSymmetricClosure : sym_rel * Sym.sym Set.set -> sym_rel
val compose : sym_rel * sym_rel -> sym_rel
val function : sym_rel -> bool
val functionFromTo : sym_rel * Sym.sym Set.set * Sym.sym Set.set -> bool
val injection : sym_rel -> bool
val bijectionFromTo : sym_rel * Sym.sym Set.set * Sym.sym Set.set -> bool
val bijectionFromAvoiding : sym_rel * Sym.sym Set.set * Sym.sym Set.set -> bool
val bijectionFromSupersetAvoiding : sym_rel * Sym.sym Set.set * Sym.sym Set.set -> bool
val applyFunction : sym_rel -> Sym.sym -> Sym.sym
val restrictFunction : sym_rel * Sym.sym Set.set -> sym_rel
val updateFunction : sym_rel * Sym.sym * Sym.sym -> sym_rel
val mlFunctionToFunction : (Sym.sym -> Sym.sym) * Sym.sym Set.set -> sym_rel
val inputFromLabToks : (int * Lex.tok) list -> sym_rel * (int * Lex.tok) list
val fromString : string -> sym_rel
val input : string -> sym_rel
val toPP : sym_rel -> PP.pp
val toString : sym_rel -> string
val output : string * sym_rel -> unit
val makeBijectionFromAvoiding : Sym.sym Set.set * Sym.sym Set.set -> sym_rel

Description

type sym_rel = (Sym.sym, Sym.sym) Rel.rel
The type of finite relations on Forlan symbols.

comparePair
is Set.comparePair(Sym.compare, Sym.compare).

memb((a, b), rel)
tests whether (a, b) is a member of rel.

fromList xs
returns a relation whose members are the pairs in xs.

compare
is Set.compare comparePair.

subset(rel1, rel2)
tests whether rel1 is a subset of rel2.

equal(rel1, rel2)
tests whether rel1 and rel2 are equal.

map f xs
If xs is compatible with a value cmp of type 'a Sort.total_ordering, then map returns the set of all pairs of symbols f x such that x is a member of xs.

mapFromList f xs
returns the set of all pairs of symbols f x such that x is a member of xs.

union(rel1, rel2)
returns the union of rel1 and rel2.

genUnion rels
returns the generalized union of rels.

inter(rel1, rel2)
returns the intersection of rel1 and rel2.

genInter rels
returns the generalized intersection of rels. Issues an error message if rels is empty.

minus(rel1, rel2)
returns the difference of rel1 and rel2.

domain rel
returns the domain of rel.

range rel
returns the range of rel.

relationFromTo(rel, xs, ys)
tests whether rel is a relation from xs to ys.

relationOn(rel, xs)
tests whether rel is a relation on xs.

apply(rel, xs)
returns the set of all symbols y such that there is a symbol x in xs such that (x, y) is a member of rel.

reflexive(rel, xs)
tests whether rel is reflexive on xs.

symmetric rel
tests whether rel is symmetric.

antisymmetric rel
tests whether rel is antisymmetric.

transitive rel
tests whether rel is transitive.

total(rel, xs)
tests whether rel is total on xs.

inverse rel
returns the inverse of rel.

reflexiveClosure(rel, xs)
returns the reflexive closure of rel with respect to xs.

transitiveClosure rel
returns the transitive closure of rel.

reflexiveTransitiveClosure(rel, xs)
returns the reflexive, transitive closure of rel with respect to xs.

symmetricClosure rel
returns the symmetric closure of rel.

transitiveSymmetricClosure rel
returns the transitive, symmetric closure of rel.

reflexiveTransitiveSymmetricClosure(rel, xs)
returns the reflexive, transitive, symmetric closure of rel with respect to xs.

compose(rel2, rel1)
returns the composition of rel2 and rel1.

function rel
tests whether rel is a function.

functionFromTo(rel, xs, ys)
tests whether rel is a function from xs to ys.

injection rel
tests whether rel is an injection.

bijectionFromTo(rel, xs, ys)
tests whether rel is a bijection from xs to ys.

bijectionFromAvoiding(rel, xs, ys)
tests whether rel is a bijection from xs to a set that is disjoint from ys.

bijectionFromSupersetAvoiding(rel, xs, ys)
tests whether rel is a bijection from a superset of xs to a set that is disjoint from ys.

applyFunction(rel, a)
applies the function rel to a. It issues an error message if rel is not a function, or if a is not in the domain of rel.

restrictFunction(rel, bs)
returns the function that is the restriction of rel to bs. Issues an error message if rel isn't a function, or if bs isn't a subset of the domain of rel.

updateFunction(rel, b, c)
returns the function that is the updating of the function rel to send b to c. Issues an error message if rel isn't a function.

mlFunctionToFunction(f, bs)
returns the function rel whose domain is bs, and where, for all elements b of bs, (b, f b) is a member of rel. Issues an error message if f raises an exception when called on one or more elements of bs.

inputFromLabToks lts
tries to input a relation from lts, consuming as much of lts as possible, and returning the pair of the relation and the rest of lts. Issues an error message if it fails. Will only return the empty relation if lts doesn't begin with a "(" (Lex.OpenPar). If, after reading a pair of symbols, the next element of the labeled token list is "," (Lex.Comma), then inputFromLabToks insists on reading another pair of symbols, even if this results in failure.

fromString s
inputs a relation from s.

input fil
inputs a relation from the file fil.

toPP rel
returns a pretty-printing expression for rel.

toString rel
pretty-prints rel to a string.

output(fil, rel)
pretty-prints rel to file fil.

makeBijectionFromAvoiding(bs, cs)
returns a bijection rel from bs to a set that's disjoint from cs. If the set of all (b, b) such that b is in bs satisfies the disjointness property, it is returned. Otherwise, the set of all (b, <b>) such that b is in bs is tried, and then the set of all (b, <<b>>) such that b is in bs, etc., until a suitable relation is found.

[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.15
Copyright © 2022 Alley Stoughton