FLABloM: Functional linear algebra with block matrices

Associated material for some work on block based matrix representation in Agda. We lift various algebraic structures (semi-near-rings, semi-rings and closed semi-rings) to matrices in order to verify algorithms that can be implemented using the closure operation in a semi-ring.

TyDe 2016: Type-driven Development

• Extended abstract accepted for TyDe 2016: "An Agda Formalisation of the Transitive Closure of Block Matrices (Extended Abstract)"
  • preprint
• This work was partially supported by the projects GRACeFUL (grant agreement No 640954) and CoeGSS (grant agreement No 676547), which have received funding from the European Union’s Horizon 2020 research and innovation programme.

@inproceedings{SandbergEriksson:2016:AFT:2976022.2976025,
  author =       {Sandberg Eriksson, Adam and Jansson, Patrik},
  title =        {An Agda Formalisation of the Transitive Closure of
                  Block Matrices (Extended Abstract)},
  booktitle =    {Proceedings of the 1st International Workshop on
                  Type-Driven Development},
  series =       {TyDe 2016},
  year =         2016,
  isbn =         {978-1-4503-4435-7},
  location =     {Nara, Japan},
  pages =        {60--61},
  numpages =     2,
  url =          {http://doi.acm.org/10.1145/2976022.2976025},
  doi =          {10.1145/2976022.2976025},
  acmid =        2976025,
  publisher =    {ACM},
  address =      {New York, NY, USA},
  keywords =     {Dependent types, Functional Programming, Linear
                  Algebra},
}

TYPES 2016 presentation

• Title: "FLABloM: Functional linear algebra with block matrices"
• Extended abstract
• Accepted for presentation at TYPES 2016.
• Conf. pres.: Thursday 2016-05-26 at 15.00 -- slides
• (Dry-run: Friday 2016-05-19 at 11.00 in EDIT-6128, Chalmers)

Overview

The development is structured using a hierarchy of Agda records implementing semi-near-rings, semi-rings and closed semi-rings.

• Preliminaries

  • Preliminaries.lagda -- some definitions, borrowed from ValiantAgda.
  • Product.lagda -- non-dependent product.

• Structures

  Agda records for our ring hierarchy.

  • SemiNearRingRecord.lagda
  • SemiRingRecord.lagda
  • ClosedSemiNearRingRecord.lagda
  • ClosedSemiRingRecord.lagda

• Matrix

  • Shape.lagda -- datatype of matrix dimensions
  • Matrix.lagda -- datatype of matrices

• Rings

  • BoolRing.lagda -- Bool as a closed semi-ring
  • TropicalRing.lagda -- ℕ + ∞ as a closed semi-ring

• Matrices as rings

  Lifts some ring structure to a matrix ring of said structure

  • LiftSNR.lagda -- Lift semi-near-rings
  • LiftSR.lagda -- Lift semi-rings
  • LiftCSNR.lagda -- Lift closed semi-near-rings (not finished)
  • LiftCSR.lagda -- Lift closed semi-rings

• Documentation

  • abstract.lagda -- abstract submitted to TYPES 2016
  • paper.lagda -- unfinished technical report (longer version of abstract)
  • slides.lagda -- slides used for presentation at TYPES 2016 and WG2.1 meeting 2016

Project course instance at Chalmers

Project title: "FLABloM: Functional Linear Algebra with Block Matrices"

A project instance of DAT235 - Research-oriented special course for Adam SE during study period 2 (Nov-Dec), 2015.

Builds on courses

Discrete mathematics, Linear algebra, Advanced functional programming, Types for programs and proofs.

Project summary

A recent paper by Bernardy and Jansson has explored Parallel Parsing formulated in terms of matrix algebra. The formulation is based on a recursive decomposition of "large" matrices into 2x2 block matrices which enables short and concise algorithm formulation, sparse matrix representation and simplified proofs of correctness. The aim of this project is to explore to what degree this idea can be back-ported to classical linear algebra with the aim to influence the DSLsofMath course.

ValiantAgda Code: https://github.com/DSLsofMath/ValiantAgda