Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Calculational Proofs in Relational Graphical Linear Algebra

  • Conference paper
  • First Online:
Formal Methods: Foundations and Applications (SBMF 2020)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12475))

Included in the following conference series:

Abstract

We showcase a modular, graphical language—graphical linear algebra—and use it as high-level language to reason calculationally about linear algebra. We propose a minimal framework of six axioms that highlight the dualities and symmetries of linear algebra, and use the resulting diagrammatic calculus as a convenient tool to prove a number of diverse theorems. Our work develops a relational approach to linear algebra, closely connected to classical relational algebra.

This research was supported by the ESF funded Estonian IT Academy research measure (project 2014-2020.4.05.19-0001). We thank Jason Erbele, Gabriel Ferreira, Lucas Rufino, and Iago Leal for fruitful conversations during various stages of this project.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Arens, R., et al.: Operational calculus of linear relations. Pac. J. Math. 11(1), 9–23 (1961)

    Article  MathSciNet  Google Scholar 

  2. Backhouse, R.: Galois connections and fixed point calculus. In: Backhouse, R., Crole, R., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, pp. 89–150. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-47797-7_4

    Chapter  Google Scholar 

  3. Baez, J., Erbele, J.: Categories in control. Theory Appl. Categ. 30, 836–881 (2015)

    MathSciNet  MATH  Google Scholar 

  4. Bonchi, F., Holland, J., Pavlovic, D., Sobocinski, P.: Refinement for signal flow graphs. In: 28th International Conference on Concurrency Theory (CONCUR 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  5. Bonchi, F., Holland, J., Piedeleu, R., Sobociński, P., Zanasi, F.: Diagrammatic algebra: from linear to concurrent systems. Proc. ACM Program. Lang. 3(POPL), 1–28 (2019)

    Google Scholar 

  6. Bonchi, F., Pavlovic, D., Sobocinski, P.: Functorial semantics for relational theories. arXiv preprint arXiv:1711.08699 (2017)

  7. Bonchi, F., Piedeleu, R., Fabio Zanasi, P.S.: Graphical affine algebra. In: ACM/IEEE Symposium on Logic and Computer Science (LiCS 2019) (2019)

    Google Scholar 

  8. Bonchi, F., Sobociński, P., Zanasi, F.: A categorical semantics of signal flow graphs. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 435–450. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_30

    Chapter  Google Scholar 

  9. Bonchi, F., Sobocinski, P., Zanasi, F.: Full abstraction for signal flow graphs. In: POPL 2015, pp. 515–526. ACM (2015)

    Google Scholar 

  10. Bonchi, F., Sobociński, P., Zanasi, F.: Interacting Hopf algebras. J. Pure Appl. Algebra 221(1), 144–184 (2017)

    Article  MathSciNet  Google Scholar 

  11. Carboni, A., Walters, R.F.: Cartesian bicategories I. J. Pure Appl. Algebra 49(1–2), 11–32 (1987)

    Article  MathSciNet  Google Scholar 

  12. Coddington, E.A.: Extension Theory of Formally Normal and Symmetric Subspaces, vol. 134. American Mathematical Soc. (1973)

    Google Scholar 

  13. Cross, R.: Multivalued Linear Operators, vol. 213. CRC Press, Boca Raton (1998)

    MATH  Google Scholar 

  14. Erbele, J.: Redundancy and zebra snakes. https://graphicallinearalgebra.net/2017/10/23/episode-r1-redundancy-and-zebra-snakes/

  15. Freyd, P.J., Scedrov, A.: Categories, Allegories, vol. 39. Elsevier, Amsterdam (1990)

    MATH  Google Scholar 

  16. Lack, S.: Composing props. Theory Appl. Categ. 13(9), 147–163 (2004)

    MathSciNet  MATH  Google Scholar 

  17. Lawvere, F.W.: Functorial semantics of algebraic theories. Proc. Natl. Acad. Sci. 50(5), 869–872 (1963)

    Article  MathSciNet  Google Scholar 

  18. Mac Lane, S.: An algebra of additive relations. Proc. Natl. Acad. Sci. U. S. A. 47(7), 1043 (1961)

    Article  MathSciNet  Google Scholar 

  19. Mac Lane, S.: An algebra of additive relations. Proc. Natl. Acad. Sci. U. S. A. 47(7), 1043–1051 (1961)

    Article  MathSciNet  Google Scholar 

  20. Macedo, H.D., Oliveira, J.N.: Typing linear algebra: a biproduct-oriented approach. Sci. Comput. Program. 78(11), 2160–2191 (2013)

    Article  Google Scholar 

  21. Mu, S.C., Oliveira, J.N.: Programming from Galois connections. J. Log. Algebraic Program. 81(6), 680–704 (2012)

    Article  MathSciNet  Google Scholar 

  22. Santos, A., Oliveira, J.N.: Type your matrices for great good: a haskell library of typed matrices and applications (functional pearl). In: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell, p. 54–66. Haskell 2020, Association for Computing Machinery, New York (2020). https://doi.org/10.1145/3406088.3409019

  23. Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. LNP, vol. 813, pp. 289–355. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12821-9_4

    Chapter  MATH  Google Scholar 

  24. Sobociński, P.: Graphical linear algebra. Mathematical blog. https://graphicallinearalgebra.net

  25. Zanasi, F.: Interacting Hopf Algebras: the theory of linear systems. Ph.D. thesis, Ecole Normale Supérieure de Lyon (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidade Federal do Rio de Janeiro, Rio de Janeiro, Brazil

    João Paixão

  2. Tallinn University of Technology, Tallinn, Estonia

    Paweł Sobociński

Authors
  1. João Paixão
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paweł Sobociński
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to João Paixão .

Editor information

Editors and Affiliations

  1. Federal University of Pernambuco, Recife, Brazil

    Gustavo Carvalho

  2. Western Norway University of Applied Sciences, Bergen, Norway

    Volker Stolz

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Paixão, J., Sobociński, P. (2020). Calculational Proofs in Relational Graphical Linear Algebra. In: Carvalho, G., Stolz, V. (eds) Formal Methods: Foundations and Applications. SBMF 2020. Lecture Notes in Computer Science(), vol 12475. Springer, Cham. https://doi.org/10.1007/978-3-030-63882-5_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-63882-5_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-63881-8

  • Online ISBN: 978-3-030-63882-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation