login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

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

\label{eq1}3(1)
fricas
m:Expr:=4

\label{eq2}4(2)
fricas
p:=n+m

\label{eq3}7(3)
fricas
eval(p)

\label{eq4}7(4)
Type: Fraction(Integer)
fricas
q:=p*5

\label{eq5}35(5)
fricas
eval(q)

\label{eq6}35(6)
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




  Subject:   Be Bold !!
  ( 13 subscribers )  
Please rate this page: