Add relation properties FUN(ctional) and BIJ(ective)

[jesper-sk]

Is your feature request related to a problem? Please describe.

Not related to a problem, but I expect its implementation adds to conciseness, readability and understandability of RELATION-statements.

Describe the solution you'd like

To the properties-part of a RELATION-statement, add the properties BIJ and FUN, as shortcuts for the property combinations INJ + SUR and UNI + TOT and indicating bijective and functional relations, respectively.

Describe alternatives you've considered

The obvious alternative is to just specify r [A * B] [INJ, SUR] or r [A * B] [UNI, TOT] instead of using the proposed shortcuts. But, considering that functional and bijective are well-known as well as commonly occurring binary relations, I believe that adding these shortcuts is warranted.

[hanjoosten]

Hi Jesper, thanks for the idea. I like it, and it should be pretty easy to implement. @stefjoosten , what do you think?

[stefjoosten]

Sure. Good idea! This one is easy:

• Augment the P-structure with Bij and Fun and adapt the parser to accept BIJ and FUN, to have Ampersand accept this notation.
• In the transformation of the P-structure to the A-structure, transform Fun to Uni and Tot and transform Bij to Inj, and Sur, so that Fun and Bij are resolved. As a consequence, Fun and Bij do not occur in the A-structure. PROP can serve as a good example. It is syntactical sugar for SYM and ASY.
• In FormalAmpersand, do the same, using enforcement rules, to ensure the proper functioning of Simon's Atlas.
  I think that should do the trick... 🙂

[stefjoosten]

Reflection

@jesper-sk , a bijection is a function, so Uni, Tot, Inj, and Sur. So it differs from an inverse function, which is just Inj and Sur.

In the past, we used to have a special syntax for functions, with an arrow between the source and target concepts. We removed that syntax because having two syntaxes for exactly the same thing confused our students a lot. That is why we only have the syntax RELATION r[A*B] for declaring relations.

[jesper-sk]

Reflection

@jesper-sk , a bijection is a function, so Uni, Tot, Inj, and Sur. So it differs from an inverse function, which is just Inj and Sur.

@stefjoosten My assumption was that the bijective property (so no bijection) can also be attributed to relations (meaning an injective and surjective relation, but not necessarily a function). So similar to the difference between e.g. injective relations and an injection (i.e. injective function). But I haven't seen it used as such, and maybe calling this property bijective adds too mutch confusion.

Would you prefer calling the INJ + SUR shortcut something related to an inverse function instead? Something like NUF or IFU?

[stefjoosten]

@jesper-sk, I think your storyline is sound. In mathematics, a bijection is a function that is both injective and surjective. Consequently, we can define a bijective relation as a relation that is both injective and surjective. To distinguish the words bijection and bijective makes all the difference. Since Ampersand defines the notations TOT, INJ, SUR, and UNI as adjectives, it makes sense to define FUN and BIJ to mean functional and bijective respectively.

I have discussed this with @hanjoosten and I am consulting some real mathematicians to see if we are doing anything strange, because I want Ampersand to be 100% consistent with mathematically accepted language. (In a quick scan, authoritative locations on the internet do not contradict this storyline, but don't give conclusive answers either.)

So for now, we'll implement BIJ as a shorthand for INJ and SUR, also because I like the symmetry w.r.t. FUN. Unless the mathematicians can convince me that this definition contradicts mathematical language conventions, this is what it will be.

Aside

This discussion is also conducted on math.stackexchange.com.