%% 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 __ : Type -> Type := \ 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 s -> t < s ->? t

. __ 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 c -->? d < c ->? d

. __ 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 c --> d < c -->? d

. __ 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

op 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))

op undefined : c -->? p = Y(\x: c -->? p .! x)

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

%% user stuff

free type bool ::= true | false

type bool : Flatcpo

type nat : Flatcpo