%% predefined universe containing all types,

%% superclass of all other classes

class Type

var s,t : Type

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% invisible type "Unit" for formulae

type Unit: Type %% flat cpo with bottom

%% type aliases

type Pred __ (t: -Type) := t ->? Unit

type ? __ (t:Type) := Unit ->? t

pred true, false : Unit

preds __/\__, __\/__, __=>__, __if__,__<=>__ : Unit * Unit

pred not : Unit

pred __=__ : s * s %% =e=

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% (builtin) type (constructors)

type __->?__ : -Type -> +Type -> Type

%% nested pairs are different from n-tupels (n > 2)

type __*__ : +Type -> +Type -> Type

type __*__*__ : +Type -> +Type -> +Type -> Type

%% ...

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% "pred p args = e" abbreviates "op p args :? unit = e"

%% CASL requires "<=>" for pred-defn and disallows "()" as result

op def, tt : Pred s

var x : s

program def = \x: s . () %% def is also total (identical to tt)

program tt = \x: s . () %% tt is total "op tt(x: s): unit = ()"

program __und__ (x, y: Unit) : Unit = ()

%% total function type

type __->__ : -Type -> +Type -> Type

type __->__ < __ ->? __

. __ in s -> t = \f: s ->? t . all(\x:s. def f(x))

%% total functions

op __res__ (x: s; y: t) : s = x

op fst (x: s; y: t) : s = x

program snd (x: s, y: t) : t = y

%% trivial because its the strict function property

. (\ (x:s, y:t). def (x res y)) = (\ (x:s, y:t). (def y) und (def x))

. fst = (__ res__)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Internal Logic

pred eq : s * s

. (\x: s. eq(x, x)) = tt

. (\(x, y:s). x res eq(x,y)) = (\(x, y:s). y res eq(x,y))

%% then %def

%% notation "\ ." abbreviates "\bla:unit."

%% where "bla" is never used, but only "()" instead

%% for type inference

%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"

type s < ?s

program all (p: Pred(s)) : Pred Unit = eq(p, tt)

%% the cast from ?s to s is still done manually here (for the strict "und")

program And (x, y: Pred Unit) : Pred Unit = t1() und t2()

%% use "And" instead of "und" to avoid cast from "?unit" to "unit"

program __impl__ (x, y: Pred Unit) : Pred Unit = eq(x, x And y)

program __or__ (x, y: Pred Unit) : Pred Unit = all(\r: Pred Unit.

((x impl r) und (y impl r)) impl r)

program ex (p: Pred(s)) : Pred Unit = all(\r: Pred Unit.

all(\x:s. p(x) impl r) impl r)

program ff () : Pred Unit = all(\r: Pred Unit. r())

program neg (r: Pred Unit) : Pred Unit = r impl ff

%% the type instance for the first "eq" should be "?t"

%% this is explicitely enforced by "\ .f(x)"

. all(\(f,g): s->?t. all(\x:s. eq(\ . f(x), g(x)) impl eq(f, g)))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"

type nat

class Cpo < Type

{

var c : Cpo

pred __<<=__ : c * c

. all(\x: c. x <<= x) %(reflexive)%

. all(\(x,y,z: c). ((x <<= y) und (y <<= z)) impl x <<= z) %(transitive)%

. all(\(x,y,z: c). ((x <<= y) und (y <<= x)) impl eq(x,y)) %(antisymmetric)%

pred isChain (s: nat -> c) <=> all(\n:nat. s(n) <<= s(Suc(n)))

pred isBound (x: c; s: nat -> c) <=> all(\n:nat. s(n) <<= x)

op sup : (nat -> c) ->? c

. all(\s: nat -> c. def(sup s) impl

(isBound(sup s, s) und all(\x:c. isBound(x, s) impl sup(s) <<= x)))

%(sup is minimally bound)%

. all(\s:nat -> c. isChain(s) impl def(sup(s))) %(sup exists)%

}

class Pcpo < Cpo

{

var p : Pcpo

op bottom : p

. all(\x : p. bottom <<= x)

}

class instance Flatcpo < Cpo

{

var f : Flatcpo

program __<<=[f]__ = eq

}

var c, d: Cpo

type instance __*__ : +Cpo -> +Cpo -> Cpo

var x1,x2 : c; y1, y2 : d

program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)

type instance __*__ : +Pcpo -> +Pcpo -> Pcpo

type Unit : Pcpo

%% Pcont

type instance __-->?__ : -Cpo -> +Cpo -> Pcpo

type __-->?__ < __->?__

. __ in c -->? d = \f : c ->? d .

all(\(x,y: c). (def (f x) und x <<= y) impl def (f y)) und

all(\s: nat -> c. (isChain(s) und def f(sup(s))) impl

ex(\m:nat. def f(s(m)) und

eq(sup(\n:nat.!f(s(n+m))), f(sup(s)))))

program f <<=[c -->? d] g = all(\x:c. def (f x) impl f(x) <<= g(x))

%% Tcont

type instance __-->__ : -Cpo -> +Cpo -> Cpo

type __-->__ < __-->?__

. __ in c --> d = \f : c -->? d . all(\x:c. def f(x))

var f, g : c --> d

program f <<= g = f <<=[c -->? d] g

type instance __-->__ : -Cpo -> +Pcpo -> Pcpo

fun Y : (p --> p) --> p

. all(\f: p -->? p . eq(f(Y(f)), Y(f)) und

all(\x:p . eq(f(x), x) impl Y(f) <<= x))

var f : p --> p; x : p

. f(Y(f)) = Y(f)

. f(x) = x => Y(f) <<= x

op undefined : c --> p = Y((\x': c --> p . x') as (c --> p) --> c --> p)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% user stuff

free type bool ::= true | false

type bool : Flatcpo

type nat : Flatcpo