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

Edit detail for SandBox SPAD dependent types revision 1 of 1

1
Editor: ric
Time: 2018/06/20 16:00:37 GMT+0
Note: SPAD does NOT support types that depend on preceding formal parameters in function declarations

changed:
-
** Notations **

\begin{axiom}
M ==> SquareMatrix
I ==> Integer
N ==> NonNegativeInteger

-- setting up a 2x2 matrix with entries in the ring of integers
m0 : M(2,I) := matrix [[1, 2], [3, 4]]

-- and a 3x3 matrix with entries in the ring of  2x2 matrices of integers
mm0 : M(3,M(2,I)):= matrix [[m0, m0^2, m0^3], [m0^4,m0^5,m0^6],[m0^7,m0^8,m0^9]]
\end{axiom}

**PROBLEM: (?Unlike Aldor) SPAD/FriCAS 1.3.3 does NOT support types that depend on preceding formal parameters in function declarations: **

\begin{axiom}
fun( ndim:N, m:M(ndim,I) ):M(ndim, I) == m-m^3
\end{axiom}

Let us try to find out some alternative approaches...

**Approach: multiple function definitions, each with a different value of n: WORKS, but with unpleasant code repetition**

\begin{axiom}
fun2(m:M(2,I)):M(2, I) == m-m^3
fun3(m:M(3, M(2, I))):M(3, M(2, I)) == m-m^3

fun2(m0)
fun3(mm0)
\end{axiom}

**Approach: multiple specializations of the same function fun with different values of n. DOES NOT WORK**

\begin{axiom}
fun(2:N, m:M(2,I)):M(2, I) == m-m^3

fun(3:N, m:M(3, M(2, I))):M(3, M(2, I)) == m-m^3

fun(2,m0) -- "WRONG" RESULT: definition of fun(2,...) has been overwritten by fun(3,...) and m0 has been promoted to a diagonal 3x3 matrix.

fun(3,mm0)
\end{axiom}

**Approach: funMaker, a function that returns an anonymous function. ERROR because a value-dependent return type for funMaker is needed**

\begin{axiom}
funMaker(n:N,R:Ring):(M(n,R)->M(n,R)) == (m:M(n,R)):M(n,R) +-> m-m^3
fu2 := funMaker(2,I)
fu2(m0)
fu3 := funMaker(3,M(2,I)
fu3(mm0)
\end{axiom}


**Approach: %funMaker, a macro that returns an anonymous function: WORKS and requires minimal code writing.**

\begin{axiom}
macro %funMaker(n,R) == (m:M(n,R)):M(n,R) +-> m-m^3

ff2 := %funMaker(2, I)
ff3 := %funMaker(3, M(2,I))

ff2(m0)
ff3(mm0)
\end{axiom}

Notations

fricas
(1) -> M ==> SquareMatrix
Type: Void
fricas
I ==> Integer
Type: Void
fricas
N ==> NonNegativeInteger
Type: Void
fricas
-- setting up a 2x2 matrix with entries in the ring of integers
m0 : M(2,I) := matrix [[1, 2], [3, 4]]

\label{eq1}\left[ 
\begin{array}{cc}
1 & 2 
\
3 & 4 
(1)
Type: SquareMatrix?(2,Integer)
fricas
-- and a 3x3 matrix with entries in the ring of  2x2 matrices of integers
mm0 : M(3,M(2,I)):= matrix [[m0, m0^2, m0^3], [m0^4,m0^5,m0^6],[m0^7,m0^8,m0^9]]

\label{eq2}\left[ 
\begin{array}{ccc}
{\left[ 
\begin{array}{cc}
1 & 2 
\
3 & 4 
(2)
Type: SquareMatrix?(3,SquareMatrix?(2,Integer))

PROBLEM: (?Unlike Aldor) SPAD/FriCAS 1.3.3 does NOT support types that depend on preceding formal parameters in function declarations:

fricas
fun( ndim:N, m:M(ndim,I) ):M(ndim, I) == m-m^3
Cannot convert the value from type Symbol to NonNegativeInteger .

Let us try to find out some alternative approaches...

Approach: multiple function definitions, each with a different value of n: WORKS, but with unpleasant code repetition

fricas
fun2(m:M(2,I)):M(2, I) == m-m^3
Function declaration fun2 : SquareMatrix(2,Integer) -> SquareMatrix( 2,Integer) has been added to workspace.
Type: Void
fricas
fun3(m:M(3, M(2, I))):M(3, M(2, I)) == m-m^3
Function declaration fun3 : SquareMatrix(3,SquareMatrix(2,Integer)) -> SquareMatrix(3,SquareMatrix(2,Integer)) has been added to workspace.
Type: Void
fricas
fun2(m0)
fricas
Compiling function fun2 with type SquareMatrix(2,Integer) -> 
      SquareMatrix(2,Integer)

\label{eq3}\left[ 
\begin{array}{cc}
-{36}& -{52}
\
-{78}& -{114}
(3)
Type: SquareMatrix?(2,Integer)
fricas
fun3(mm0)
fricas
Compiling function fun3 with type SquareMatrix(3,SquareMatrix(2,
      Integer)) -> SquareMatrix(3,SquareMatrix(2,Integer))

\label{eq4}\left[ 
\begin{array}{ccc}
{\left[ 
\begin{array}{cc}
-{17874987357356}& -{26051491125412}
\
-{39077236688118}& -{56952224045474}
(4)
Type: SquareMatrix?(3,SquareMatrix?(2,Integer))

Approach: multiple specializations of the same function fun with different values of n. DOES NOT WORK

fricas
fun(2:N, m:M(2,I)):M(2, I) == m-m^3
Function declaration fun : (NonNegativeInteger, SquareMatrix(2, Integer)) -> SquareMatrix(2,Integer) has been added to workspace.
Type: Void
fricas
fun(3:N, m:M(3, M(2, I))):M(3, M(2, I)) == m-m^3
Function declaration fun : (NonNegativeInteger, SquareMatrix(3, SquareMatrix(2,Integer))) -> SquareMatrix(3,SquareMatrix(2, Integer)) has been added to workspace.
Type: Void
fricas
fun(2,m0) -- "WRONG" RESULT: definition of fun(2,...) has been overwritten by fun(3,...) and m0 has been promoted to a diagonal 3x3 matrix.
fricas
Compiling function fun with type (NonNegativeInteger, SquareMatrix(3
      ,SquareMatrix(2,Integer))) -> SquareMatrix(3,SquareMatrix(2,
      Integer))

\label{eq5}\left[ 
\begin{array}{ccc}
{\left[ 
\begin{array}{cc}
-{36}& -{52}
\
-{78}& -{114}
(5)
Type: SquareMatrix?(3,SquareMatrix?(2,Integer))
fricas
fun(3,mm0)

\label{eq6}\left[ 
\begin{array}{ccc}
{\left[ 
\begin{array}{cc}
-{17874987357356}& -{26051491125412}
\
-{39077236688118}& -{56952224045474}
(6)
Type: SquareMatrix?(3,SquareMatrix?(2,Integer))

Approach: funMaker, a function that returns an anonymous function. ERROR because a value-dependent return type for funMaker is needed

fricas
funMaker(n:N,R:Ring):(M(n,R)->M(n,R)) == (m:M(n,R)):M(n,R) +-> m-m^3
Cannot convert the value from type Symbol to NonNegativeInteger .

Approach: %funMaker, a macro that returns an anonymous function: WORKS and requires minimal code writing.

fricas
macro %funMaker(n,R) == (m:M(n,R)):M(n,R) +-> m-m^3
Type: Void
fricas
ff2 := %funMaker(2, I)

\label{eq7}\mbox{theMap (...)}(7)
Type: (SquareMatrix?(2,Integer) -> SquareMatrix?(2,Integer))
fricas
ff3 := %funMaker(3, M(2,I))

\label{eq8}\mbox{theMap (...)}(8)
Type: (SquareMatrix?(3,SquareMatrix?(2,Integer)) -> SquareMatrix?(3,SquareMatrix?(2,Integer)))
fricas
ff2(m0)

\label{eq9}\left[ 
\begin{array}{cc}
-{36}& -{52}
\
-{78}& -{114}
(9)
Type: SquareMatrix?(2,Integer)
fricas
ff3(mm0)

\label{eq10}\left[ 
\begin{array}{ccc}
{\left[ 
\begin{array}{cc}
-{17874987357356}& -{26051491125412}
\
-{39077236688118}& -{56952224045474}
(10)
Type: SquareMatrix?(3,SquareMatrix?(2,Integer))