Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by José Nuno Oliveira

2013

Composing Least-change Lenses

Authors
Macedo, N; Pacheco, H; Cunha, A; Oliveira, JN;

Publication
ECEASST

Abstract

2013

WEIGHTED AUTOMATA AS COALGEBRAS IN CATEGORIES OF MATRICES

Authors
Oliveira, JN;

Publication
INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE

Abstract
The evolution from non-deterministic to weighted automata represents a shift from qualitative to quantitative methods in computer science. The trend calls for a language able to reconcile quantitative reasoning with formal logic and set theory, which have for so many years supported qualitative reasoning. Such a lingua franca should be typed, polymorphic, diagrammatic, calculational and easy to blend with conventional notation. This paper puts forward typed linear algebra as a candidate notation for such a unifying role. This notation, which emerges from regarding matrices as morphisms of suitable categories, is put at work in describing weighted automata as coalgebras in such categories. Some attention is paid to the interface between the index-free (categorial) language of matrix algebra and the corresponding index-wise, set-theoretic notation.

2013

Typing linear algebra: A biproduct-oriented approach

Authors
Macedo, HD; Oliveira, JN;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
Interested in formalizing the generation of fast running code for linear algebra applications, the authors show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming. The derivation of fusion, cancellation and abide laws from the biproduct equations makes it easy to calculate algorithms implementing matrix multiplication, the central operation of matrix algebra, ranging from its divide-and-conquer version to its vectorization implementation. From errant attempts to learn how particular products and coproducts emerge from biproducts, not only blocked matrix algebra is rediscovered but also a way of extending other operations (e.g. Gaussian elimination) blockwise, in a calculational style, is found. The prospect of building biproduct-based type checkers for computer algebra systems such as MATLAB (TM) is also considered.

2015

A linear algebra approach to OLAP

Authors
Macedo, HD; Oliveira, JN;

Publication
FORMAL ASPECTS OF COMPUTING

Abstract
Inspired by the relational algebra of data processing, this paper addresses the foundations of data analytical processing from a linear algebra perspective. The paper investigates, in particular, how aggregation operations such as cross tabulations and data cubes essential to quantitative analysis of data can be expressed solely in terms of matrix multiplication, transposition and the Khatri-Rao variant of the Kronecker product. The approach offers a basis for deriving an algebraic theory of data consolidation, handling the quantitative as well as qualitative sides of data science in a natural, elegant and typed way. It also shows potential for parallel analytical processing, as the parallelization theory of such matrix operations is well acknowledged.

2017

The data cube as a typed linear algebra operator

Authors
Oliveira, JN; Macedo, HD;

Publication
ACM International Conference Proceeding Series

Abstract
There is a need for a typed notation for linear algebra applicable to the ields of econometrics and data mining. In this paper we show that such a notation exists and can be useful in formalizing and reasoning about data aggregation operations. One such operation - the construction of a data cube - is shown to be easily expressible as a linear algebra operator. The construction is shown to be type-generic and some of its properties are derived from its typed deinition and proved using matrix algebra. Other forms of data aggregation such as eg. rollup and cross tabulation are shown to be algebraically derivable from data cubes. © 2017 Association for Computing Machinery.

2013

Alloy Meets the Algebra of Programming: A Case Study

Authors
Oliveira, JN; Ferreira, MA;

Publication
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING

Abstract
Relational algebra offers to software engineering the same degree of conciseness and calculational power as linear algebra in other engineering disciplines. Binary relations play the role of matrices with similar emphasis on multiplication and transposition. This matches with Alloy's lemma "everything is a relation" and with the relational basis of the Algebra of Programming (AoP). Altogether, it provides a simple and coherent approach to checking and calculating programs from abstract models. In this paper, we put Alloy and the Algebra of Programming together in a case study originating from the Verifiable File System mini-challenge put forward by Joshi and Holzmann: verifying the refinement of an abstract file store model into a journaled (FLASH) data model catering to wear leveling and recovery from power loss. Our approach relies on diagrams to graphically express typed assertions. It interweaves model checking (in Alloy) with calculational proofs in a way which offers the best of both worlds. This provides ample evidence of the positive impact in software verification of Alloy's focus on relations, complemented by induction-free proofs about data structures such as stores and lists.

  • 1
  • 3