Skip to content

TODO.org

Latest commit

 

History

History
94 lines (71 loc) · 3.4 KB

TODO.org

File metadata and controls

94 lines (71 loc) · 3.4 KB

Book “dry-run” presentation slot in the week 2016-05-09/13

Prepare a presentation for TYPES 2016

Book trip to TYPES

Book hotel for TYPES

try to find a scholarship to apply for travel funding

Register for TYPES

Submit final version of the abstract

Kanske citera: http://www.cs.cornell.edu/~kozen/papers/kacs.pdf

Future work

Look at empty shapes

perhaps add an empty shape (but probably in a separate experiment file because many things change in the matrix representation).

Implement matrix determinant (with block matrices)

there is a block matrix decomposition of the determinant:

det(A B ; C D) = det(A)det(D - CA-1B) (requires A to be invertible)

A is invertible when: https://en.wikipedia.org/wiki/Invertible_matrix#Blockwise_inversion

Generalised determinants:

Determinants that work with matrices over things that are noncommutative:

  • Dieudonné determinant: matrices over division rings
  • Quasideterminant: still needs negation and inversion

Make easier matrices

fromVec : ∀ {a} sh sh2 → Vec a (toNat sh * toNat sh2) → M a sh sh2 ?

Read “Fun with semirings”

https://www.cl.cam.ac.uk/~sd601/papers/semirings.pdf

Block matrices and algorithms using them. Closed semirings (closed rigs).

2015-12-01: Prioritet 2!

Graph algorithms, is the 1 essential for them to work?

Read “Typing linear algebra: a biproduct-oriented approach”

http://arxiv.org/pdf/1312.4818v1.pdf

The category Mat_K over some structure K (a Rg in this setting, ring w/o multiplicative identity and negation).

“Abelian category” / “Category R-Mod of modules over some ring R”

(intuition: modules: generalised vector spaces, linear maps (arrows between vector spaces) are matrices?)

objects: shapes arrows: $r <- c$: matrices M K r c composition: matrix multiplication identities: square (identity) matrices $a <- a$

  • m : r <- c, id : c <- c. m . id : r <- c
  • m : r <- c, id : r <- r. id . m : r <- c

What kind of category does adding the closure make?

Sätt igång med “rapport”

(baserat på mall från https://github.com/patrikja/skeleton)

2015-12-01: Prioritet 1!

Try to implement closure (either penetrate the ValiantAgda version or roll your own)

What is a closed seminearring? for a semiring closure satisfies $a^* = 1 + a ∙ a^*$, but in seminearring there is no 1…

$a^+ = a + a^+ ∙ a^+$ <— (“quadratic equation” in ValiantAgda)

Complete “Square snr (B shape shape₁)”

Do some of the proofs (isCommMon; zeroˡ; zeroʳ; <∙>)

lifting commutative monoid works for non square shapes?

Redo the Seminearring for non-square matrices (and define square as a special case on the outside)