Data structures are similar to variables. Algorithms to functions. Objects combine both data and algorithms. Is there a mathematical object / concept that combines variables and functions?

  • $\begingroup$ For "object", there is a simple answer: Coinduction! See Anton Setzer's papers. For object orientation there are a few more features. One is subtyping, which is solved by "Coercive subtyping in type theory" (and similar papers. Of course there is now exact definition of object orientation, so there might be more features depending on who you ask. $\endgroup$
    – mrsteve
    Nov 1 '17 at 3:40

I think you are looking for type theory. It combines mathematical objects and proofs - proofs are constructive, meaning that a proof is an algorithm, consisting of symbolic manipulations.

I am a bit vague on the details, it takes some time to give a proper introduction and it is not my field.

So, in short, type theory and constructive mathematics is what you are looking for. In constructive mathematics, a proposition of the form "there exists an X ..." must also provide an algorithm to construct said X, not just proving its existence.


Not the answer you're looking for? Browse other questions tagged or ask your own question.