Open jesper-sk opened 1 week ago
Hi Jesper, thanks for the idea. I like it, and it should be pretty easy to implement. @stefjoosten , what do you think?
Sure. Good idea! This one is easy:
PROP
can serve as a good example. It is syntactical sugar for SYM and ASY.@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.
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?
@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.
This discussion is also conducted on math.stackexchange.com.
This feature has been added in the branch Add-prop-BIJ-FUN .
This branch is a derivative of the ATLAS-import branch still running on Ampersand 4, which prevents pushing the functionality to the main branch. As a result, this feature will only become accessible when the ATLAS-import branch is converted to/implemented in Ampersand 5.
@Stefjoosten has consulted @WolframKahl about this issue. The details of that will be included in this discussion by @stefjoosten as soon as he has got time for this.
An outcome of this discussion was that a function could be only injective: The well-known partial function. What we intend here with function is called a mapping, which is a relation that is total and injective. So I substituted the keyword "FUN" by the keyword "MAP", to reflect that.
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
andFUN
, as shortcuts for the property combinationsINJ + SUR
andUNI
+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]
orr [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.