Previous Up Next

Interface for module Mtt

The module contains the definitions of transduction, iteration, and quotienting of (tree) transducers. For a final version, the interface should be tightened (most is exported currently for debugging and diagnosis).


typeqequations=(qstarindexנqstarindex)list(∗ subset of Q Q ∗)

The type twopartition is nothing else than a pair of lists. It will be used here to represent the partition, more specifically the partition of finite relations, i.e., pairs of elements, but twopartition is given here parametric in the type.

The type d_partition is a “refinement” and specialisation of the generic partition type. Since the set, whose relation is being partitioned —in the bisimulation calculation— will change over time, the last component keeps track of the set (as list).


typeαtwopartition=(αlist)נ(αlist)
typed_partition=((qstarindexנqstarindex)twopartitionqstarindexlist

valqstarindex_as_qstarterm:qstarindexqindextermqindexterm

valis_puretermtermbool
valis_lhs_term_startermbool
valis_rhs_term_startermbool

valtransducemtt→αterm→(αterm)list

valextract_linear_term_and_n:qindexterm→(qindextermint

valone_fbisimstep:
((qindexrule)list)→ssignatureqequations
d_partitiond_partition

valfbisimulation_states:
((qindexrule)list)→ssignatureqequations
d_partitiond_partition

valfbisimulation_states_fromscratch:
((qindexrule)list)→ssignatureqequations
(qstarindexlist)→d_partition

valqstar_and_symbol_notin_rel:
(qstarindexנqstarindex)list→((qstarindexנsymbol)נ(qstarindexנsymbol))→bool

valpost_on_symbol:(qindexrule)list→(symbolנint)→qstarindex→(qindexterm)list

valpre_on_rhs:(qindexrule)list→(qindexterm)→(qindexterm)list

valbuild_statecombinations:
qstarindexנqstarindex
(qstarindexlist)→
int
((qstarindexlist)list)נ((qstarindexlist)list)

valbuild_relevant_rhs:
(qstarindexנqstarindex)→
(qstarindexlist)→
qindexterm
(qindextermנqindexterm)list

valbuild_relevant_rhss:
(qstarindexנqstarindex)→
(qstarindexlist)→
(qindexterm)list
(qindextermנqindexterm)list

valone_pbisimstep:
((qindexrule)list)→ssignatureqequations
d_partitiond_partition

valpbisimulation_states:
((qindexrule)list)→ssignatureqequations
d_partitiond_partition

valbuild_fstart_qstars_eq:qindexlistintqstarindexlist
valbuild_fstart_qstars_leq:qindexlistintqstarindexlist

valbuild_startpartition:qstarindexlistd_partition

valstarterm_of_term:qindextermqstarindexterm
valnormalise_qstarterm:qequationsqstarindextermqstarindexterm

valglean_transitions:ssignatureqstarindex→((qindexrule)list)→
((qstarindexrule)list)

valglean_T:ssignature→((qindexrule)list)→qequations→(qstarindexlist)→(qstarindexlist)
→(((qstarindexrule)list)נ(qstarindexlist))

valmerge_p_f:(qequationsנqequations)→qequations

valiterate_T_static:ssignatureqindexlist→((qindexrule)list)
→((qstarindexrule)list)
qequations
d_partition
int
→((qstarindexrule)list)

valiterate_T:ssignatureqindexlist→(qindexrulelist)
d_partition
int
→(qequations)נ(qstarindexrulelist)→(qequations)נ(qstarindexrulelist)

valiterate_T_rules:ssignatureqindexlist→(qindexrulelist)
d_partition
int
→(qequations)נ(qstarindexrulelist)→(qequations)נ(qstarindexrulelist)

valstar:qindexmttqindexmtt


Previous Up Next