Hacker News Reader

Comment by pron | Hacker News Reader

> 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.

View on HN

I'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*.

An 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

The 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.

In 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.

> 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.

First, while you can express those statements in programming languages, they will either be expressed differently in order to have the same meaning or, if expressed in a similar way, have a different meaning (even ignoring that many such statements are not computable at all). This merely shows that math is not an FP language.

Second, you can prove those equivalences in any language that allows you to directly express relations, be it the type-level language of Agda, Coq or F*, or the contract language of an imperative language -- this is nothing to do with FP, but with a language that can express relations.

Yes, 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.

Can you provide an example of mutability in, say, high school or undergraduate math?

any sum with an index of summation requires mutability

"requires" is a strong word. the only explicit definition ive seen given for n-ary summations and products products was recursive.

I 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.

We'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.

I 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.

That is not what the Curry-Howard Isomorphism -- AKA propositions-as-types -- says. Propositions-as-types is the observation that the typing rules of certain type systems follow the inference rules of certain logics (largely because they were designed this way), and that in general typing rules and inference rules can be made to mimic one another, so that a type system can represent propositions in some logic, and type checking represent proof-checking.

That arbitrary mathematical proofs can be equivalently made by Turing machines (and conversely, that predicate calculus is Turing complete) is a lemma by Turing, published in the same 1936 paper in which he introduced the notion of computation, Turing machines and proved what today is known as the halting problem.

I 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?

Just 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]

The 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.

I 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.

Not to mention that whole fields of mathematics deal with numerical algorithms: Computational algebraic geometry, number theory, numerical mathematics etc.

Reply on news.ycombinator.com