4 ms·
> Mathematics is a purely functional language. It is not. E.g. x ∈ ℕ ∧ x > 2 ∧ x < 5 ∧ x % 2 = 0 implies x = 4. This is not something pure functional languages
by pron 7y ago
> Mathematics is a purely functional language.
It is not. E.g. x ∈ ℕ ∧ x > 2 ∧ x < 5 ∧ x % 2 = 0 implies x = 4. This is not something pure functional languages can express directly. In math we make common use of relations, of which functions are a special case, but not the common one and certainly not the only one. But even when we do work with functions, a functional PL does not suffice. E.g. writing f(t) = t + 1 ∧ x ∈ ℕ ∧ f(x) = 3 is equivalent to writing x = 2. Also, we commonly employ objects that are not computable.
This is just one of the many mathy myths that plague the FP community. Yes, there are some similarities between FP and mathematical notation, but FP and imperative are much closer to one another than either is to mathematics.
- orbifold 7y agoNot to mention that whole fields of mathematics deal with numerical algorithms: Computational algebraic geometry, number theory, numerical mathematics etc.
- j88439h84 7y agoI don't know much about this area. What about "x ∈ ℕ ∧ x > 2 ∧ x < 5 ∧ x % 2 = 0 implies x = 4." can't be expressed in common languages? Don't lots of solver systems have support for sets, and deriving facts from statements about them?
- Recursing 7y agoJust in case somebody might benefit from finding out how easy it is in python with z3 >>> from z3 import Int, solve >>> x = Int('x') >>> solve([x > 2, x < 5, x % 2 == 0]) [x = 4]
- taeric 7y agoThe argument here is that you used a program to solve an equation. You did not write your program in that way. Indeed, you are using operator overloading/fancy syntax to make this work. If anything, this seems to support the original claim.
- brianberns 7y agoI'm not sure what point you're trying to make. You can certainly express those statements in both FP and imperative languages, and you can prove the equivalences you mention in FP languages like Agda, Coq, and F*.
- cinnamonheart 7y agoAn example of > E.g. x ∈ ℕ ∧ x > 2 ∧ x < 5 ∧ x % 2 = 0 implies x = 4. in Agda would be this, I think: _ : ∀ { x : ℕ } → x > 2 → x < 5 → (x % 2) ≡ 0 → x ≡ 4
- pron 7y agoThe type level of dependently typed languages or other languages that allow directly expressing relations (including Java's JML) can do that. That's little to do with pure FP.
- cofunctor 7y agoIn some sense it does though. Type Theories (and their associated pure FP languages) often have the exact same algebraic structure as different classes of logic. To my understanding, JML uses Hoare Logic, which is a great tool for proving correctness of imperative languages, but is not quite as expressive. For example, Hoare Logic cant really deal with Higher-Order things. That's not to say Coq/Agda are perfect though. They do struggle with more "extensional" properties, such as function extensionality.
- pron 7y ago> but is not quite as expressive It's as expressive. > For example, Hoare Logic cant really deal with Higher-Order things. 1. It can. 2. It doesn't matter so much, as there are no higher order "things" but rather higher-order ways to describe things. For example, in mathematics higher-order systems can be described as either higher-order ODEs or equivalent first-order ODEs. In other words, "order" is a feature of the signifier, not the signified. For example, things that would be higher-order in Agda are first-order in TLA+ (and you don't need to go that far: formal set theories are usually first-order, yet you need higher-order typed logics to describe the same things). > They do struggle with more "extensional" properties, such as function extensionality. Well, that's because they're constructive. There are type-theory-based proof assistants that more easily support classical mathematics, like Lean.
- deleted 7y ago[deleted]
- hyperjeff 7y agoYes, well said. Math is not any form of programming, and programming is not math. Studying the relations between the two can be very helpful, and the difference itself is interesting. One may have specific reasons to us FP to cleanly decouple from certain kinds of side-effects, but there’s nothing un-mathy about mutability, and there are times when it’s a fine choice.
- brianberns 7y agoCan you provide an example of mutability in, say, high school or undergraduate math?
- mlevental 7y agoany sum with an index of summation requires mutability
- chobytes 7y ago"requires" is a strong word. the only explicit definition ive seen given for n-ary summations and products products was recursive.
- brianberns 7y agoI don't think so. For example, sum of first 5 integers: sum i = 1 to 5 of i -> 1 + 2 + 3 + 4 + 5 = 15 Nothing mutable there. In functional programming this is done with a `fold`, which doesn't use mutation.
- pron 7y agoWe're talking about notation. Anything could be described in any Turing complete language. It's uncommon to have something similar to mutation in ordinary mathematical notation, but summation is one example where it's used.
- mruts 7y agoI mean, that’s exactly what the Curry-Howard Isomorphism says: that math and programming are equivalent. Both can express and are equivalent to Turing machines.
- BlackFly 7y agoI also found this sidetrack to be a bit of a straw man. A large proportion of physics is devoted to dynamics: the study of change. There are mathematical descriptions for dynamics whereby a thing is updated x ↦ x + v * dt, v ↦ v + a * dt. You can think of a classical particle's position both as a thing that gets updated and as a function of time (time is definitely updating whether you like it and model it or not). Many numerical algorithms for differential equations update a field in place. Sometimes you need to be very careful in your description of how something gets updated in order to avoid data conflicts. If you define it as a function then you have a single option if you want to do this "in place": sparse matrix representation of the updated values and a write of the updated values into the memory. As an example, memory requirements for line relaxation in multigrid can be done as an O(1) operation instead of as the O(n^1/d) operation of a sparse copy. A mathematical function does not always return the same value. There are stochastic differential equations and random variables. For the sake of formality, they are frequently treated as discrete samples taken from a random distribution, but the naive approach of acting like the output of some function ε is random maps nicely into computers. If you are not "abusing notation" by using the functional notation, then the sample can be different every time you "take" it. Either way, you are not returning the same value each time. It is useful to be able to describe certain mathematical operations as updates instead of as pure functions. Mathematics certainly isn't incapable of doing this. There is a lot of value in functional descriptions as well. If you are a purist on either side, you are just ignoring valuable things for the sake of your ideal.