Multiplicative SemiGroup with Unit

Syntax

syntax mulexpr
{
  //$ multiplication: non-associative.
  x[sproduct_pri] := x[>sproduct_pri] ("*" x[>sproduct_pri])+ =>#
    "(chain 'ast_product _1 _2)" note "mul";
}

Semantics

class FloatMultSemi1[t] {
  inherit Eq[t];
  proc muleq(px:&t, y:t) { *= (px,y); }
  fun mul(x:t, y:t) => x * y;
  fun sqr(x:t) => x * x;
  fun cube(x:t) => x * x * x;
  virtual fun one: unit -> t;
  virtual fun * : t * t -> t;
  virtual proc *= (px:&t, y:t) { px <- *px * y; }
  //reduce id (x:t): x*one() => x;
  //reduce id (x:t): one()*x => x;
}

class MultSemi1[t] {
  inherit FloatMultSemi1[t];
  axiom assoc (x:t,y:t,z:t): (x * y) * z == x * (y * z);
  //reduce cancel (x:t,y:t,z:t): x * z ==  y * z => x == y;
}

Description

A multiplicative semigroup with unit is an approximate multiplicative semigroup with unit and associativity and satisfies the cancellation law.