help links subscribe changes refresh edit

	Limits and Colimits
	↑	→ SandBoxEqualizerInOpenAxiom

SandBoxAldorInductiveTypes

Edit detail for SandBoxAldorInductiveTypes revision 1 of 2

	1 2
Editor: Time: 2007/11/18 17:45:37 GMT-8
Note: categorical co-product construction

changed:
-
This implementation of an Inductive (recursive) data type involves
the categorical co-product construction. See: SandBoxLimitsAndColimits
\begin{axiom}
)library colimits
\end{axiom}

An example of Arithmetic Expressions as an Inductive Type
\begin{aldor}[expr]
#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)
\end{aldor}

Now extend it to provide the Axiom interpreter interface.
\begin{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 ))
\end{aldor}

\begin{axiom}
n:Expr:=3
m:Expr:=4
p:=n+m
eval(p)
q:=p*5
eval(q)
\end{axiom}

**Ralf Hemmecke and Bill Page wrote:**

Recursive Types

\begin{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;
    }
}
\end{aldor}

Here is an example expression
\begin{axiom}
10::RecExpr
11::RecExpr
12::RecExpr
11::RecExpr + 12::RecExpr
10::RecExpr * (11::RecExpr + 12::RecExpr)
\end{axiom}

This implementation of an Inductive (recursive) data type involves the categorical co-product construction. See: SandBoxLimitsAndColimits?

axiom)library colimits
   Reading /var/zope2/var/LatexWiki/colimits.asy
   Sum is now explicitly exposed in frame initial 
   Sum will be automatically loaded when needed from 
      /var/zope2/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/zope2/var/LatexWiki/expr.as using AXIOM-XL compiler and 
      options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file ./expr.lsp
   Issuing )library command for expr
   Reading /var/zope2/var/LatexWiki/expr.asy
   Expr is now explicitly exposed in frame initial 
   Expr will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/expr
   MkAdd is now explicitly exposed in frame initial 
   MkAdd will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/expr
   MkInt is now explicitly exposed in frame initial 
   MkInt will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/expr
   MkMul is now explicitly exposed in frame initial 
   MkMul will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/expr
   ExprCat is now explicitly exposed in frame initial 
   ExprCat will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/expr

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/zope2/var/LatexWiki/1062037838131250571-25px003.as using 
      AXIOM-XL compiler and options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file 
      ./1062037838131250571-25px003.lsp
   Issuing )library command for 1062037838131250571-25px003
   Reading /var/zope2/var/LatexWiki/1062037838131250571-25px003.asy
   Expr is already explicitly exposed in frame initial 
   Expr will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/1062037838131250571-25px003
   MkAdd is already explicitly exposed in frame initial 
   MkAdd will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/1062037838131250571-25px003
   MkInt is already explicitly exposed in frame initial 
   MkInt will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/1062037838131250571-25px003
   MkMul is already explicitly exposed in frame initial 
   MkMul will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/1062037838131250571-25px003

axiom
n:Expr:=3

(1)

Type: Expr

axiom
m:Expr:=4

(2)

Type: Expr

axiom
p:=n+m

(3)

Type: Expr

axiom
eval(p)

(4)

Type: PositiveInteger?

axiom
q:=p*5

(5)

Type: Expr

axiom
eval(q)

(6)

Type: PositiveInteger?

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/zope2/var/LatexWiki/4075514935174965511-25px005.as using 
      AXIOM-XL compiler and options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file 
      ./4075514935174965511-25px005.lsp
   Issuing )library command for 4075514935174965511-25px005
   Reading /var/zope2/var/LatexWiki/4075514935174965511-25px005.asy
   RecExpr is now explicitly exposed in frame initial 
   RecExpr will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/4075514935174965511-25px005

Here is an example expression

axiom
10::RecExpr

(7)

Type: RecExpr?

axiom
11::RecExpr

(8)

Type: RecExpr?

axiom
12::RecExpr

(9)

Type: RecExpr?

axiom
11::RecExpr + 12::RecExpr

(10)

Type: RecExpr?

axiom
10::RecExpr * (11::RecExpr + 12::RecExpr)

(11)

Type: RecExpr?