diff options
Diffstat (limited to 'src/algebra')
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 43 | ||||
| -rw-r--r-- | src/algebra/catdef.spad.pamphlet | 11 |
2 files changed, 38 insertions, 16 deletions
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index e3c6ab7f..dcdf0562 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -611,11 +611,11 @@ Bits(): Exports == Implementation where )abbrev domain KTVLOGIC KleeneTrivalentLogic ++ Author: Gabriel Dos Reis ++ Date Created: September 20, 2008 -++ Date Last Modified: May 27, 2009 +++ Date Last Modified: January 14, 2012 ++ Description: ++ This domain implements Kleene's 3-valued propositional logic. KleeneTrivalentLogic(): Public == Private where - Public == PropositionalLogic with + Public == Join(PropositionalLogic,Finite) with unknown: % ++ the indefinite `unknown' case: (%,[| false |]) -> Boolean ++ x case false holds if the value of `x' is `false' @@ -623,54 +623,69 @@ KleeneTrivalentLogic(): Public == Private where ++ x case unknown holds if the value of `x' is `unknown' case: (%,[| true |]) -> Boolean ++ s case true holds if the value of `x' is `true'. - Private == add - Rep == Byte -- We need only 3 bits, in fact. - false == per(0::Byte) - unknown == per(1::Byte) - true == per(2::Byte) + Private == Maybe Boolean add + false == per just(false@Boolean) + unknown == per nothing + true == per just(true@Boolean) x = y == rep x = rep y x case true == x = true@% x case false == x = false@% x case unknown == x = unknown + not x == x case false => true x case unknown => unknown false + x and y == x case false => false x case unknown => y case false => false unknown y + x or y == x case false => y x case true => x y case true => y unknown + implies(x,y) == x case false => true x case true => y y case true => true unknown + equiv(x,y) == x case unknown => x x case true => y not y + coerce(x: %): OutputForm == - x case true => outputForm 'true - x case false => outputForm 'false - outputForm 'unknown + case rep x is + y@Boolean => y::OutputForm + otherwise => outputForm 'unknown + + size() == 3 + + index n == + n > 3 => error "index: argument out of bound" + n = 1 => false + n = 2 => unknown + true + + lookup x == + x = false => 1 + x = unknown => 2 + 3 @ - - - \section{License} <<license>>= --Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd. --All rights reserved. ---Copyright (C) 2007-2010, Gabriel Dos Reis. +--Copyright (C) 2007-2012, Gabriel Dos Reis. --All rights reserved. -- --Redistribution and use in source and binary forms, with or without diff --git a/src/algebra/catdef.spad.pamphlet b/src/algebra/catdef.spad.pamphlet index e546bb01..6fae2576 100644 --- a/src/algebra/catdef.spad.pamphlet +++ b/src/algebra/catdef.spad.pamphlet @@ -915,7 +915,6 @@ Field(): Category == Join(EuclideanDomain,UniqueFactorizationDomain, ++ \spad{index(lookup(s)) = s} Finite(): Category == SetCategory with - --operations size: () -> NonNegativeInteger ++ size() returns the number of elements in the set. index: PositiveInteger -> % @@ -928,7 +927,15 @@ Finite(): Category == SetCategory with ++ \spad{x = index lookup x}. random: () -> % ++ random() returns a random element from the set. - + add + --FIXME: Tthe only purpose of this local function is to bring + --FIXME: the compiler to admission that the successor of a + --FIXME: nonnegative integer has positive value. + --FIXME: Take it out when the its logic is sufficiently advanced. + succ(x: NonNegativeInteger): PositiveInteger == + (1 + x) : PositiveInteger + random() == + index succ random(size())$NonNegativeInteger @ \section{category FLINEXP FullyLinearlyExplicitRingOver} <<category FLINEXP FullyLinearlyExplicitRingOver>>= |