Safe Haskell	None
Language	GHC2024

Free.Agent.Derivation

Description

endgame-path).

A derivation is a square: the horizontal edge is the agent box (the sender — process dimension); the vertical edges are the ancestry, resolved to strictly-earlier posts (record dimension). With honest ancestry (synthesisPosts, stage 4) the square is /recoverable from the log alone/ — the record projects the derivation, which is the unification claim of the endgame.

Pasting:

horizontal — merging two boxes (both) pastes their squares side by side: the merged box derives the same log as the two boxes in a roster. Oracle: meetLog n [both a b] seed == meetLog n [a, b] seed.
vertical — stacking squares in time: chasing resolved parents from any post walks the pasting back to the roots. Oracle: the chase from the last post of a meeting covers the whole log.

Synopsis

data Derivation a = Derivation {
- dPost :: Post a
- dParents :: [Post a]
}
derivation :: [Post a] -> Post a -> Derivation a
valid :: [Post a] -> Post a -> Bool
chaseLog :: Eq a => [Post a] -> [Post a]

Documentation

data Derivation a Source #

A derivation square: dPost is the output (the square's target); dParents are the resolved vertical sources, in thread order. Dangling ids are an error (the log is expected to be well-formed).

Constructors

Derivation
Fields dPost :: Post a dParents :: [Post a]

Instances

Instances details

Eq a => Eq (Derivation a) Source #
Instance details Defined in Free.Agent.Derivation Methods (==) :: Derivation a -> Derivation a -> Bool # (/=) :: Derivation a -> Derivation a -> Bool #
Show a => Show (Derivation a) Source #
Instance details Defined in Free.Agent.Derivation Methods showsPrec :: Int -> Derivation a -> ShowS # show :: Derivation a -> String # showList :: [Derivation a] -> ShowS #

derivation :: [Post a] -> Post a -> Derivation a Source #

The square of a post against the posts prior to it (oldest first). Each thread edge is a PostId interpreted as a positional index into prior, exactly as in branches.

valid :: [Post a] -> Post a -> Bool Source #

A square is valid when every vertical edge resolves to a strictly-earlier post — no dangling ancestry.

chaseLog :: Eq a => [Post a] -> [Post a] Source #

The posts reachable from the last post by chasing derivations back through the log (vertical pasting made executable). When ancestry is honest and the log is one meeting, the chase covers the whole log.

Posts are compared by value; duplicate posts collapse (bag at the wire, but the chase is a set walk).