diff options
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 142 |
1 files changed, 142 insertions, 0 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr new file mode 100644 index 0000000..f0a0ef7 --- /dev/null +++ b/src/Soat/SecondOrder/Algebra.idr @@ -0,0 +1,142 @@ +module Soat.SecondOrder.Algebra + +import Data.List.Elem + +import Soat.Data.Product +import Soat.Data.Sublist +import Soat.Relation +import Soat.SecondOrder.Signature + +public export +extend : (U : a -> List a -> Type) -> (ctx : List a) -> Pair (List a) a -> Type +extend x ctx ty = x (snd ty) (fst ty ++ ctx) + +public export +extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U)) + -> (ctx : List a) -> IRel (extend U ctx) +extendRel rel ctx (ctx', t) = rel (t, ctx' ++ ctx) + +public export +algebraOver : (sig : Signature) -> (U : sig.T -> List sig.T -> Type) -> Type +algebraOver sig x = (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) + -> extend x ctx ^ op.arity -> x t ctx + +public export +record RawAlgebra (0 sig : Signature) where + constructor MakeRawAlgebra + 0 U : (t : sig.T) -> (ctx : List sig.T) -> Type + rename : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') -> U t ctx -> U t ctx' + sem : sig `algebraOver` U + var : forall t, ctx . (i : Elem t ctx) -> U t ctx + subst : (t : sig.T) -> (ctx : List sig.T) + -> forall ctx' . U t ctx' -> flip U ctx ^ ctx' -> U t ctx + +public export +record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where + constructor MkIsAlgebra + 0 equivalence : IEquivalence (uncurry a.U) rel + -- Congruences + 0 renameCong : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') + -> {tm, tm' : a.U t ctx} -> rel (t, ctx) tm tm' + -> rel (t, ctx') (a.rename t f tm) (a.rename t f tm') + 0 semCong : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) + -> {tms, tms' : extend a.U ctx ^ op.arity} + -> Pointwise (extendRel {U = a.U} rel ctx) tms tms' + -> rel (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms') + 0 substCong : (t : sig.T) -> (ctx : List sig.T) + -> forall ctx' . {tm, tm' : a.U t ctx'} -> rel (t, ctx') tm tm' + -> {tms, tms' : flip a.U ctx ^ ctx'} -> Pointwise (\t => rel (t, ctx)) tms tms' + -> rel (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms') + -- rename is functorial + 0 renameId : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx) + -> rel (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm + 0 renameComp : (t : sig.T) + -> forall ctx, ctx', ctx'' . (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx') + -> (tm : a.U t ctx) + -> rel (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm) + -- sem are natural transformation + 0 semNat : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t) + -> (tms : extend a.U ctx ^ op.arity) + -> rel (t, ctx') + (a.rename t f $ a.sem ctx op tms) + (a.sem ctx' op $ + map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $ + tms) + -- var is natural transformation + 0 varNat : forall t, ctx, ctx' . (f : ctx `Sublist` ctx') -> (i : Elem t ctx) + -> rel (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i) + -- subst is natural transformation + 0 substNat : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') + -> forall ctx'' . (tm : a.U t ctx'') -> (tms : flip a.U ctx ^ ctx'') + -> rel (t, ctx') + (a.rename t f $ a.subst t ctx tm tms) + (a.subst t ctx' tm $ map (\t => a.rename t f) tms) + -- subst is extranatural transformation + 0 substExnat : (t : sig.T) -> (ctx : List sig.T) + -> forall ctx', ctx'' . (f : ctx' `Sublist` ctx'') + -> (tm : a.U t ctx') -> (tms : flip a.U ctx ^ ctx'') + -> rel (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms)) + -- var, subst is a monoid + 0 substComm : (t : sig.T) -> (ctx : List sig.T) + -> forall ctx', ctx'' . (tm : a.U t ctx'') + -> (tms : flip a.U ctx' ^ ctx'') -> (tms' : flip a.U ctx ^ ctx') + -> rel (t, ctx) + (a.subst t ctx (a.subst t ctx' tm tms) tms') + (a.subst t ctx tm $ map (\t, tm => a.subst t ctx tm tms') tms) + 0 substVarL : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx') + -> (tms : flip a.U ctx ^ ctx') + -> rel (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i) + 0 substVarR : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx) + -> rel (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm + -- sem, var and subst are compatible + 0 substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) + -> forall ctx' . (tms : extend a.U ctx' ^ op.arity) -> (tms' : flip a.U ctx ^ ctx') + -> rel (t, ctx) + (a.subst t ctx (a.sem ctx' op tms) tms') + (a.sem ctx op $ + map (\ty, tm => + a.subst (snd ty) (fst ty ++ ctx) tm + (tabulate {is = fst ty} (a.var . Sublist.elemJoinL {ys = ctx}) ++ + map (\t => a.rename t ([] {ys = fst ty} ++ Relation.reflexive {x = ctx})) tms')) $ + tms) + +public export +record Algebra (0 sig : Signature) where + constructor MkAlgebra + raw : RawAlgebra sig + 0 rel : IRel (uncurry raw.U) + algebra : IsAlgebra sig raw rel + +public export +(.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T)) +(.setoid) a = MkISetoid (uncurry a.raw.U) a.rel a.algebra.equivalence + +public export +record IsHomomorphism + {0 sig : Signature} (a, b : Algebra sig) + (f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx) + where + constructor MkIsHomomorphism + 0 cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx} + -> a.rel (t, ctx) tm tm' -> b.rel (t, ctx) (f t ctx tm) (f t ctx tm') + 0 renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx) + -> b.rel (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm) + 0 semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) + -> (tms : extend a.raw.U ctx ^ op.arity) + -> b.rel (t, ctx) + (f t ctx $ a.raw.sem ctx op tms) + (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms) + 0 varHomo : forall t, ctx . (i : Elem t ctx) + -> b.rel (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i) + 0 substHomo : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx') + -> (tms : flip a.raw.U ctx ^ ctx') + -> b.rel (t, ctx) + (f t ctx $ a.raw.subst t ctx tm tms) + (b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms) + +public export +record Homomorphism {0 sig : Signature} (a, b : Algebra sig) + where + constructor MkHomomorphism + f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx + homo : IsHomomorphism a b f |