An Internal Language for Categories Enriched over Generalised
Metric Spaces
University of Minho
Abstract: Programs with a continuous state space or that interact
with physical processes often require notions of equivalence going
beyond the standard binary setting in which equivalence either holds
or does not hold. In this paper we explore the idea of equivalence
taking values in a quantale V, which covers the cases of
(in)equations and (ultra)metric equations among others.
Our main result is the introduction of a V-equational deductive
system for linear λ-calculus together with a proof that it is sound
and complete (in fact, an internal language) for a class of enriched
autonomous categories. In the case of inequations, we get an internal
language for autonomous categories enriched over partial orders. In
the case of (ultra)metric equations, we get an internal language for
autonomous categories enriched over (ultra)metric spaces.
We use our results to obtain examples of inequational and metric
equational systems for higher-order programs that contain real-time and
probabilistic behaviour.