diff options
Diffstat (limited to 'src/algebra')
| -rw-r--r-- | src/algebra/Makefile.in | 8 | ||||
| -rw-r--r-- | src/algebra/Makefile.pamphlet | 8 | ||||
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 230 | ||||
| -rw-r--r-- | src/algebra/exposed.lsp.pamphlet | 3 | ||||
| -rw-r--r-- | src/algebra/mkrecord.spad.pamphlet | 57 |
5 files changed, 296 insertions, 10 deletions
diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in index 7fe8dd8f..4a806873 100644 --- a/src/algebra/Makefile.in +++ b/src/algebra/Makefile.in @@ -391,7 +391,7 @@ axiom_algebra_layer_1 = \ PATAB.o PLOT1.o PPCURVE.o PSCURVE.o \ REAL.o RESLATC.o RETRACT.o RETRACT-.o \ SEGBIND2.o SEGCAT.o STREAM1.o STREAM2.o \ - STREAM3.o + STREAM3.o axiom_algebra_layer_1_nrlibs = \ $(axiom_algebra_layer_1:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) @@ -433,7 +433,7 @@ axiom_algebra_layer_4 = \ REPDB.o RFDIST.o RIDIST.o RMODULE.o \ SEXCAT.o SGROUP.o SGROUP-.o SPACEC.o \ SPLNODE.o STEP.o SUCH.o TEX1.o \ - UDVO.o YSTREAM.o + UDVO.o YSTREAM.o PAIR.o axiom_algebra_layer_4_nrlibs = \ $(axiom_algebra_layer_4:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) @@ -453,7 +453,7 @@ axiom_algebra_layer_5 = \ ODVAR.o OPQUERY.o ORDFIN.o ORDMON.o \ PATMATCH.o PERMCAT.o PDRING.o PDRING-.o \ SDVAR.o SUP2.o TRIGCAT.o TRIGCAT-.o \ - ULS2.o UP2.o + ULS2.o UP2.o axiom_algebra_layer_5_nrlibs = \ $(axiom_algebra_layer_5:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) @@ -732,7 +732,7 @@ axiom_algebra_layer_19 = \ SET.o SPECOUT.o SQMATRIX.o SWITCH.o \ SYMS.o SYMTAB.o SYSSOLP.o UTSCAT.o \ UTSCAT-.o VARIABLE.o WFFINTBS.o SPADPRSR.o \ - PARSER.o + PARSER.o PROPFRML.o axiom_algebra_layer_19_nrlibs = \ $(axiom_algebra_layer_19:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet index 70a3f05c..2e8dc2be 100644 --- a/src/algebra/Makefile.pamphlet +++ b/src/algebra/Makefile.pamphlet @@ -233,7 +233,7 @@ axiom_algebra_layer_1 = \ PATAB.o PLOT1.o PPCURVE.o PSCURVE.o \ REAL.o RESLATC.o RETRACT.o RETRACT-.o \ SEGBIND2.o SEGCAT.o STREAM1.o STREAM2.o \ - STREAM3.o + STREAM3.o axiom_algebra_layer_1_nrlibs = \ $(axiom_algebra_layer_1:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) @@ -308,7 +308,7 @@ axiom_algebra_layer_4 = \ REPDB.o RFDIST.o RIDIST.o RMODULE.o \ SEXCAT.o SGROUP.o SGROUP-.o SPACEC.o \ SPLNODE.o STEP.o SUCH.o TEX1.o \ - UDVO.o YSTREAM.o + UDVO.o YSTREAM.o PAIR.o axiom_algebra_layer_4_nrlibs = \ $(axiom_algebra_layer_4:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) @@ -339,7 +339,7 @@ axiom_algebra_layer_5 = \ ODVAR.o OPQUERY.o ORDFIN.o ORDMON.o \ PATMATCH.o PERMCAT.o PDRING.o PDRING-.o \ SDVAR.o SUP2.o TRIGCAT.o TRIGCAT-.o \ - ULS2.o UP2.o + ULS2.o UP2.o axiom_algebra_layer_5_nrlibs = \ $(axiom_algebra_layer_5:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) @@ -997,7 +997,7 @@ axiom_algebra_layer_19 = \ SET.o SPECOUT.o SQMATRIX.o SWITCH.o \ SYMS.o SYMTAB.o SYSSOLP.o UTSCAT.o \ UTSCAT-.o VARIABLE.o WFFINTBS.o SPADPRSR.o \ - PARSER.o + PARSER.o PROPFRML.o axiom_algebra_layer_19_nrlibs = \ $(axiom_algebra_layer_19:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index 85b2c056..4fe76ef3 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -1,4 +1,4 @@ -\documentclass{article} +documentclass{article} \usepackage{axiom} \title{src/algebra boolean.spad} @@ -33,6 +33,233 @@ PropositionalLogic(): Category == with ++ equiv(p,q) returns the logical equivalence of `p', `q'. @ +\section{domain PROPFRML PropositionalFormula} +<<domain PROPFRML PropositionalFormula>>= +)set mess autoload on +)abbrev domain PROPFRML PropositionalFormula +++ Author: Gabriel Dos Reis +++ Date Created: Januray 14, 2008 +++ Date Last Modified: January 16, 2008 +++ Description: This domain implements propositional formula build +++ over a term domain, that itself belongs to PropositionalLogic +PropositionalFormula(T: PropositionalLogic): PropositionalLogic with + if T has CoercibleTo OutputForm then CoercibleTo OutputForm + coerce: T -> % + ++ coerce(t) turns the term `t' into a propositional formula + coerce: Symbol -> % + ++ coerce(t) turns the term `t' into a propositional variable. +-- variables: % -> Set Symbol + ++ variables(p) returns the set of propositional variables + ++ appearing in the proposition `p'. + + term?: % -> Boolean + term: % -> T + + variable?: % -> Boolean + variable: % -> Symbol + + not?: % -> Boolean + notOperand: % -> % + + and?: % -> Boolean + andOperands: % -> Pair(%, %) + + or?: % -> Boolean + orOperands: % -> Pair(%,%) + + implies?: % -> Boolean + impliesOperands: % -> Pair(%,%) + + equiv?: % -> Boolean + equivOperands: % -> Pair(%,%) + + == add + FORMULA ==> Union(base: T, var: Symbol, unForm: %, + binForm: Record(op: Symbol, lhs: %, rhs: %)) + + per(f: FORMULA): % == + f pretend % + + rep(p: %): FORMULA == + p pretend FORMULA + + coerce(t: T): % == + per [t]$FORMULA + + coerce(s: Symbol): % == + per [s]$FORMULA + + not p == + per [p]$FORMULA + + binaryForm(o: Symbol, l: %, r: %): % == + per [[o, l, r]$Record(op: Symbol, lhs: %, rhs: %)]$FORMULA + + p and q == + binaryForm('_and, p, q) + + p or q == + binaryForm('_or, p, q) + + implies(p,q) == + binaryForm('implies, p, q) + + equiv(p,q) == + binaryForm('equiv, p, q) + +-- variables p == +-- p' := rep p +-- p' case base => empty()$Set(Symbol) +-- p' case var => { p'.var } +-- p' case unForm => variables(p'.unForm) +-- p'' := p'.binForm +-- union(variables(p''.lhs), variables(p''.rhs))$Set(Symbol) + + -- returns true if the proposition `p' is a formula of kind + -- indicated by `o'. + isBinaryNode?(p: %, o: Symbol): Boolean == + p' := rep p + p' case binForm and p'.binForm.op = o + + -- returns the operands of a binary formula node + binaryOperands(p: %): Pair(%,%) == + p' := (rep p).binForm + pair(p'.lhs,p'.rhs)$Pair(%,%) + + term? p == + rep p case base + + term p == + term? p => (rep p).base + userError "formula is not a term" + + variable? p == + rep p case var + + variable p == + variable? p => (rep p).var + userError "formula is not a variable" + + not? p == + rep p case unForm + + notOperand p == + not? p => (rep p).unForm + userError "formula is not a logical negation" + + and? p == + isBinaryNode?(p,'_and) + + andOperands p == + and? p => binaryOperands p + userError "formula is not a conjunction formula" + + or? p == + isBinaryNode?(p,'_or) + + orOperands p == + or? p => binaryOperands p + userError "formula is not a disjunction formula" + + implies? p == + isBinaryNode?(p, 'implies) + + impliesOperands p == + implies? p => binaryOperands p + userError "formula is not an implication formula" + + equiv? p == + isBinaryNode?(p,'equiv) + + equivOperands p == + equiv? p => binaryOperands p + userError "formula is not an equivalence equivalence" + + -- Unparsing grammar. + -- + -- Ideally, the following syntax would the external form + -- Formula: + -- EquivFormula + -- + -- EquivFormula: + -- ImpliesFormula + -- ImpliesFormula <=> EquivFormula + -- + -- ImpliesFormula: + -- OrFormula + -- OrFormula => ImpliesFormula + -- + -- OrFormula: + -- AndFormula + -- AndFormula or OrFormula + -- + -- AndFormula + -- NotFormula + -- NotFormula and AndFormula + -- + -- NotFormula: + -- PrimaryFormula + -- not NotFormula + -- + -- PrimaryFormula: + -- Term + -- ( Formula ) + -- + -- Note: Since the token '=>' already means a construct different + -- from what we would like to have as a notation for + -- propositional logic, we will output the formula `p => q' + -- as implies(p,q), which looks like a function call. + -- Similarly, we do not have the token `<=>' for logical + -- equivalence; so we unparser `p <=> q' as equiv(p,q). + -- + -- So, we modify the nonterminal PrimaryFormula to read + -- PrimaryFormula: + -- Term + -- implies(Formula, Formula) + -- equiv(Formula, Formula) + if T has CoercibleTo OutputForm then + formula: % -> OutputForm + coerce(p: %): OutputForm == + formula p + + primaryFormula(p: %): OutputForm == + term? p => term(p)::OutputForm + variable? p => variable(p)::OutputForm + if rep p case binForm then + p' := (rep p).binForm + p'.op = 'implies or p'.op = 'equiv => + return elt(outputForm p'.op, + [formula p'.lhs, formula p'.rhs])$OutputForm + paren(formula p)$OutputForm + + notFormula(p: %): OutputForm == + not? p => + elt(outputForm '_not, [notFormula((rep p).'unForm)])$OutputForm + primaryFormula p + + andFormula(p: %): OutputForm == + and? p => + p' := (rep p).binForm + -- ??? idealy, we should be using `and$OutputForm' but + -- ??? a bug in the compiler currently prevents that. + infix(outputForm '_and, notFormula p'.lhs, + andFormula p'.rhs)$OutputForm + notFormula p + + orFormula(p: %): OutputForm == + or? p => + p' := (rep p).binForm + -- ??? idealy, we should be using `or$OutputForm' but + -- ??? a bug in the compiler currently prevents that. + infix(outputForm '_or, andFormula p'.lhs, + orFormula p'.rhs)$OutputForm + andFormula p + + formula p == + -- Note: this should be equivFormula, but see the explanation above. + orFormula p + +@ \section{domain REF Reference} <<domain REF Reference>>= @@ -503,6 +730,7 @@ Bits(): Exports == Implementation where <<domain IBITS IndexedBits>> <<domain BITS Bits>> <<category PROPLOG PropositionalLogic>> +<<domain PROPFRML PropositionalFormula>> @ \eject \begin{thebibliography}{99} diff --git a/src/algebra/exposed.lsp.pamphlet b/src/algebra/exposed.lsp.pamphlet index 94b05ddb..be4f8464 100644 --- a/src/algebra/exposed.lsp.pamphlet +++ b/src/algebra/exposed.lsp.pamphlet @@ -254,6 +254,7 @@ (|OrthogonalPolynomialFunctions| . ORTHPOL) (|OutputPackage| . OUT) (|PadeApproximantPackage| . PADEPAC) + (|Pair| . PAIR) (|Palette| . PALETTE) (|PartialFraction| . PFR) (|PatternFunctions2| . PATTERN2) @@ -289,6 +290,7 @@ (|PrimeField| . PF) (|PrimitiveArrayFunctions2| . PRIMARR2) (|PrintPackage| . PRINT) + (|PropositionalFormula| . PROPFRML) (|QuadraticForm| . QFORM) (|QuasiComponentPackage| . QCMPACK) (|Quaternion| . QUAT) @@ -663,6 +665,7 @@ (|PrimitiveFunctionCategory| . PRIMCAT) (|PrincipalIdealDomain| . PID) (|PriorityQueueAggregate| . PRQAGG) + (|PropositionalLogic| . PROPLOG) (|QuaternionCategory| . QUATCAT) (|QueueAggregate| . QUAGG) (|QuotientFieldCategory| . QFCAT) diff --git a/src/algebra/mkrecord.spad.pamphlet b/src/algebra/mkrecord.spad.pamphlet index 2fe15855..0087800c 100644 --- a/src/algebra/mkrecord.spad.pamphlet +++ b/src/algebra/mkrecord.spad.pamphlet @@ -25,10 +25,64 @@ MakeRecord(S: Type, T: Type): public == private where [s,t]$Record(part1: S, part2: T) @ + +\section{domain PAIR Pair} +<<domain PAIR Pair>>= +)abbrev domain PAIR Pair +++ Author: Gabriel Dos Reis +++ Date Created: January 16, 2008 +++ Date Last Modified: January 16, 2008 +++ Description: This domain provides a very simple representation +++ of the notion of `pair of objects'. It does not try to achieve +++ all possible imaginable things. +Pair(S: Type, T: Type): Public == Private where + Public ==> Type with + + if S has CoercibleTo OutputForm and T has CoercibleTo OutputForm then + CoercibleTo OutputForm + + if S has SetCategory and T has SetCategory then SetCategory + + pair: (S,T) -> % + ++ pair(s,t) returns a pair object composed of `s' and `t'. + construct: (S,T) -> % + ++ construct(s,t) is same as pair(s,t), with syntactic sugar. + first: % -> S + ++ first(p) extracts the first component of `p'. + second: % -> T + ++ second(p) extracts the second components of `p'. + + Private ==> add + Rep := Record(fst: S, snd: T) + + pair(s,t) == + [s,t]$Rep + + construct(s,t) == + pair(s,t) + + first x == + x.fst + + second x == + x.snd + + if S has CoercibleTo OutputForm and T has CoercibleTo OutputForm then + coerce x == + paren([first(x)::OutputForm, second(x)::OutputForm])$OutputForm + + if S has SetCategory and T has SetCategory then + x = y == + first(x) = first(y) and second(x) = second(y) +@ + + \section{License} <<license>>= ---Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. +--Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd. --All rights reserved. +-- Copyright (C) 2007-2008, Gabriel Dos Reis. +-- All rights reserved. -- --Redistribution and use in source and binary forms, with or without --modification, are permitted provided that the following conditions are @@ -62,6 +116,7 @@ MakeRecord(S: Type, T: Type): public == private where <<license>> <<package MKRECORD MakeRecord>> +<<domain PAIR Pair>> @ \eject \begin{thebibliography}{99} |