- type TIDEq = (TID, TID)
- type TIDRoleEq = (TID, Role)
- type RoleEq = (Role, Role)
- type AgentEqRHS = Either AgentId AVar
- type AgentEq = (AgentId, AgentEqRHS)
- type AVarEq = (AVar, AVar)
- type MVarEq = (MVar, Message)
- type MsgEq = (Message, Message)
- data AnyEq
- agentEqToMsgEq :: AgentEq -> MsgEq
- mvarEqToMsgEq :: MVarEq -> MsgEq
- data Equalities
- empty :: Equalities
- solve :: Monad m => [AnyEq] -> Equalities -> m Equalities
- trimTIDEqs :: Equalities -> ([TID], Equalities)
- trimAgentEqs :: Equalities -> ([AgentId], Equalities)
- getTIDEqs :: Equalities -> [TIDEq]
- getTIDRoleEqs :: Equalities -> [TIDRoleEq]
- getAgentEqs :: Equalities -> [AgentEq]
- getAVarEqs :: Equalities -> [AVarEq]
- getMVarEqs :: Equalities -> [MVarEq]
- getPostEqs :: Equalities -> [MsgEq]
- toAnyEqs :: Equalities -> [AnyEq]
- anyEqTIDs :: AnyEq -> [TID]
- substTID :: Equalities -> TID -> TID
- substLocalId :: Equalities -> LocalId -> LocalId
- substAVar :: Equalities -> AVar -> AVar
- substMVar :: Equalities -> MVar -> Message
- substAgentId :: Equalities -> AgentId -> AgentEqRHS
- substAgentEqRHS :: Equalities -> AgentEqRHS -> AgentEqRHS
- substMsg :: Equalities -> Message -> Message
- substAnyEq :: Equalities -> AnyEq -> AnyEq
- threadRole :: TID -> Equalities -> Maybe Role
- maxMappedTID :: Equalities -> Maybe TID
- maxMappedAgentId :: Equalities -> Maybe AgentId
- reflexive :: AnyEq -> Bool
- null :: Equalities -> Bool
- newtype Mapping = Mapping {}
- emptyMapping :: Mapping
- mkMapping :: Map TID TID -> Map AgentId AgentId -> Mapping
- addTIDMapping :: TID -> TID -> Mapping -> Mapping
- addAgentIdMapping :: AgentId -> AgentId -> Mapping -> Mapping
- addTIDRoleMapping :: TID -> Role -> Mapping -> Mapping
- deleteTIDMapping :: TID -> Mapping -> Mapping
- deleteAgentIdMapping :: AgentId -> Mapping -> Mapping
- sptAnyEq :: AnyEq -> Doc

# Single Equalities

Equalities over thread identifers.

Logically these are equalities between logical thread identifier variables.

type AgentEqRHS = Either AgentId AVarSource

type AgentEq = (AgentId, AgentEqRHS)Source

type AVarEq = (AVar, AVar)Source

Equalities between different agent variables.

We do not have to reason about equalities between an agent variable and some other message because our semantics guarantees that agent variables are only instantiated with agent names. Hence, they can only be equal to other agent variables or message variables. In the latter case, we store the equality the other way round; assigning the agent variable to the message variable.

Some representable equality.

agentEqToMsgEq :: AgentEq -> MsgEqSource

Convert an agent equality to a message equality.

mvarEqToMsgEq :: MVarEq -> MsgEqSource

Convert a message variable equallity to a message equality.

# Compound Equalities

data Equalities Source

A conjunction of equality facts.

Invariants for a value `eqs = Equalities tideqs roleeqs avareqs mvareqs agnteqs`

:

- Domain and range normalized with respect to equalities. Note that this implies substitution must always consider TID substitution first.

forall tid : ran(tideqs). substTID eqs tid = tid forall tid : dom(roleeqs). substTID eqs tid = tid forall (lid, lid') : avareqs. substLocalId eqs lid = lid & substAVar eqs lid' = lid' forall (lid, m) : mvareqs. substLocalId eqs lid = lid & substMsg eqs m = m

TODO: Complete properties for Agent ID's

forall aid : dom(agnteqs). substAgentId eqs aid = Just (Left aid) forall : dom(agnteqs). substAgentId eqs aid = Just (Left aid)

- Origin always greater than image for symmetric eqs.

forall (tid, tid') : tideqs. tid > tid' forall (lid, lid') : avareqs. lid > lid'

- Range of message variable equalities normalized with respect to key inversion.

forall m : ran(mvareqs). normMsg m = m

- All thread identifiers are in the domain of roleeqs.
- All agent identifiers are in the domain of agnteqs.
- No cycles.

## Construction

Empty equality premises.

solve :: Monad m => [AnyEq] -> Equalities -> m EqualitiesSource

Solve a list of unification equations.

The unification is performed modulo key inversion and thread identifier equalities. Additional thread identifier equalities may result from equalities over fresh messages. Bidirectional keys are handled by delaying their solution until only one solution is possible.

:: Equalities | |

-> ([TID], Equalities) | Dropped TIDs plus updated equalities |

Remove the thread identifier equalities. This is logically safe iff there is no fact outside the equalities that still refers to the dropped thread identifiers.

:: Equalities | |

-> ([AgentId], Equalities) | Dropped AgentIds plus updated equalities |

Remove the agent identifiers equalities. This is logically safe iff there is no fact outside the equalities that still refers to the dropped agent identifiers.

## Destruction

getTIDEqs :: Equalities -> [TIDEq]Source

The list of thread identifier equalities.

getTIDRoleEqs :: Equalities -> [TIDRoleEq]Source

The list of role equalities.

getAgentEqs :: Equalities -> [AgentEq]Source

The list of agent variable equalities.

getAVarEqs :: Equalities -> [AVarEq]Source

The list of agent variable equalities.

getMVarEqs :: Equalities -> [MVarEq]Source

The list of message variable equalities.

getPostEqs :: Equalities -> [MsgEq]Source

The list of postponed message equalities.

toAnyEqs :: Equalities -> [AnyEq]Source

Convert a set of equalities to a list of equalities.

POST: Order of equalities equal to order in result of `toLists`

.

## Substitution

substTID :: Equalities -> TID -> TIDSource

Substitute a thread identifier according to thread identifier equalities.

substLocalId :: Equalities -> LocalId -> LocalIdSource

Substitute a local identifier according to thread identifier equalities.

substAVar :: Equalities -> AVar -> AVarSource

Substitute a local identifier belonging to an agent variable.

substMVar :: Equalities -> MVar -> MessageSource

Substitute a local identifier belonging to a message variable.

substAgentId :: Equalities -> AgentId -> AgentEqRHSSource

Substitute an agent id representing an arbitrary agent name.

substAgentEqRHS :: Equalities -> AgentEqRHS -> AgentEqRHSSource

Substitute the right-hand-side of an agent id equality.

substMsg :: Equalities -> Message -> MessageSource

Substitute message constituents according to equalities.

POST: Message normalized w.r.t. `normMsg`

.

substAnyEq :: Equalities -> AnyEq -> AnyEqSource

Substitute both sides of a representable equality.

## Additional Queries

threadRole :: TID -> Equalities -> Maybe RoleSource

Retrieve the role of a thread.

maxMappedTID :: Equalities -> Maybe TIDSource

The maximal mapped thread identifier.

maxMappedAgentId :: Equalities -> Maybe AgentIdSource

The maximal mapped agent identifier.

null :: Equalities -> BoolSource

True if no equalities are present.

# Mapping Logical Variables

An empty mapping.

mkMapping :: Map TID TID -> Map AgentId AgentId -> MappingSource

A mapping of logical variables and the corresponding substitution can be represented as an abstract Equalities value. However, it violates the invariant that the domain of the equalities must be invariant under substitution. This is OK, as domain and range of a mapping are from different logical contexts.

addTIDMapping :: TID -> TID -> Mapping -> MappingSource

Add a mapping from one thread identifier to another one, possibly overriding an existing mapping.

addAgentIdMapping :: AgentId -> AgentId -> Mapping -> MappingSource

Add a mapping from one thread identifier to another one, possibly overriding an existing mapping.

addTIDRoleMapping :: TID -> Role -> Mapping -> MappingSource

Add a mapping from one thread identifier to an other role, possibly overriding an existing mapping.

deleteTIDMapping :: TID -> Mapping -> MappingSource

Delete the mapping of the given thread identifier.

deleteAgentIdMapping :: AgentId -> Mapping -> MappingSource

Delete the mapping of the given agent identifier.