monoid.mlw 1.87 KB
Newer Older
1
2
3
4
5
6
7

(** {1 Abstract monoids}
    Author: Martin Clochard *)

(** {2 Abstract logic monoid} *)

module Monoid
8

9
10
  (** Elements of the monoid. *)
  type t
11

12
13
14
15
  (** Neutral element. *)
  constant zero : t
  (** Composition law. *)
  function op (a b:t) : t
16

17
18
19
  (** Monoid properties. *)
  axiom assoc : forall a b c:t. op a (op b c) = op (op a b) c
  axiom neutral : forall x:t. op x zero = x = op zero x
20

21
22
23
24
end

(** {2 Abstract monoid with aggregation} *)
module MonoidSum
25

26
  use import seq.Seq
27
  clone import Monoid as M with axiom .
28

29
30
31
32
33
34
  function agg (f:'a -> t) (s:seq 'a) : t
  axiom agg_empty : forall f:'a -> t. agg f empty = zero
  axiom agg_sing : forall f,s:seq 'a.
    length s = 1 -> agg f s = f s[0]
  axiom agg_cat : forall f,s1 s2:seq 'a.
    agg f (s1 ++ s2) = op (agg f s1) (agg f s2)
35

36
37
end

38
(** {2 Definition of aggregation (refinement of MonoidSum} *)
39
module MonoidSumDef
40
41
42
43
44

  use import seq.Seq
  use import seq.FreeMonoid

  (* TODO: do that refinement correctly ! *)
45
  clone import Monoid as M with axiom .
46
47
48

  let rec ghost function agg (f:'a -> t) (s:seq 'a) : M.t
    variant { length s }
49
  = if length s = 0 then zero else op (f s[0]) (agg f s[1 ..])
50
51
52
53
54
55

  lemma agg_sing_core : forall s:seq 'a. length s = 1 -> s[1 ..] == empty

  let rec lemma agg_cat (f:'a -> t) (s1 s2:seq 'a)
    ensures { agg f (s1++s2) = op (agg f s1) (agg f s2) }
    variant { length s1 }
56
  = if length s1 <> 0 then let s3 = s1[1 ..] in agg_cat f s3 s2
57
58
59
60
61
62
63
64
65
66

  clone MonoidSum as MS with type M.t = M.t,
    constant M.zero = M.zero,
    function M.op = M.op,
    goal M.assoc,
    goal M.neutral,
    function agg = agg,
    goal agg_empty,
    goal agg_sing,
    goal agg_cat
67

68
69
70
71
end

(** {2 Computable monoid} *)
module ComputableMonoid
72

73
  clone export Monoid with axiom .
74

75
76
  (** Abstract routines computing operations in the monoid. *)
  val zero () : t ensures { result = zero }
77

78
  val op (a b:t) : t ensures { result = op a b }
79

80
end