This implementation of an Inductive (recursive) data type involves
the categorical co-product construction. See: LimitsAndColimits
fricas
)library colimits
fricas
Reading /var/aw/var/LatexWiki/colimits.asy
Sum2 is now explicitly exposed in frame initial
Sum2 will be automatically loaded when needed from
/var/aw/var/LatexWiki/colimits
Sum2Functions is now explicitly exposed in frame initial
Sum2Functions will be automatically loaded when needed from
/var/aw/var/LatexWiki/colimits
Sum3 is now explicitly exposed in frame initial
Sum3 will be automatically loaded when needed from
/var/aw/var/LatexWiki/colimits
Sum3Functions is now explicitly exposed in frame initial
Sum3Functions will be automatically loaded when needed from
/var/aw/var/LatexWiki/colimits
An example of Arithmetic Expressions as an Inductive Type
aldor
#pile
#include "axiom"
#library COLIMIT "colimits.ao"
import from COLIMIT
+++ Category of Integer-valued Arthemetic Expresions
ExprCat:Category == with
eval: % -> Integer
-- evaluates the expression as an Integer
coerce: % -> OutputForm
-- displays the expression
+++ Constructor for atomic Integers
MkInt(Z:IntegerNumberSystem): ExprCat
== add
Rep == Integer
-- Export
eval(x:%):Integer == rep(x)
coerce(x:%):OutputForm == outputForm rep x
+++ Constructor for additions
MkAdd(X:ExprCat,Y:ExprCat): ExprCat
== add
Rep==Record(left:X,right:Y)
import from Rep, OutputForm
-- Local:
plus(x:X,y:Y):OutputForm == paren(x::OutputForm + y::OutputForm);
sum(x:X,y:Y):Integer == eval(x) + eval(y);
-- Export:
eval(x:%):Integer == sum explode rep x
coerce(x:%):OutputForm == plus explode rep x
+++ Constructor for multiplications
MkMul(X:ExprCat,Y:ExprCat): ExprCat
== add
Rep==Record(left:X,right:Y)
import from Rep, OutputForm
-- Local:
times(x:X,y:Y):OutputForm== paren(x::OutputForm * y::OutputForm);
product(x:X,y:Y):Integer == eval(x) * eval(y);
-- Export:
eval(x:%):Integer == product explode rep x
coerce(x:%):OutputForm == times explode rep x
MI==>MkInt(Integer)
MA==>MkAdd(%,%)
MM==>MkMul(%,%)
+++ Constructor of Arithmetic Expressions over the Integers
Expr: ExprCat
== add
Rep == Sum(MI,MA,MM)
import from Rep, MI, MA, MM
-- Export:
eval(x:%):Integer == sum(Integer,eval,eval,eval)(rep x)
coerce(x:%):OutputForm == sum(OutputForm,coerce,coerce,coerce)(rep x)
aldor
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/expr.as using
AXIOM-XL compiler and options
-O -Fasy -Fao -Flsp -laxiom -Mno-ALDOR_W_WillObsolete -DAxiom -Y $AXIOM/algebra -I $AXIOM/algebra
Use the system command )set compiler args to change these
options.
#1 (Warning) Could not use archive file `libaxiom.al'.
#2 (Warning) Could not use archive file `libaxiom.al'.
#9 (Warning) Could not use archive file `libaxiom.al'.
Program fault (segmentation violation).#10 (Error) Program fault (segmentation violation).
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 4:
import from AxiomLib;
............^
[L4 C13] #3 (Error) No meaning for identifier `AxiomLib'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 15:
import { true: %, false: % } from Boolean;
..................................^
[L15 C35] #4 (Error) No meaning for identifier `Boolean'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 17:
string: Literal -> %;
........................^.......^
[L17 C25] #5 (Error) No meaning for identifier `Literal'.
[L17 C33] #6 (Error) There are no suitable meanings for the operator `->'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 18:
} from String;
.......^
[L18 C8] #8 (Error) No meaning for identifier `String'.
The )library system command was not called after compilation.
Now extend it to provide the Axiom interpreter interface.
aldor
#pile
#include "axiom"
#library EXPR "expr.ao"
import from EXPR
#library COLIMIT "colimits.ao"
import from COLIMIT
extend MkInt(Z:IntegerNumberSystem): with
coerce: Z -> %
-- converts a Z-valued object to an atomic Integer
== add
Rep == Integer
-- Export
coerce(i:Z):% == per(convert(i))
extend MkAdd(X:ExprCat,Y:ExprCat): with
+: (X,Y) -> %
-- returns an expression representing the sum
== add
Rep==Record(left:X,right:Y)
import from Rep
-- Export
((x:X) + (y:Y)):% == per [x,y]
extend MkMul(X:ExprCat,Y:ExprCat): with
*: (X,Y) -> %
-- returns an expression representing the product
== add
Rep==Record(left:X,right:Y)
import from Rep
-- Export
((x:X) * (y:Y)):% == per [x,y]
MI==>MkInt(Integer)
MA==>MkAdd(%,%)
MM==>MkMul(%,%)
+++ extends domain Expr as above
extend Expr: with
coerce: Integer -> %
+:(%,%) -> %
*:(%,%) -> %
== add
Rep == Sum(MI,MA,MM)
import from Rep, MI, MA, MM
-- Export:
coerce(n: Integer):% == per(inject( n::MI ))
((x:%) + (y:%)):% == per(inject( (x + y)$MA ))
((x:%) * (y:%)):% == per(inject( (x * y)$MM ))
aldor
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1062037838131250571-25px003.as
using AXIOM-XL compiler and options
-O -Fasy -Fao -Flsp -laxiom -Mno-ALDOR_W_WillObsolete -DAxiom -Y $AXIOM/algebra -I $AXIOM/algebra
Use the system command )set compiler args to change these
options.
#1 (Warning) Could not use archive file `libaxiom.al'.
#2 (Warning) Could not use archive file `libaxiom.al'.
#9 (Warning) Could not use archive file `libaxiom.al'.
Program fault (segmentation violation).#10 (Error) Program fault (segmentation violation).
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 4:
import from AxiomLib;
............^
[L4 C13] #3 (Error) No meaning for identifier `AxiomLib'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 15:
import { true: %, false: % } from Boolean;
..................................^
[L15 C35] #4 (Error) No meaning for identifier `Boolean'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 17:
string: Literal -> %;
........................^.......^
[L17 C25] #5 (Error) No meaning for identifier `Literal'.
[L17 C33] #6 (Error) There are no suitable meanings for the operator `->'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 18:
} from String;
.......^
[L18 C8] #8 (Error) No meaning for identifier `String'.
The )library system command was not called after compilation.
fricas
n:Expr:=3
fricas
m:Expr:=4
fricas
p:=n+m
fricas
eval(p)
Type: Fraction(Integer)
fricas
q:=p*5
fricas
eval(q)
Type: Fraction(Integer)
Ralf Hemmecke and Bill Page wrote:
Recursive Types
aldor
#include "axiom"
RecExpr:with {
coerce: Integer -> %;
+: (%, %) -> %;
*: (%, %) -> %;
coerce: % -> OutputForm;
eval: % -> Integer;
} == add {
Rep == Union(MakeInt:Integer,
MakeAdd:Record(l:%, r:%),
MakeMul:Record(l:%, r:%));
import from Rep;
import from 'MakeInt', 'MakeAdd', 'MakeMul';
import from OutputForm;
--
-- Local
plus(x:%,y:%):OutputForm == paren(x::OutputForm + y::OutputForm);
times(x:%,y:%):OutputForm== paren(x::OutputForm * y::OutputForm);
sum(x:%,y:%):Integer == eval(x) + eval(y);
product(x:%,y:%):Integer == eval(x) * eval(y);
--
-- Input
coerce(n: Integer):% == per [MakeInt==n];
((x:%) + (y:%)): % == per [MakeAdd==[x,y]];
((x:%) * (y:%)): % == per [MakeMul==[x,y]];
--
-- Output
coerce(i:%):OutputForm == { n:=rep(i);
n case MakeInt => outputForm n.MakeInt;
n case MakeAdd => plus explode n.MakeAdd;
n case MakeMul => times explode n.MakeMul;
never;
};
--
-- Evaluation
eval(i:%):Integer == { n:=rep(i);
n case MakeInt => n.MakeInt;
n case MakeAdd => sum explode n.MakeAdd;
n case MakeMul => product explode n.MakeMul;
never;
}
}
aldor
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as
using AXIOM-XL compiler and options
-O -Fasy -Fao -Flsp -laxiom -Mno-ALDOR_W_WillObsolete -DAxiom -Y $AXIOM/algebra -I $AXIOM/algebra
Use the system command )set compiler args to change these
options.
#1 (Warning) Could not use archive file `libaxiom.al'.
#2 (Warning) Could not use archive file `libaxiom.al'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 4:
import from AxiomLib;
............^
[L4 C13] #3 (Error) No meaning for identifier `AxiomLib'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 15:
import { true: %, false: % } from Boolean;
..................................^
[L15 C35] #4 (Error) No meaning for identifier `Boolean'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 17:
string: Literal -> %;
........................^.......^
[L17 C25] #5 (Error) No meaning for identifier `Literal'.
[L17 C33] #6 (Error) There are no suitable meanings for the operator `->'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 18:
} from String;
.......^
[L18 C8] #8 (Error) No meaning for identifier `String'.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as", line 3:
coerce: Integer -> %;
............^
[L3 C13] #9 (Error) No meaning for identifier `Integer'.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as", line 6:
coerce: % -> OutputForm;
.................^
[L6 C18] #12 (Error) No meaning for identifier `OutputForm'.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as", line 7:
eval: % -> Integer;
............^
[L7 C13] #10 (Error) There are no suitable meanings for the operator `->'.
[L7 C13] #13 (Fatal Error) Too many errors (use `-M emax=n' or `-M no-emax' to change the limit).
The )library system command was not called after compilation.
Here is an example expression
fricas
10::RecExpr
Cannot convert from type PositiveInteger to NIL for value
10
11::RecExpr
Cannot convert from type PositiveInteger to NIL for value
11
12::RecExpr
Cannot convert from type PositiveInteger to NIL for value
12
11::RecExpr + 12::RecExpr
Cannot convert from type PositiveInteger to NIL for value
11
10::RecExpr * (11::RecExpr + 12::RecExpr)
Cannot convert from type PositiveInteger to NIL for value
10