4 ms·

If you have a math-background, category theory is easy to learn, as it's merely a trivial (in retrospect, but not in prospect) generalisation of existing mathem

If you have a math-background, category theory is easy to learn, as it's merely a trivial (in retrospect, but not in prospect) generalisation of existing mathematics. It's basically the abstract theory of binary associative 'thingies' and 'functions' that preserve these 'thingies'. Most mathematicians pick it up by osmosis without really trying. That's because they understand so well what CT abstracts from. Experience has shown that without a maths background learning CT is extremely difficult. Almost everybody basically fails. As somebody who taught himself CT without a math background, I suggest to expect between 100 and 300 hours of serious, intensive study before CT begins to make sense. My recommendation is to bite the bullet and study one of the many good textbooks, and solve every exercise, and rote-learn the definitions until they become second nature. You will know you've understood CT when see why Peter Freyd's quip "[t]he purpose of [category theory] is to show that which is trivial is trivially trivial" is apt. The key concepts to learn are: category, functor, natural transformation, adjunction, universal property, limit and dualisation. Once you understand those, an extremely large number of prima facie separate mathematical concepts can be seen as instances of the same few trivial ideas. But they must be rephrased in this seemingly alien and unnatural language called CT. My favourite example is Lawvere's unification of most known paradoxa (e.g. Cantor, Russell, Goedel, Tarski) as a basically a trivial fixpoint [1]. Note that after Lawvere had realised what most paradoxa have in common using a categorical re-formulation, it then became trivial to get the same insight without CT [2]. Let me illustrate the power of looking at a phenomenon using a new language with the example of computation itself: we have two dominant abstractions of computation: - Turing machines - Lambda calculus Simplifying only a tiny bit: Turing machines gave us the theory of computational complexity but has not been helpful at all in the development of programming languages in general, and typing systems in particular; in contrast, lambda-calculus has been the foundation of most work on programming languages in general and practically all work on types. Yet lambda-calculus has been mostly silent on complexity theory (although [3] is the beginning of a rapprochement). Finally, let me state my belief that the average programmer has currently no need to understand CT. The main categorical concept that has filtered down to conventional programming are monads, and monads can be explained and understood completely without reference to CT. [1] F. W. Lawvere, Diagonal arguments and cartesian closed categories. [2] N. S. Yanofsky, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points. [3] https://arxiv.org/abs/1601.01233 https://arxiv.org/abs/1601.01233

hackernewsacct 9y ago
Can you explain the fixed point idea more in a beginner way? I'm curious to understand the result.
- vorotato 9y ago
  A function has a fixed point when for some value of x, x = f(x). This is interesting because it's some change, that doesn't change the result. in the lingua franca of javascript. var timesThree = (x => x * 3) //for this function 0 is a fixed point... var a = 0 console.log(a == timesThree(a)) //7 is not a fixed point var b = 7 console.log(b == timesThree(b))
  - hackernewsacct 9y ago
    Thanks for the response. My question is how does fixed point relate to the incomplete theorems and decidability?
    - darkinvisible 9y ago
      The key to e.g. Goedel's results is the Fixed Point Lemma: if ψ is a formula with v free then there is a sentence φ such that, provably, φ <=> ψ(<φ>) [where <..> is the numerical code of .. ]. The proof, if you are interested, is not difficult. Let sub be the function that describes, via codes, substituting the (numeral n_ of the number) n for a free variable v of a formula χ : sub(<χv>, n_) = <χn_>. Then the PROOF is: consider ψ(sub(v,v)), call it θv, let m be <θv> and let φ be θm_. Then, provably, φ <=> ψ(sub(m_,m_)) <=> ψ(sub(<θv>,m_)) <=> ψ(<θm_>) <=> ψ(<φ>). Ta-da! Goedel used this to get the "formula that says I am not provable", φ <=> not Prov(<φ>).
- mafribe 9y ago
  explain the fixed point idea The Yanofsky paper explains is in quite gentle a manner. The key insight behind Lawvere's abstract framework to paradoxa is the the general existence of certain fixpoints. Definition. We say that a set B has the fixpoint property if any function f:B→B has a fixpoint (i.e. f b = b for some b in B). With this convenient definition, we are now ready to state and prove Lawvere's ridiculously simple and yet great theorem. Theorem (Lawvere). If e:A→(A→B) is a surjective function, then B has the fixed point property. The proof is quite easy. Let e:A→(A→B) be surjective. We have to show that B has the fixpoint property. That means for every f:B→B there is b∈B such that f(b)=b. Choose a function f:B→B and define the function g:A→B by setting a ↦ f (e a a) As e is surjective, there must be a0∈A such that e a0 = g. But then immediately f (g a0) = f (e a0 a0) = g a0 Hence g a0 is a fixpoint of f's. Now many/most paradoxa are special cases of Lawvere's theorem. But for each paradox, the specific functions involved are a bit different. Let's look at an example. Theorem (Cantor). There is no surjection e:A→Pow(A). To see why this is true, note that Pow(A) is isomorphic to A→Bool. But there is a function on Bool that has no fixpoints, for example negation ¬:Bool→Bool, contradicting Lawvere's theorem. --------------- What is the intuition behind Lawvere's theorem? At first worrying about A→(A→Bool) is a bit surprising. What does that have to do with paradoxa and self-reference? Well, what does it mean that A can speak about itself? To approach an answer, we could maybe first ask a simpler question: what does it mean to speak about A? How about this for an answer: to speak about A means to say something about A's elements. What does it mean to say something about A's elements? Maybe stating whether any given element a∈A has a property of interest? But what's a property? Easy: a property of A's elements is a function p:A→Bool But we don't want just a fixed property, we want arbitrary properties. To do so, we have to consider the function space A→Bool And how can we turn this into self-reference? What if each element a in A corresponded to a property over A? In other words, (with a lot of handwaving) self-reference means the existence of a surjective function A→(A→Bool) The next step is to wonder: why Bool? Why not any old set? Note that Cantor's theorem continues to hold if we replace Bool with a larger set, but does not hold, if B in A→(A→B) has cardinality 1. What Bool and larger sets have in common is that we can rearrange them, i.e. there is a permuation that doesn't have a fixpoint.

hackernewsacct 9y ago

Can you explain the fixed point idea more in a beginner way? I'm curious to understand the result.

vorotato 9y ago
A function has a fixed point when for some value of x, x = f(x). This is interesting because it's some change, that doesn't change the result. in the lingua franca of javascript. var timesThree = (x => x * 3) //for this function 0 is a fixed point... var a = 0 console.log(a == timesThree(a)) //7 is not a fixed point var b = 7 console.log(b == timesThree(b))
- hackernewsacct 9y ago
  Thanks for the response. My question is how does fixed point relate to the incomplete theorems and decidability?
  - darkinvisible 9y ago
    The key to e.g. Goedel's results is the Fixed Point Lemma: if ψ is a formula with v free then there is a sentence φ such that, provably, φ <=> ψ(<φ>) [where <..> is the numerical code of .. ]. The proof, if you are interested, is not difficult. Let sub be the function that describes, via codes, substituting the (numeral n_ of the number) n for a free variable v of a formula χ : sub(<χv>, n_) = <χn_>. Then the PROOF is: consider ψ(sub(v,v)), call it θv, let m be <θv> and let φ be θm_. Then, provably, φ <=> ψ(sub(m_,m_)) <=> ψ(sub(<θv>,m_)) <=> ψ(<θm_>) <=> ψ(<φ>). Ta-da! Goedel used this to get the "formula that says I am not provable", φ <=> not Prov(<φ>).
mafribe 9y ago
explain the fixed point idea The Yanofsky paper explains is in quite gentle a manner. The key insight behind Lawvere's abstract framework to paradoxa is the the general existence of certain fixpoints. Definition. We say that a set B has the fixpoint property if any function f:B→B has a fixpoint (i.e. f b = b for some b in B). With this convenient definition, we are now ready to state and prove Lawvere's ridiculously simple and yet great theorem. Theorem (Lawvere). If e:A→(A→B) is a surjective function, then B has the fixed point property. The proof is quite easy. Let e:A→(A→B) be surjective. We have to show that B has the fixpoint property. That means for every f:B→B there is b∈B such that f(b)=b. Choose a function f:B→B and define the function g:A→B by setting a ↦ f (e a a) As e is surjective, there must be a0∈A such that e a0 = g. But then immediately f (g a0) = f (e a0 a0) = g a0 Hence g a0 is a fixpoint of f's. Now many/most paradoxa are special cases of Lawvere's theorem. But for each paradox, the specific functions involved are a bit different. Let's look at an example. Theorem (Cantor). There is no surjection e:A→Pow(A). To see why this is true, note that Pow(A) is isomorphic to A→Bool. But there is a function on Bool that has no fixpoints, for example negation ¬:Bool→Bool, contradicting Lawvere's theorem. --------------- What is the intuition behind Lawvere's theorem? At first worrying about A→(A→Bool) is a bit surprising. What does that have to do with paradoxa and self-reference? Well, what does it mean that A can speak about itself? To approach an answer, we could maybe first ask a simpler question: what does it mean to speak about A? How about this for an answer: to speak about A means to say something about A's elements. What does it mean to say something about A's elements? Maybe stating whether any given element a∈A has a property of interest? But what's a property? Easy: a property of A's elements is a function p:A→Bool But we don't want just a fixed property, we want arbitrary properties. To do so, we have to consider the function space A→Bool And how can we turn this into self-reference? What if each element a in A corresponded to a property over A? In other words, (with a lot of handwaving) self-reference means the existence of a surjective function A→(A→Bool) The next step is to wonder: why Bool? Why not any old set? Note that Cantor's theorem continues to hold if we replace Bool with a larger set, but does not hold, if B in A→(A→B) has cardinality 1. What Bool and larger sets have in common is that we can rearrange them, i.e. there is a permuation that doesn't have a fixpoint.