Re: Pure Functions?

Dear Henry,

I put Ben in cc, because I think he could also be interested in discussions about the function ontology (as a side-note: I think I already had a similar discussion with him in the past about functions and partial functions, he will remember :) ).

Here in the group, we discussed the function ontology as a possible way to formally describe built-in functions, but since there are other aspects open, this discussion has been postponed (but maybe someone reading this mail is willing to volunteer and write some specifications? :) ).



 I have been working a bit recently with the function ontology https://fno.io/

and was wondering if one could not have a pure function ontology subset of it.

I also think it would be nice to have pure function ontology, especially if we want to describe built-ins: we should be able to say that two implementations of the sum function need to come to the same conclusion when, for example, being confronted with the values 2 and 4 (like in the example: https://fno.io/spec/#fn-returns). For our built-in functions it would not be acceptable when one result is 6 and one is 8. Yet, the problem of „equality“ is a little bit more complicated here: is "6"^^xsd:integer the same as „06"^^xsd:integer or "6"^^xsd:double? We could consider these solutions as equivalent and then see the equivalence classes as solutions. Of course these classes could not contain general error values ("time out" should not be equivalent to „4“ AND „6“).

I think one problem we have here is that there is a difference between the expected output and the output of  a particular execution. One could for example still argue, that if we see the implementation, the current time and the input values as the actual input argument of the function then this function is still functional because it returns one single result (as time evolves, it is totally possible that we keep getting new random results from our function). Of course our description would become meaningless at some point.

From what I see, it might be possible to simply add something like fno:CorrectOutput  as a counter part to fno:Output where we specify what we expect as opposed to what we get from the execution of a function. But I would not be surprised if Ben had a better solution for that? Do you work with shapes here, Ben?


There is a nice mapping between the category Rel of sets and relations and the
category Set of Sets and functions (somewhere in David Spivak’s work on the subject).
I think all one needs is a relation from an functional property its restricted domain,
to get a function.

I did not read the work yet, but I would also say that this would be a way to get a function. So, if you would go here https://fno.io/spec/#example-generatedID-6 and consider the example, would you then propose to make the predicate ex:sumResult functional? I think this would be problematic since it could happen that one execution of a function returns an unexpected result (8 from above or simply ERROR). We again have two different aspects: the result of a mathematical function and  the result of a concrete execution. Ideally, these do not differ. In practice, they sometimes do


It seems like having that could help clarify the function ontology. So I wrote it
up here

https://github.com/FnOio/fno-specification/issues/7


But then I also get the feeling that this was thought of before, and
that there was an issue that came up.  I am asking here as I think the
experts that know should be here :-)

I think this is not only a discussion for the N3 group as possible customers and also providers of formalisms, but also something for the creators of fno. So I’dlike to ask you directly, Ben, would you want fno to be used to describe functions from a mathematical point of view (if so, I believe Henry and I would be happy to help :)) or would you see that (for now) beyond the scope of fno and say it focusses more on concrete executions?

Kind regards,
Dörthe




Henry Story

https://co-operating.systems

WhatsApp, Signal, Tel: +33 6 38 32 69 84‬
Twitter: @bblfish