This implementation of an Inductive (recursive) data type involves
the categorical co-product construction. See: LimitsAndColimits
fricas
(1) -> )library colimits
fricas
Reading #P"/var/aw/var/LatexWiki/colimits.asy"
Sum2 is now explicitly exposed in frame initial
Sum2Functions is now explicitly exposed in frame initial
Sum3 is now explicitly exposed in frame initial
Sum3Functions is now explicitly exposed in frame initial
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
Aldor compiler and options
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
Use the system command )set compiler args to change these
options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/expr.as", line 2:
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.
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 Aldor compiler and options
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
Use the system command )set compiler args to change these
options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1062037838131250571-25px003.as", line 2:
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.
fricas
n:Expr:=3
Expr is not a valid type.
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 Aldor compiler and options
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
Use the system command )set compiler args to change these
options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as", line 1:
#include "axiom"
^
[L1 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.
Here is an example expression
fricas
10::RecExpr
RecExpr is not a valid type.