Égalité

VIRTUAL TYPE equality {t: type}
  IMPORT Deterministic FROM function{any, any}
  EXPORT Reflexive Symmetric Transitive Identity_relation Eternal

  MESSAGE equal(x y: t)  -- Weak equality, can be computed.
    REPLY(b: boolean)
    WHERE Reflexive(equal), Symmetric(equal), Transitive(equal),
      Identity_relation(equal),
        -- Equals can be substituted for equals.
      Eternal(equal)
        -- If two objects are equal,
        -- they are equal in all states.

  MESSAGE not_equal(x y: t)
    REPLY(b: boolean) WHERE b <=> ~equal(x, y)

  CONCEPT "="(x y: t) VALUE(b: boolean)
      -- Strong logical equality, not computable.
    WHERE Strongly_reflexive("="),
        -- (! = !) = true but equal(!, !) = !.
      ALL(x y: t :: (x = y) <=> equal(x, y))
        -- "=" is the same as "equal" for all well defined
        -- data values.

  CONCEPT "~="(x y: t) VALUE(b: boolean)
    -- Strong logical inequality, not computable.
    WHERE b <=> ~(x = y)

  CONCEPT Reflexive(f: function{t, t, boolean}) VALUE(b: boolean)
    WHERE b <=> ALL(x: t :: f(x, x))
      -- x ranges over well defined values of type t.

  CONCEPT Strongly_reflexive(f: function{t, t, boolean})
    VALUE(b: boolean)
    WHERE b <=> Reflexive(f) & f(!, !)
      -- Reflexive also for the undefined element "!".

  CONCEPT Symmetric(f: function{t, t, boolean}) VALUE(b: boolean)
    WHERE b <=> ALL(x y: t :: f(x, y) => f(y, x))

  CONCEPT Transitive(f: function{t, t, boolean})
    VALUE(b: boolean)
    WHERE b <=> ALL(x y z: t :: f(x, y) & f(y, z) => f(x, z))

  CONCEPT Identity_relation(f: function{t, t, boolean})
    VALUE(b: boolean)
    WHERE b <=> 
      ALL(a b: t, ts1 ts2: sequence{type}, s1: ts1, s2: ts2,
          range: type, g: function{$ts1, t, $ts2, range}
          SUCH THAT Deterministic(g) ::
          f(a, b) => g($s1, a, $s2) = g($s1, b, $s2) )
            -- If f(x, y) there is no way
            -- to distinguish x from y.
            -- This means x and y are identical,
            -- so you can substitute x for y.

  CONCEPT Eternal(f: function{t, t, boolean}) VALUE(b: boolean)
    WHERE b <=> ALL(a b: t :: f(a, b) => always(f(a, b)))
      -- This means the relation f cannot be affected by
      -- state changes.
END