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

This page was renamed to AnonymousCategories?. You can delete this one if no longer needed.

Or click edit or Add Comments to make further online tests here.

On Aug 12, 2007 6:35 PM Weiss, Juergen wrote:

I found the old document about type equivalence in Scratchpad. It's: A New Algebra System, May, 29 th 1984, James H Davenport. I have only found a paper version. Maybe someone has an online version.

It states that:

  1. Two named types are only equivalent if the names are the same.
  2. Anonymous types are equivalent when stucturally equivalent
  3. An anonymous type is never equivalent to a named type.

So following 1:

  t1 == List Term
  t2 == List Term
  x : t1
  y : t2
  y := x

is not supposed to work, [t1 and t2 should be treated as different types]

spad
)abbrev package TEST test
test(): with
    main:()->Integer
  == add
    main() ==
      t1:IntegerNumberSystem == Integer
      t2:IntegerNumberSystem == Integer
      x : t1
      x := 1$t1
      y : t2
      y := x
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4406049181591081329-25px001.spad
      using old system compiler.
   TEST abbreviates package test 
------------------------------------------------------------------------
   initializing NRLIB TEST for test 
   compiling into NRLIB TEST 
   compiling exported main : () -> Integer
   Semantic Errors: 
      [1] main:  +-> is not a known type
****** comp fails at level 3 with expression: ****** error in function main
(SEQ (DEF (|t1|) ((|IntegerNumberSystem|)) (NIL) (|Integer|)) (DEF (|t2|) ((|IntegerNumberSystem|)) (NIL) (|Integer|)) (|:| |x| |t1|) (|:=| |x| | << | (|Sel| |t1| 1) | >> |) (|:| |y| |t2|) (|exit| 1 (|:=| |y| |x|))) ****** level 3 ****** $x:= (Sel t1 (One)) $m:= t1 $f:= ((((|x| #) (|t2| #) (|t1| #) (|main| #) ...)))
>> Apparent user error: NoValueMode is an unknown mode

There should be a compile error above.

fricas
main()
There are no library operations named main Use HyperDoc Browse or issue )what op main to learn if there is any operation containing " main " in its name.
Cannot find a no-argument definition or library operation named main .

but following 2:

  x : List Term
  y : List Term
  y := x

is ok,

spad
)abbrev package TEST test2
test2(): with
    main2:()->Integer
  == add
    main2()==
      x : Integer
      x := 1
      y : Integer
      y := x
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3154192227704798176-25px003.spad
      using old system compiler.
   TEST abbreviates package test2 
------------------------------------------------------------------------
   initializing NRLIB TEST for test2 
   compiling into NRLIB TEST 
   compiling exported main2 : () -> Integer
Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |test2| REDEFINED
;;; *** |test2| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor test2 Time: 0 seconds
finalizing NRLIB TEST Processing test2 for Browser database: --->-->test2(constructor): Not documented!!!! --->-->test2((main2 ((Integer)))): Not documented!!!! --->-->test2(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TEST.NRLIB/TEST.lsp" (written 04 APR 2022 05:49:43 PM):
; /var/aw/var/LatexWiki/TEST.NRLIB/TEST.fasl written ; compilation finished in 0:00:00.010 ------------------------------------------------------------------------ test2 is now explicitly exposed in frame initial test2 will be automatically loaded when needed from /var/aw/var/LatexWiki/TEST.NRLIB/TEST

fricas
main2()

\label{eq1}1(1)
Type: PositiveInteger?

also

spad
)abbrev package TEST test4
test4(): with
    main4:()->Integer
  == add
    main4():Integer ==
      t1():IntegerNumberSystem == Integer
      x : t1
      x := 1$t1
      y : t1
      y := x
      1
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/346730625682591668-25px005.spad
      using old system compiler.
   TEST abbreviates package test4 
------------------------------------------------------------------------
   initializing NRLIB TEST for test4 
   compiling into NRLIB TEST 
   compiling exported main4 : () -> Integer
   Semantic Errors: 
      [1] main4:  +-> is not a known type
****** comp fails at level 3 with expression: ****** error in function main4
(SEQ (DEF (|t1|) ((|IntegerNumberSystem|)) (NIL) (|Integer|)) (|:| |x| |t1|) (|:=| |x| | << | (|Sel| |t1| 1) | >> |) (|:| |y| |t1|) (|:=| |y| |x|) (|exit| 1 1)) ****** level 3 ****** $x:= (Sel t1 (One)) $m:= t1 $f:= ((((|x| #) (|t1| #) (|main4| #) (|$DomainsInScope| # # #) ...)))
>> Apparent user error: NoValueMode is an unknown mode

This compiles ok but there is a run-time error. Why?

fricas
main4()
There are no library operations named main4 Use HyperDoc Browse or issue )what op main4 to learn if there is any operation containing " main4 " in its name.
Cannot find a no-argument definition or library operation named main4 .

and following 3:

  t == List Term
  x : List Term
  y : t
  y := x

is not supposed to work as well

spad
)abbrev package TEST test3
test3(): with
    main3:()->Integer
  == add
    main3() ==
      t:IntegerNumberSystem == Integer
      x : Integer
      x := 1
      y : t
      y := x
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2232261183027663296-25px007.spad
      using old system compiler.
   TEST abbreviates package test3 
------------------------------------------------------------------------
   initializing NRLIB TEST for test3 
   compiling into NRLIB TEST 
   compiling exported main3 : () -> Integer
   Semantic Errors: 
      [1] main3:  +-> is not a known type
****** comp fails at level 3 with expression: ****** error in function main3
(SEQ (DEF (|t|) ((|IntegerNumberSystem|)) (NIL) (|Integer|)) (|:| |x| (|Integer|)) (|:=| |x| 1) (|:| |y| |t|) (|exit| 1 | << | (|:=| |y| |x|) | >> |)) ****** level 3 ****** $x:= (:= y x) $m:= (Integer) $f:= ((((|y| #) (|x| # #) (|t| #) (|main3| #) ...)))
>> Apparent user error: CANNOT ASSIGN: x OF MODE: (Integer) TO: y OF MODE: t

There should produce a compile error above.

fricas
main3()
There are no library operations named main3 Use HyperDoc Browse or issue )what op main3 to learn if there is any operation containing " main3 " in its name.
Cannot find a no-argument definition or library operation named main3 .

All examples are taken from the paper.

I am not sure how much of this design is preserved in the current system. But without having had an intense look at the examples, I got the impression, that they follow the rules above.

Regards

Juergen Weiss

The failure above is not convincing, since the spad code did not compile. It's not clear where the failure lies. For example, in Test4, the compiler message says |t1| is not defined. A slight modification causes a different error (for example adding () after t1 in test4):

spad
)abbrev package TESTFIVE test5
test5(): with
    main5:()->Integer
  == add
    main5():Integer ==
      t1():IntegerNumberSystem == Integer 
      x : t1()
      x := 1$t1()
      y : t1()
      y := x
      1$Integer
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3611641870102941622-25px009.spad
      using old system compiler.
   TESTFIVE abbreviates package test5 
------------------------------------------------------------------------
   initializing NRLIB TESTFIVE for test5 
   compiling into NRLIB TESTFIVE 
   compiling exported main5 : () -> Integer
   Internal Error
   Error while instantiating type t1

fricas
main5()
There are no library operations named main5 Use HyperDoc Browse or issue )what op main5 to learn if there is any operation containing " main5 " in its name.
Cannot find a no-argument definition or library operation named main5 .

The better way to test equivalence of domains is to actually construct new domains.

spad
)abbrev domain TEEONE tee1
tee1():IntegerNumberSystem == Integer
)abbrev domain TEETWO tee2 tee2():IntegerNumberSystem == Integer
)abbrev package TESTSIX test6 test6(): with main6:()->Integer == add main6():Integer == x : tee1 x := 1$tee1 y : tee1 y := x 1$Integer
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5058510425788394140-25px011.spad
      using old system compiler.
   TEEONE abbreviates domain tee1 
------------------------------------------------------------------------
   initializing NRLIB TEEONE for tee1 
   compiling into NRLIB TEEONE 
(time taken in buildFunctor:  10)
;;; *** |tee1| REDEFINED
;;; *** |tee1| REDEFINED Time: 0.01 SEC.
Cumulative Statistics for Constructor tee1 Time: 0.01 seconds
--------------non extending category---------------------- .. tee1 of cat (|IntegerNumberSystem|) has no (|LinearlyExplicitOver| (|Integer|)) finalizing NRLIB TEEONE Processing tee1 for Browser database: --->-->tee1(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TEEONE.NRLIB/TEEONE.lsp" (written 04 APR 2022 05:49:44 PM):
; /var/aw/var/LatexWiki/TEEONE.NRLIB/TEEONE.fasl written ; compilation finished in 0:00:00.008 ------------------------------------------------------------------------ tee1 is now explicitly exposed in frame initial tee1 will be automatically loaded when needed from /var/aw/var/LatexWiki/TEEONE.NRLIB/TEEONE
TEETWO abbreviates domain tee2 ------------------------------------------------------------------------ initializing NRLIB TEETWO for tee2 compiling into NRLIB TEETWO (time taken in buildFunctor: 0)
;;; *** |tee2| REDEFINED
;;; *** |tee2| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor tee2 Time: 0 seconds
--------------non extending category---------------------- .. tee2 of cat (|IntegerNumberSystem|) has no (|LinearlyExplicitOver| (|Integer|)) finalizing NRLIB TEETWO Processing tee2 for Browser database: --->-->tee2(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TEETWO.NRLIB/TEETWO.lsp" (written 04 APR 2022 05:49:44 PM):
; /var/aw/var/LatexWiki/TEETWO.NRLIB/TEETWO.fasl written ; compilation finished in 0:00:00.007 ------------------------------------------------------------------------ tee2 is now explicitly exposed in frame initial tee2 will be automatically loaded when needed from /var/aw/var/LatexWiki/TEETWO.NRLIB/TEETWO
TESTSIX abbreviates package test6 ------------------------------------------------------------------------ initializing NRLIB TESTSIX for test6 compiling into NRLIB TESTSIX compiling exported main6 : () -> Integer Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |test6| REDEFINED
;;; *** |test6| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor test6 Time: 0 seconds
finalizing NRLIB TESTSIX Processing test6 for Browser database: --->-->test6(constructor): Not documented!!!! --->-->test6((main6 ((Integer)))): Not documented!!!! --->-->test6(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TESTSIX.NRLIB/TESTSIX.lsp" (written 04 APR 2022 05:49:44 PM):
; /var/aw/var/LatexWiki/TESTSIX.NRLIB/TESTSIX.fasl written ; compilation finished in 0:00:00.007 ------------------------------------------------------------------------ test6 is now explicitly exposed in frame initial test6 will be automatically loaded when needed from /var/aw/var/LatexWiki/TESTSIX.NRLIB/TESTSIX

fricas
main6()

\label{eq2}1(2)
Type: PositiveInteger?

spad
)abbrev package TESTSEV test7
test7(): with
    foo7:tee1 -> tee2
    main7:(tee1, tee2) -> tee2
  == add
    foo7(x) == 5$tee2
    main7(x,y) == foo7(x) + y
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5193838586659015839-25px013.spad
      using old system compiler.
   TESTSEV abbreviates package test7 
------------------------------------------------------------------------
   initializing NRLIB TESTSEV for test7 
   compiling into NRLIB TESTSEV 
   compiling exported foo7 : tee1 -> tee2
****** comp fails at level 1 with expression: ******
error in function foo7 
((|Sel| (|tee2|) 5)) ****** level 1 ****** $x:= (Sel (tee2) 5) $m:= (tee2) $f:= ((((|x| # #) (|main7| #) (|foo7| #) (|$DomainsInScope| # # #) ...)))
>> Apparent user error: unspecified error

Would you have expected a compile error with test7? This shows there is no automatic coercion in the compiler from Integer to tee2.

spad
)abbrev package TESTEGT test8
test8(): with
    foo8:tee1 -> tee2
    main8:(tee1, tee2) -> tee2
  == add
    foo8(x) == 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2
    main8(x,y) == foo8(x) + y
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2052161184486383446-25px014.spad
      using old system compiler.
   TESTEGT abbreviates package test8 
------------------------------------------------------------------------
   initializing NRLIB TESTEGT for test8 
   compiling into NRLIB TESTEGT 
   compiling exported foo8 : tee1 -> tee2
Time: 0 SEC.
compiling exported main8 : (tee1,tee2) -> tee2 Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |test8| REDEFINED
;;; *** |test8| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor test8 Time: 0 seconds
finalizing NRLIB TESTEGT Processing test8 for Browser database: --->-->test8(constructor): Not documented!!!! --->-->test8((foo8 ((tee2) (tee1)))): Not documented!!!! --->-->test8((main8 ((tee2) (tee1) (tee2)))): Not documented!!!! --->-->test8(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TESTEGT.NRLIB/TESTEGT.lsp" (written 04 APR 2022 05:49:44 PM):
; /var/aw/var/LatexWiki/TESTEGT.NRLIB/TESTEGT.fasl written ; compilation finished in 0:00:00.013 ------------------------------------------------------------------------ test8 is now explicitly exposed in frame initial test8 will be automatically loaded when needed from /var/aw/var/LatexWiki/TESTEGT.NRLIB/TESTEGT

Note that tee2 does have a multiplicative unit without requiring a coercion from Integer! So test8 compiles okay. Let's see this in action.

fricas
-- expects 6
main8(1$tee1, 1$tee2)

\label{eq3}6(3)
Type: tee2
fricas
-- expects error
main8(1$tee2, 1$tee1)
There are 1 exposed and 0 unexposed library operations named main8 having 2 argument(s) but none was determined to be applicable. Use HyperDoc Browse, or issue )display op main8 to learn more about the available operations. Perhaps package-calling the operation or using coercions on the arguments will allow you to apply the operation.
Cannot find a definition or applicable library operation named main8 with argument type(s) tee2 tee1
Perhaps you should use "@" to indicate the required return type, or "$" to specify which version of the function you need.

So even the interpreter does not coerce tee1 into tee2. Guess the next three:

fricas
main8(1$Integer, 1$Integer)

\label{eq4}6(4)
Type: tee2
fricas
main8(2$tee1, 5$tee2)

\label{eq5}10(5)
Type: tee2
fricas
main8(3::tee1, (2$tee1)::tee2)
Cannot convert the value from type tee1 to tee2 .

The compiler would not recognize 5$tee2, but the interpreter has no problem coercing any integer automatically to tee1 or tee2. This shows Integer is very special for the interpreter, and not treated the same as tee1.

Let's see if we change the name of foo8 to convert and make the converted value to be 4 instead of 5.

spad
)abbrev package TESTNINE test9
test9(): with
    convert:tee1 -> tee2
    main9:(tee1, tee2) -> tee2
  == add
    convert(x) == 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2
    main9(x,y) == convert(x) + y
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8608886520085933680-25px017.spad
      using old system compiler.
   TESTNINE abbreviates package test9 
------------------------------------------------------------------------
   initializing NRLIB TESTNINE for test9 
   compiling into NRLIB TESTNINE 
   compiling exported convert : tee1 -> tee2
Time: 0 SEC.
compiling exported main9 : (tee1,tee2) -> tee2 Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |test9| REDEFINED
;;; *** |test9| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor test9 Time: 0 seconds
finalizing NRLIB TESTNINE Processing test9 for Browser database: --->-->test9(constructor): Not documented!!!! --->-->test9((convert ((tee2) (tee1)))): Not documented!!!! --->-->test9((main9 ((tee2) (tee1) (tee2)))): Not documented!!!! --->-->test9(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TESTNINE.NRLIB/TESTNINE.lsp" (written 04 APR 2022 05:49:44 PM):
; /var/aw/var/LatexWiki/TESTNINE.NRLIB/TESTNINE.fasl written ; compilation finished in 0:00:00.013 ------------------------------------------------------------------------ test9 is now explicitly exposed in frame initial test9 will be automatically loaded when needed from /var/aw/var/LatexWiki/TESTNINE.NRLIB/TESTNINE

test9 also compiles okay. Let's see this in action. Recall that there is a convert: tee1 -> tee2, but no coerce.

fricas
-- expects 5
main9(1$tee1, 1$tee2)

\label{eq6}5(6)
Type: tee2
fricas
-- expects error
main9(1$tee2, 1$tee1)
There are 1 exposed and 0 unexposed library operations named main9 having 2 argument(s) but none was determined to be applicable. Use HyperDoc Browse, or issue )display op main9 to learn more about the available operations. Perhaps package-calling the operation or using coercions on the arguments will allow you to apply the operation.
Cannot find a definition or applicable library operation named main9 with argument type(s) tee2 tee1
Perhaps you should use "@" to indicate the required return type, or "$" to specify which version of the function you need.

Note convert is not automatically used by the interpreter. Now let's change convert to coerce. Even though there is now a coerce, tee1 is not declared to be CoercibleTo?(tee2) (to do so would have made the two domain constructors different in structure). We use a value 1 this time for coerce.

spad
)abbrev package TESTTEN test10
test10(): with
    coerce:tee1 -> tee2
    main10:(tee1, tee2) -> tee2
  == add
    coerce(x) == 1$tee2
    main10(x,y) == coerce(x) + y
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7317946861256718720-25px019.spad
      using old system compiler.
   TESTTEN abbreviates package test10 
------------------------------------------------------------------------
   initializing NRLIB TESTTEN for test10 
   compiling into NRLIB TESTTEN 
   compiling exported coerce : tee1 -> tee2
Time: 0.01 SEC.
compiling exported main10 : (tee1,tee2) -> tee2 Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |test10| REDEFINED
;;; *** |test10| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor test10 Time: 0.01 seconds
finalizing NRLIB TESTTEN Processing test10 for Browser database: --->-->test10(constructor): Not documented!!!! --->-->test10((coerce ((tee2) (tee1)))): Not documented!!!! --->-->test10((main10 ((tee2) (tee1) (tee2)))): Not documented!!!! --->-->test10(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TESTTEN.NRLIB/TESTTEN.lsp" (written 04 APR 2022 05:49:44 PM):
; /var/aw/var/LatexWiki/TESTTEN.NRLIB/TESTTEN.fasl written ; compilation finished in 0:00:00.010 ------------------------------------------------------------------------ test10 is now explicitly exposed in frame initial test10 will be automatically loaded when needed from /var/aw/var/LatexWiki/TESTTEN.NRLIB/TESTTEN

fricas
-- expects 2
main10(1$tee1, 1$tee2)

\label{eq7}2(7)
Type: tee2
fricas
-- expects error
main10(1$tee2, 1$tee1)
There are 1 exposed and 0 unexposed library operations named main10 having 2 argument(s) but none was determined to be applicable. Use HyperDoc Browse, or issue )display op main10 to learn more about the available operations. Perhaps package-calling the operation or using coercions on the arguments will allow you to apply the operation.
Cannot find a definition or applicable library operation named main10 with argument type(s) tee2 tee1
Perhaps you should use "@" to indicate the required return type, or "$" to specify which version of the function you need.

Now 1$tee1 is automatically coerced to 1$tee2 even though tee1 does not have CoercibleTo?(tee2), but this is the interpreter!

The next thing to do would be to test equivalence of categories. Some other time.




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