Theory: stateTransformer

Parents

• pair

Types

Constants

• JOIN  :('a -> ('a -> 'b # 'a) # 'a) -> 'a -> 'b # 'a
• MMAP  :('c -> 'b) -> ('a -> 'c # 'a) -> 'a -> 'b # 'a
• UNIT  :'b -> 'a -> 'b # 'a
• BIND  :('a -> 'b # 'a) -> ('b -> 'a -> 'c # 'a) -> 'a -> 'c # 'a

Definitions

BIND_DEF

|- !g f. BIND g f = UNCURRY f o g

JOIN_DEF

|- !z. JOIN z = BIND z I

MMAP_DEF

|- !f m. MMAP f m = BIND m (UNIT o f)

UNIT_DEF

|- !x. UNIT x = (\s. (x,s))

Theorems

BIND_ASSOC

|- !k m n. BIND k (\a. BIND (m a) n) = BIND (BIND k m) n

BIND_LEFT_UNIT

|- !k x. BIND (UNIT x) k = k x

BIND_RIGHT_UNIT

|- !k. BIND k UNIT = k

JOIN_MAP

|- !k m. BIND k m = JOIN (MMAP m k)

JOIN_MAP_JOIN

|- JOIN o MMAP JOIN = JOIN o JOIN

JOIN_MMAP_UNIT

|- JOIN o MMAP UNIT = I

JOIN_UNIT

|- JOIN o UNIT = I

MMAP_COMP

|- !f g. MMAP (f o g) = MMAP f o MMAP g

MMAP_ID

|- MMAP I = I

MMAP_JOIN

|- !f. MMAP f o JOIN = JOIN o MMAP (MMAP f)

MMAP_UNIT

|- !f. MMAP f o UNIT = UNIT o f

UNIT_UNCURRY

|- !s. UNCURRY UNIT s = s