The Logic of Functional Programming(lisp-ai.blogspot.com) |
The Logic of Functional Programming(lisp-ai.blogspot.com) |
If we can peer in to focus in on parts a data structure, we should also be able to focus in on parts of functions. To expose how functions behave relative to parts of structures like those determined by lenses. I describe how commutative squares let you do that. A large assortment of references is provided at the end for interested parties who want to know more.
B/ I have been playing around with the following idea lately; does it correspond to anything nicely explainable in your theory?
If we have a function f (respecting some sort of structure), we can do 3 (6) particularly nice things with it to get more functions:
- f°g precompose with a projection (or a section)
- h°f postcompose with an injection (or a retraction)
- g*°f°g conjugate with a bijection (or the split of an idempotent)1. precomposition: with precomposition you should use a function pair (h, 1_b) that has an identity for the second part to form a morphism m: fg -> f like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFswL...
2. postcomposition: with postcomposition you should use a function pair (1_b, k) that has an identity for the first part to form a morphism m: f -> hf like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFsyL...
3. conjugation: with conjugation you can actually use an equal function pair (g,g) to get a morphism from a function f to its conjugate gfg^{-1}. Then we see that this forms a commutative square for gfg^{-1}g = gf. Thusly, there is always a morphism from any function to its conjugate by a bijection like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQSJdLFswL...
Therefore, I would say that precomposition, postcomposition, and conjugation form special types of morphisms between functions defined by special properties like having one function be the identity or having both functions be equal to one another. Then beyond that we can classify these morphisms by rather or not their components are projections, injections, or bijections to get towards what you are speaking about. This all fits in to the perspective that functions are objects in Sets^(->), so that is nice.
I can't say I've ever used APL but I have heard of it. It has some very interesting syntax and notation, but I have made it far enough to actually try it out yet.
As a double-check, to get precomposition m : f -> fg like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFswL... ?
The property that Sets^(->) is a topos gives us a lot to work with. All impredicative constructive mathematics can be defined internal to Sets^(->). This is interesting because it means almost all mathematics can be done internal to Sets^(->), with functions instead of sets as its first class logical objects.
Secondly, the fact that it is a topos gives us an internal logic in Sets^(->). The internal logic of Sets^(->) is a trivalent logic with three values: true, false, and half truth that fails to satisfy the law of excluded middle. Sets^(->) has its own distinct system of logical operators and connectives which generalize those in classical logic and that can be used on all subobjects.
All aside from that, Sets^(->) has an incredibly remarkable logic of quotients. It has been shown that the dual logic of quotients in Sets^(->) is intuitively similar to the partition pairs construction of Hartmanis and Stearns in Algebraic Structure Theory of Sequential Machines (1966). So the immense power of the topos Sets^(->) is enough to capture their central construction for creating a computational structure theory, and mine.
All this demonstrates that Sets^(->) by itself has an incredibly rich theory which is worthy of further exploration. The theory of Sets^(->) is really the functional counterpart of set theoretic foundations, a foundation for a different kind of function-based mathematics, and the means by which we can create a system of logical reasoning for functional programs.
[1] https://ncatlab.org/nlab/show/topos
[2] https://ncatlab.org/nlab/show/internalization
[3] https://ncatlab.org/nlab/show/internal+logic
[4] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.