emih

no profile record

投稿

A case against currying

118 ポイント投稿者 emih4 か月前130 コメント

Wordle as a Two-Player Game

3 ポイント投稿者 emih4 か月前0 コメント

Biconnected components

53 ポイント投稿者 emih10 か月前20 コメント

コメント

3 か月前議論

I like the story in the article, but I think it tries to create some drama where there isn't any.

I think it's great that a lot of work is done using proof assistants, because clearly it's working out for researchers; diversity of research and of methods is a great strength of science. I really can't see how you can "push it too far", pen-and-paper proofs are not going anywhere. And as more researchers write machine-checked proofs, new techniques for automating these proofs are invented (which is what my research is about hehe) which will only make it easier for more researchers to join in.

> Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean.

_Some_ mathematicians are trying to formalize _some_ of mathematics using a proof assistant called Lean. It's not a new development, proof assistants have been used for decades. Lean 4 has definitely been gaining popularity recently compared to others, but other proof assistants are still very popular.

> a dedicated group of Lean users is responsible for determining which definitions should go into Lean’s library

The article makes it sound like there is a single, universal "The Lean Library" that everyone is restricted to. I assume it refers to mathlib? But at the end of the day it's just code and everyone is writing their own libraries, and they can make their own decisions.

4 か月前議論

Mathematically it's quite pretty, and it gives you elegant partial application for free (at least if you want to partially apply the first N arguments).

4 か月前議論

I didn't know Standard ML, that's interesting.

And yeah I think this is the way to go. For higher-order functions like map it feels too elegant not to write it in a curried style.

4 か月前議論

Those are nice examples, thanks.

I was imagining you might achieve this optimization by inlining the function. So if you have

  getClosest(points, p) = findInTree(buildTree(points), p)

And call it like

  myPoints = [...]
  map (getClosest(myPoints, $)) myPoints

Then the compiler might unfold the definition of getClosest and give you

  map (\p -> findInTree(buildTree(myPoints), p)) myPoints

Where it then notices the first part does not depend on p, and rewrite this to

  let tree = buildTree(myPoints) in map (\p -> findInTree(tree, p)) myPoints

Again, pretty contrived example. But maybe it could work.

4 か月前議論

That's a very good point, I never thought really about how this relates to the execution model & graph reduction and such. Do you have an example of a function where this can make a difference? I might add something to the article about it.

It's also a question of whether this is exclusive to a curried definition or if such an optimization may also apply to partial application with a special operator like in the article. I think it could, but the compiler might need to do some extra work?

4 か月前議論

Glad to hear the article did what I meant for it to do :)

And yes, another comment mentioned that Scala supports this syntax!

4 か月前議論

It's not that serious :)

4 か月前議論

You can still do this though:

  let result = (barbalyze(c, d, $) . foobinade(a, b, $)) input

Or if you prefer left-to-right:

  let result = input
    |> foobinade(a, b, $)
    |> barbalyze(c, d, $)

Maybe what isn't clear is that this hole operator would bind to the innermost function call, not the whole statement.

4 か月前議論

Thanks for sharing, interesting to see that people writing functional languages also experience the same issues in practice. And they give some reasons I didn't think about.

4 か月前議論

That's a fair point, they are all isomorphic.

The distinction is mostly semantic so you could say they are the same. But I thought it makes sense to emphasize that the former is a feature of function types, and the latter is still technically single-parameter.

I suppose one real difference is that you cannot feed a tuple into a parameter list function. Like:

fn do_something(name: &str, age: u32) { ... }

let person = ("Alice", 40);

do_something(person); // doesn't compile

5 か月前議論

Machine learning is definitely enabling writing _proofs_ within a proof assistant, and I'm sure it will help to make formal verification more viable in the future.

Where it cannot (fully) replace humans, is writing the _theorems_ themselves. A human has to check that the theorem being proven is actually what you were trying to prove, and this is not safe from LLM hallucinations. If you ask an LLM, is this bridge safe, and it writes `Theorem bridge_is_safe : 1 + 1 = 2.` and proves this theorem, that does _not_ mean the bridge is safe...

The article then also makes some wild extrapolations:

> We could imagine an LLM assistant for finance that provides an answer only if it can generate a formal proof that it adheres to accounting rules or legal constraints.

I guess it's true because you could imagine this, hypothetically. But it's not going to happen, because you cannot formalize a financial or legal statement in a proof assistant. It's a fundamentally informal, real-world thing, and proof assistants are fundamentally for proving formal, abstract things.

7 か月前議論

Graph coloring is NP-hard so it would be very difficult to replace it with an O(1) algorithm.

If you mean graph coloring restricted to planar graphs, yes it can always be done with at most 4 colors. But it could still be less, so the answer is not always the same.

(I know it was probably not a very serious comment but I just wanted to infodump about graph theory.)

7 か月前議論

You can't just put words in the author's mouth.

It's also not true at all. For instance, teaching in primary school is a field that is dominated by women where I live, and I (and I agree with the points described in the article) think it would be great to have more male teachers, so that girls and boys can both have rolemodels when growing up. This would also actually help to solve one of the problems that is described in the article, that boys feel unmotivated in school and fall behind.

10 か月前議論

The Boost algorithm computes the vertex-biconnected components rather than the edge-biconnected components, which are two different but related concepts. Articulation points are also more related to vertex-biconnectedness than to edge-biconnectedness (articulation points are vertices that lie in multiple vertex-biconnected components, i.e., if you remove one you split up the graph into more components). From what I can see in the Boost docs, it doesn't have an implementation of edge-biconnected components.

You can write an algorithm to compute all of the articulation points & bridges & edge-biconnected components & vertex-biconnected components in a single DFS. Because of this you refer to all of them as just "Tarjan's algorithm" even if you just compute one of them (he is kind of the Euler of graph algorithms in that like half of graph algorithms is named after him). So, on a technical level, I guess my implementation is similar to the algorithm in Boost because they both use DFS and this `low` map, but they compute different things.

Finding the vertex-biconnected components next to the articulation points involves more work though (the implementation I used to have manages to also do it in the same pass but also maintains a stack of edges).

10 か月前議論

That one is intentional. Note: a tree edge (u, v) is a bridge if and only if low[v] is strictly greater than the entry time of u.

Here 4 is the entry time of that node. (For convenience I made sure that the node labels are just the DFS entry times.)

Though maybe comparing both low values might also work, I'd have to think about that...

10 か月前議論

Whoops, you got me. Fixed!

At some point I relabeled the vertices to match the DFS order, but I must have forgotten to update this example.

10 か月前議論

I used to get annoyed by these kinds of questions, but honestly I love talking about things I'm passionate about anyway and I want to get more people interested in the subject. So, I'm happy to answer questions like this and simultaneously sneak in some of my own personal experiences.

10 か月前議論

Basically you get a bunch of problems (ranging from "check if a number is prime" to complicated graph theoretical problems) and some time to figure them out and code a correct & efficient solution. Often there are computer science concepts and reasoning techniques you need to know about (like biconnected components) to figure out how to make an efficient enough implementation.

The contests I used to go to, you got 11-13 problems and 5 hours to solve them with a team of 3. However, you only have one PC to share, so a lot of the time you are discussing, drawing stuff on paper and figuring out the solution in your head. There is also a printing service during the contest where you can literally get a paper version of your code :) so somebody else can code while you debug on paper.

See for instance https://www.acmicpc.net/category/detail/4319 for the kinds of problems they give (Korean website unfortunately but the problems are in English).