agda
Functional Relation
As far as I searched, there are no definitions about functional (binary) relations, e.g.
Functional R = ∀ x {y z} → R x y → R x z → y ≈ z
Computable R = ∀ x → ∃[ y ] R x y
Surjective R = ∀ y → ∃[ x ] R x y
Injective R = ∀ x y z → R x z → R y z → x ≈ y
and so on. This would be useful to define a function before showing its termination, and proving its termination in a step-by-step way.
Looks like a good idea, but as with the refactoring of Function.Definitions (esp. regarding Surjective), it might/probably will be worth generalising these definitions arbitrary equalities, and relations R which are suitably 'respectful' of such...?
Computable is also perhaps a debatable name, but Defined/Entire/Total aren't much better, esp. the last, currently already much debated in a separate context... #453 , which moreover draws attention to characterisation of such concepts wrt the abstract (bicategorical/profunctorial) algebra of relations...
Regarding Surjective, I do not see an alternative definition for that. Could you please provide such a definition?
For Injective, I think the following definition would be good enough for me:
Injective R = ∀ x y z w → x ∼ y → R x z → R y w → z ≈ w
(or even the one taking _∼_ and _≈_ as arguments)
For Computable, an alternative name I had was LeftTotal. I think in this case the word "Total" is more acceptable because the word "Total function" is more widely used. One reason against "LeftTotal" is that the sigma type actually gives us a way to compute y, not just stating that there (classically) exists a y.
I think your revised definition of Injective should be
Injective R = ∀ x y z w → z ≈ w → R x z → R y w → x ∼ y
As for Surjective, something like
Surjective R = ∀ y → ∃ λ x → ∀ {z} → z ∼ x → R z y
but I think it perhaps also might require R respects _≈_ in the second argument position?
Oh right, I miswrote Injective. Actually the definition I used should be the definition of Functional w.r.t. those equivalences:
Functional R = ∀ x y z w → x ∼ y → R x z → R y w → z ≈ w
If you think adding the respectful condition would be better, we can use
FunctionalLike R = ∀ x y z w → x ∼ y → R x z → R y w → z ≈ w
Functional R = FunctionalLike R × R Respectsˡ _∼_ × R Respectsʳ _≈_
I like the first definition of Functional (wrt _∼_ and _≈_) above; the second makes me worry that my suggestion to build-in Respects could get very painful very quickly!
I think the test of a good definition should be what you can use it for, and how easily/'smoothly' that works out in practice.
Specifically, what I have in mind is defining partial algebraic structures, e.g. partial monoid and so on. These are useful tools for mechanizing substructural calculi such as the linear lambda calculus or adjoint calculus.
The 'design space' of partial algebraic structures in the type theory that agda-stdlib chooses to use is... non-trivial. I'll summon @TOTBWF as he's been forced to think about this quite a lot in the last few months. All sorts of reasonable-looking definitions end up being rather un-ergonomic.
Thanks @JacquesCarette I nevertheless agree with @Ailrun that the function-as-relation, implementation-meets-specification as relation-inclusion perspective is simple, powerful, and under explored in the library (I've just been teaching this through the medium of Rocq to our undergrads)
So I welcome this, but as I've said above, nevertheless in a form which fits the grain of what we already have.
Oh, absolutely, that perspective is all those things (simple, powerful and under explored in stdlib). I think the issue at the top makes sense to deal with. My only comment was that extending this to partial algebraic structures is seriously non-trivial.
In other words: the concrete cases of defining various functions as functional-relations (etc) is very powerful. Figuring out what interfaces these have in common is hard. Especially since, in that 'functional relation' paradigm, things are not actually partial!