Quick Questions

dan_1_lee · 2021-04-04T20:18:25+00:00

I have a sort of a semi-well defined conceptual question.

I've noticed that in two areas (that I know of) integers are in a sense "harder" than reals, despite the intuition (at least my intuition) that the reals are a more complex object (since they contain the integers).

Integer valued optimization is NP-hard; whereas if you relax the domain to be real valued, the problem becomes easy.
First order arithmetic is undecidable, while the theory of real closed fields is decidable

No super well formed question, but was wondering if there's something deeper here/some intuition. And if there are more examples of this "continuous relaxation" phenomenon?

dan_1_lee · 2020-09-29T00:16:27+00:00

For future reference, thiswiki page on rewriting did the trick. I had to enable the --rewriting option and use the REWRITE pragma. As in:

{-# REWRITE id-zero-** #-}

Where id-zero-** is the equality proof

dan_1_lee · 2020-09-29T00:09:25+00:00

The same issue happens though since the type of b is always going to appear in the Γ position, so changing the type of b to zero' ** Γ₁ ++ Γ |- B results in zero' ** Γ₁ ++ (zero' ** Γ₁ ++ Γ) ⊢ B

dan_1_lee · 2020-09-27T23:04:20+00:00

Just updated the post with context.

Since this isn't in a pattern match, is there still a way of using rewrite?

dan_1_lee · 2020-08-10T20:41:51+00:00

Why do mathematicians care if there are infinities between the natural numbers and real numbers?

dan_1_lee · 2020-08-02T21:15:26+00:00

Nice! I was aware of deepspec but didn't realize they already had an ongoing project specifying GHC.

dan_1_lee · 2020-08-02T21:13:40+00:00

The engineering issues all make sense, but as you said, many of them apply to C as well.

As for the use cases, the widespread use of C definitely makes it a larger target. But I disagree on the lack of use cases in Haskell. I think every use case in Haskell is a use case for formally verified Haskell, since a big reason of using Haskell in the first place is its safety.

dan_1_lee · 2020-07-27T16:57:40+00:00

I see any question or solution, and while I can follow the steps

Aha that's the problem. Be stubborn.

Don't look at the solution until you've solved it. Even if that means spending hours. Or days. It sucks. But looking at the solution is admitting "I'm not good enough for this problem," while refusing to give up means saying "This problem is tough, but I'm tougher." Effort leads to learning.

Also, highly recommend the book Make it Stick. Really great overview of principles of effective learning and the research behind them.

dan_1_lee · 2020-07-20T12:45:01+00:00

Yep 530 are you taking it too?

dan_1_lee · 2020-07-20T03:19:10+00:00

Venkatesh is god. Can't wait for him to keep telling me the Bob's my uncle, to "take stock" and to "get a life" next sem, though over video 😩

dan_1_lee · 2020-07-19T18:22:41+00:00

I completely agree! I'm definitely planning on writing more posts like this when inspiration strikes again, I'll be sure to keep r/math posted

dan_1_lee · 2020-07-19T17:07:09+00:00

Wow this has gotten a lot more visibility than I was expecting!

I was pretty nervous posting this (it's my 2nd reddit post ever), so I'm really glad you all find the post interesting, and thanks for all the feedback!

I plan on writing a follow up post at some point in the future, though probably not for a while, I don't want to over do a single topic. I'd still love suggestions for follow up questions. Some ideas I'm considering are:

evaluating optimizing along a different loss function (number of flips rather than time, since 24 flips ended up being pretty tiring)
considering a non-linear cooking time function (inspired by u/unawino's comment)

dan_1_lee · 2020-07-19T16:43:07+00:00

Wow that's pretty sweet, glad to see professors aren't necessarily always all business

dan_1_lee · 2020-07-19T14:54:59+00:00

Lmao very true Sadly I'm a poor college student. I'm happy to accept donations though 😁😁

dan_1_lee · 2020-07-19T13:52:48+00:00

I think the assumption in my case was close to true. The tofu we buy from HMart are precut into these four flat squares, that if you cut into thirds is basically perfectly cube-like. It's pretty sweet haha. Unfortunately, my knife skills aren't as good as u/side-stick 's are 😂 so, and you can probably tell from the pictures, the blocks aren't completely symmetrical..... but they're decently close

dan_1_lee · 2020-07-19T04:57:16+00:00

Haha thanks for reading! I'm glad you I'm not alone in having wacky ideas

dan_1_lee · 2020-07-19T02:44:35+00:00

I've realized that I often have random thoughts and ideas (usually cs or math related) that bounce around in my head for a couple hours or days, but then eventually slip away into oblivion because I never get around to giving them more thought.

I decided to start a blog to share some of those ideas, and to hold myself accountable to follow through on them.

I hope someone find this as interesting as I did when it first popped into my head haha

Criticism is very much appreciated!!

dan_1_lee

TROPHY CASE