A mechanised abstract formalisation of concept lattices. (English) Zbl 1407.68480

Höfner, Peter (ed.) et al., Relational and algebraic methods in computer science. 14th international conference, RAMiCS 2014, Marienstatt, Germany, April 28 – May 1, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8428, 242-260 (2014).
Summary: Using the dependently-typed programming language Agda, we formalise a category of algebraic contexts with relational homomorphisms presented by P. Jipsen [Lect. Notes Comput. Sci. 7560, 195–206 (2012; Zbl 1364.68337)] and M. A. Moshier [“A relational category of polarities” (unpublished draft)]. We do this in the abstract setting of locally ordered categories with converse (OCCs) with residuals and direct powers, without requiring meets (as in allegories) or joins (as in Kleene categories). The abstract formalisation has the advantage that it can be used both for theoretical reasoning, and for executable implementations, by instantiating it with appropriate choices of concrete OCCs.
For the entire collection see [Zbl 1284.68016].


68T30 Knowledge representation
06B23 Complete lattices, completions
18B35 Preorders, orders, domains and lattices (viewed as categories)
68N18 Functional programming and lambda calculus


Zbl 1364.68337
Full Text: DOI