Edit detail for Dynamic Function Domains revision 1 of 1

On Wednesday, January 12, 2005 12:00 PM you wrote: Ralf Hemmecke wrote:

Well, I haven't checked whether it should really work, but shouldn't be:

 Foo: with {
    g: (n: PositiveInteger, k: PositiveInteger) ->
       (P: PrimeFieldCategory, x: P)
 } == add {
    g(n: PositiveInteger, k: PositiveInteger ):
     (P: PrimeFieldCategory, x:P) == {
     (PrimeField(n), k::Integer::PrimeField(n)
    }
 }

be even better?

Later William Sit wrote:

In fact you just pointed a way to solve the problem! Notice that you are in effect constructing a domain! So first create this domain (call this anything else you like)

(1) -> )abbrev domain PPF PointedPrimeField
--%PointedPrimeField
PointedPrimeField(n:PositiveInteger):Cat==Dog where
  Cat == FiniteFieldCategory with
    foo:PositiveInteger->PrimeField(n)
  Dog == PrimeField(n) add
    foo(k)==k::Integer::PrimeField(n)

Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3896265268149061013-25px.001.spad
      using old system compiler.
   PPF abbreviates domain PointedPrimeField 
------------------------------------------------------------------------
   initializing NRLIB PPF for PointedPrimeField 
   compiling into NRLIB PPF 
   compiling exported foo : PositiveInteger -> PrimeField n
Time: 0.01 SEC.

(time taken in buildFunctor:  4186)

;;;     ***       |PointedPrimeField| REDEFINED

;;;     ***       |PointedPrimeField| REDEFINED
Time: 0.03 SEC.

   Cumulative Statistics for Constructor PointedPrimeField
      Time: 0.04 seconds

--------------non extending category----------------------
.. PointedPrimeField(#1) of cat 
(|Join| (|FiniteFieldCategory|)
        (CATEGORY |package|
         (SIGNATURE |foo| ((|PrimeField| |#1|) (|PositiveInteger|)))))   has no 
(|FiniteAlgebraicExtensionField| %)    finalizing NRLIB PPF 
   Processing PointedPrimeField for Browser database:
--->-->PointedPrimeField(constructor): Not documented!!!!
--->-->PointedPrimeField((foo ((PrimeField n) (PositiveInteger)))): Not documented!!!!
--->-->PointedPrimeField(): Missing Description
; compiling file "/var/aw/var/LatexWiki/PPF.NRLIB/PPF.lsp" (written 19 NOV 2024 04:29:23 AM):

; wrote /var/aw/var/LatexWiki/PPF.NRLIB/PPF.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   PointedPrimeField is now explicitly exposed in frame initial 
   PointedPrimeField will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/PPF.NRLIB/PPF

After compiling, define in the interpreter

g(n,k)==foo(k)$PPF(n)

g(7,4)

   Cannot compile a $-expression involving a local variable.
   FriCAS will attempt to step through and interpret the code.

(1)

and it works (in Axiom)! (Do not declare the types for g because n is not defined).

Compiling g is still a problem in Axiom due to signature limitation. At least this way, inlining a complicated function is almost like a function call.

The idea is: Since in creating domains (or any other types of constructors), we are in effect creating a function(the domain constructor PPF is a function of sorts, or functor) and the compiler can take dependent types in its signature,structurally:

  PPF(n:PositiveInteger)==PrimeField(n) with foo

so it should be able to compile something like g by lifting it to the package level.

So here is another way using package.

)abbrev package FOO Foo
Foo(n:PositiveInteger, k:Integer):with point:()->PrimeField(n)
  == add point()==k::PrimeField(n)

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/6339949729126981292-25px003.spad
      using old system compiler.
   FOO abbreviates package Foo 
------------------------------------------------------------------------
   initializing NRLIB FOO for Foo 
   compiling into NRLIB FOO 
   compiling exported point : () -> PrimeField n
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |Foo| REDEFINED

;;;     ***       |Foo| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor Foo
      Time: 0 seconds

   finalizing NRLIB FOO 
   Processing Foo for Browser database:
--->-->Foo(constructor): Not documented!!!!
--->-->Foo((point ((PrimeField n)))): Not documented!!!!
--->-->Foo(): Missing Description
; compiling file "/var/aw/var/LatexWiki/FOO.NRLIB/FOO.lsp" (written 19 NOV 2024 04:29:23 AM):

; wrote /var/aw/var/LatexWiki/FOO.NRLIB/FOO.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   Foo is now explicitly exposed in frame initial 
   Foo will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/FOO.NRLIB/FOO

After compiling, we can use:

  point()$Foo(n,k)

in any computation in compiler code (and in interpreter). In the interpreter you can call this bar(n,k):

bar(n,k) == point()$Foo(n,k)

bar(7,4)

   Cannot compile a $-expression involving a local variable.
   FriCAS will attempt to step through and interpret the code.

(2)

Can someone give an example where the signature of bar:

  bar: (n: PositiveInteger, k: PositiveInteger) -> PrimeField(n)

is actually needed?

)abbrev package FOO2 Foo2
Foo2(n:PositiveInteger, k:IntegerMod(n)):with point:()->PrimeField(n)
  == add point()==convert(k)$IntegerMod(n)::PrimeField(n)

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3511022708306225656-25px005.spad
      using old system compiler.
   FOO2 abbreviates package Foo2 
------------------------------------------------------------------------
   initializing NRLIB FOO2 for Foo2 
   compiling into NRLIB FOO2 
   compiling exported point : () -> PrimeField n
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |Foo2| REDEFINED

;;;     ***       |Foo2| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor Foo2
      Time: 0 seconds

   finalizing NRLIB FOO2 
   Processing Foo2 for Browser database:
--->-->Foo2(constructor): Not documented!!!!
--->-->Foo2((point ((PrimeField n)))): Not documented!!!!
--->-->Foo2(): Missing Description
; compiling file "/var/aw/var/LatexWiki/FOO2.NRLIB/FOO2.lsp" (written 19 NOV 2024 04:29:23 AM):

; wrote /var/aw/var/LatexWiki/FOO2.NRLIB/FOO2.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   Foo2 is now explicitly exposed in frame initial 
   Foo2 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/FOO2.NRLIB/FOO2

point()$Foo2(13,2)

(3)