Data Types, Checklist 1.1.4. (constraints), Checklist 1.2.2. (algebra of types);
This pattern contains a proposal for denoting constraints such as free term generation, reachability, and constructors with axioms by special abbreviations in data type definitions.
[cf. also the Study Note on Constraints (EA, AH, GR), where a similar proposal is made based on RSL]
Nat: type = [ zero: Zero; succ: (pred: Nat) -> Pos ]
By definition, it is expanded into the following specification:
Nat: type
Zero: type < Nat
Pos: type < Nat
for all n: Nat ·
n in Zero <=> not n in Pos -
disjoint subdomains
n in Nat <=> n in Zero or n in Pos -no
outside junk
zero: Zero
succ: Nat -> Pos -constructors
pred: Pos -> Nat - selector
for all n: Pos · succ (pred n) = n
for all n: Nat · pred (succ n) = n - no
confusion, no junk
for all p: Nat -> Bool ·
p zero /\ (for all n: Nat · p n => p
(succ n)) => for all n: Nat · p n
- induction principle
zero and succ are free constructors and pred is a selector. The condition of disjoint subdomains is expressed by giving distinct (and new) subtype indentifiers.
| BinNat: type = [ | zero: EvenNat | |||||||
| times2: (div2even: BinNat) -> EvenNat | ||||||||
| times2plus1: (div2odd: BinNat) -> OddNat ] | ||||||||
By definition, it is expanded into the following specification:
| BinNat: type | ||||||||
| EvenNat: type < BinNat | ||||||||
| OddNat: type < BinNat | ||||||||
| for all n: BinNat · | ||||||||
| n in EvenNat <=> not n in OddNat - disjoint subdomains | ||||||||
| n in BinNat <=> n in EvenNat or n in OddNat - no outside junk | ||||||||
| zero: EvenNat | ||||||||
| times2: BinNat -> EvenNat | ||||||||
| times2plus1: BinNat -> OddNat - constructors | ||||||||
| div2even: EvenNat -> BinNat | ||||||||
| div2odd: OddNat -> BinNat - selectors | ||||||||
| for all n: EvenNat · times2 (div2even n) = n | ||||||||
| for all n: OddNat · times2plus1 (div2odd n) = n | ||||||||
| for all n: BinNat · | div2even (times2 n) = n | |||||||
| div2odd (times2plus1 n) = n | ||||||||
| - plus some induction principle | ||||||||
Extra axioms for the example:
for all n: EvenNat · (div2even zero) = zero
If the selectors are also omitted in the definition, then reachability is still retained, but equations are possible for each constructor.
The above transformations (for which only examples are given) can be defined in a structured, stepwise manner, separating reachability, induction, and disjointness. Also, explicit operators for disjoint and non-disjoint union could be defined.
Therefore:
Achieve constraints such as free term generation, reachability, etc. by special variations of data type definitions rather than with additional constraint operators.