help links subscribe changes refresh edit

	SandBox
SandBox Risch ←	↑	→ SandBox Set Any

SandBox SPAD dependent types

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))