9.49 Magma

Initialisations

x:Symbol :='x

\[\]

x

_{Type: Symbol}

y:Symbol :='y

\[\]

y

_{Type: Symbol}

z:Symbol :='z

\[\]

z

_{Type: Symbol}

word := OrderedFreeMonoid(Symbol)

\[\]

OrderedFreeMonoidSymbol

_{Type: Domain}

tree := Magma(Symbol)

\[\]

MagmaSymbol

_{Type: Domain}

Let’s make some trees

a:tree := x*x

\[\]

[x,x]

_{Type: Magma Symbol}

b:tree := y*y

\[\]

[y,y]

_{Type: Magma Symbol}

c:tree := a*b

\[\]

[[x,x],[y,y]]

_{Type: Magma Symbol}

Query the trees

left c

\[\]

[x,x]

_{Type: Magma Symbol}

right c

\[\]

[y,y]

_{Type: Magma Symbol}

length c

\[\]

4

_{Type: PositiveInteger}

Coerce to the monoid

c::word

\[\]

x2y2

_{Type: OrderedFreeMonoid Symbol}

Check ordering

a < b

\[\]

true

_{Type: Boolean}

a < c

\[\]

true

_{Type: Boolean}

b < c

\[\]

true

_{Type: Boolean}

Navigate the tree

first c

\[\]

x

_{Type: Symbol}

rest c

\[\]

[x,[y,y]]

_{Type: Magma Symbol}

rest rest c

\[\]

[y,y]

_{Type: Magma Symbol}

Check ordering

ax:tree := a*x

\[\]

[[x,x],x]

_{Type: Magma Symbol}

xa:tree := x*a

\[\]

[x,[x,x]]

_{Type: Magma Symbol}

xa < ax

\[\]

true

_{Type: Boolean}

lexico(xa,ax)

\[\]

false

_{Type: Boolean}