Prev Up Next
Go backward to 3.1 Requirements to the semantics
Go up to 3 Semantics
Go forward to 3.3 Well-typed terms and formulas

3.2 Extensions of the subsort relation

Given a set S of basic sorts and a subsort relation (preorder) < on S, and let S -> denote the set of types generated by S.

Let < -> be the least preorder on S -> satisfying the following rules:

  1. s < -> s', if s < s'
  2. w -> s < -> w -> s', if s < -> s'
  3. w +s < -> w +s', if s < -> s'
  4. w +s < -> w -> s
Let < => be the least preorder on S -> satisfying the following rules:
  1. s < => s', if s < s'
  2. s1...sn -> s < => s1'...sn' -> s', if si' < => si for i = 1, ..., n, and s < => s'
  3. s1...sn +s < => s1'...sn' +s', if si' < => si for i = 1, ..., n, and s < => s'
  4. w +s < -> w -> s
Note that < -> is a suborder of < => .
CoFI Note: L-2 --Version 1.0-- 10 April 1997.
Comments to ah@it.dtu.dk

Prev Up Next