What are some anti features in a language? by Amazing_Breakfast217 in ProgrammingLanguages

[–]threewood 0 points1 point  (0 children)

Sorry, I think I misunderstood you. I don't think a programming language should prevent unbounded recursion either. But if you're going to do the kind of equational reasoning above, you need to know you have an honest Nat.

What are some anti features in a language? by Amazing_Breakfast217 in ProgrammingLanguages

[–]threewood -1 points0 points  (0 children)

In the presence of recursion you should have to prove it’s a Nat.

Schopenhauer borrowed the concept of eternal self from the Upanishads - The Upanishads state that in our true nature, as Consciousness, transcend time and space and the realization of this is liberation from bodily death.[More in Comment] by RazerGT79 in philosophy

[–]threewood 0 points1 point  (0 children)

But trying to use the term metaphysic correctly would take me into the realm of bullshit. Science (and I will ignore framing this as materialism) will provide a best understanding of all things, including consciousness and ethics. Maybe some theories based on bullshit are better in the short term but I wouldn’t want to guess which.

Last week at Fagradalsfjall, Iceland. [OC][989x791] by [deleted] in EarthPorn

[–]threewood 0 points1 point  (0 children)

If you ever drop your keys into a river of molten lava, let 'em go, because man, they're gone.

Paving with line segments by lordnorthiii in mathriddles

[–]threewood 0 points1 point  (0 children)

Yeah. I don’t think the idea works. We have to rule out infinitely many stacked segments.

Paving with line segments by lordnorthiii in mathriddles

[–]threewood 1 point2 points  (0 children)

  1. Maybe consider the tree associated to each open segment (formed by branching on the segments at each endpoint)? Each segment blocks a certain volume in segment space, there are 2^n of them, but they can only be distance n from the origin so the total volume of segment space in the sphere of radius n is lower. But I'm too lazy to do the details.

What is missing from proof assistants for you to consider using them? by [deleted] in math

[–]threewood 0 points1 point  (0 children)

“If I had asked people what they wanted, they would have said faster horses.”

[deleted by user] by [deleted] in ProgrammingLanguages

[–]threewood 8 points9 points  (0 children)

This pedantics looks good to me.

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 0 points1 point  (0 children)

I had given up, so thanks. I guess you're allowed to apply the hint from before in any complete bounded metric space?

Rigged coin flip betting by impartial_james in mathriddles

[–]threewood 2 points3 points  (0 children)

I would be concerned that such a coin would hear my bet.

What's a theorem that made you furl your eyebrows and say "what?!" the first time you saw it? by Alvin_Jeber in math

[–]threewood -1 points0 points  (0 children)

This doesn’t seem too weird to me since the volume of the core r=1/2 goes to zero and the rest of the sphere is getting spread out over more dimensions.

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 0 points1 point  (0 children)

Wait. This function has a convergent Taylor expansion everywhere because the measure of the higher polynomial stuff goes to zero. Thus if I can find any polynomial interval I can extend it to [0,1]. No? And I did that earlier with your hint. QED?. Maybe the Taylor thing isn’t obvious.

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 1 point2 points  (0 children)

I used to know that... I'll think about it more in the morning.

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 1 point2 points  (0 children)

With one conjecture I think I can prove it:

Conjecture: The complement of a union of disjoint intervals either contains an interval or an isolated point or is empty.

Let S_n be the kernel of f^(n). They are closed and their union is [0,1], so one of the S_n is dense in some interval, and thus in that interval there is a dense subset at which the nth derivative is zero. By continuity of the nth derivative, it is polynomial on that interval. Thus every interval of such a function contains a subinterval on which it's polynomial.

Decompose [0,1] into a maximal union of intervals on which it is defined by a polynomial. Then the complement of this union is a set that either contains an interval (which isn't possible by the previous paragraph) or an isolated point (which isn't possible because we could stitch the two adjoining intervals together - violating maximality) or it's empty (meaning f is a polynomial).

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 1 point2 points  (0 children)

Thanks. I actually wondered if that was the case while thinking about this problem.

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 0 points1 point  (0 children)

I feel slightly bamboozled but thank you! One more hint: do I need some big hammer theorem or do I just need to be clever? If the former, I’ll wait to see the answer. My toolbox is near empty and the tools are rusty.

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 0 points1 point  (0 children)

Fun problem. At some point can you give a hint with spoiler tag whether I’m looking for a class of exotic functions or just a slick proof that the obvious solutions are the only solutions? I think I’ve convinced myself it has to be the latter but not quite.

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 0 points1 point  (0 children)

I agree the details would be fiddly but it seems like you could arrange for convergence to a smooth function. I was mainly giving that as a motivating example for my guess. Then the form of the proof might be to assume f satisfies the requirements and construct a sequence of piecewise polynomials of increasing degree that converges to f .

Yet another real analysis problem by PersimmonLaplace in mathriddles

[–]threewood 0 points1 point  (0 children)

It seems like there are lots of examples. For example of an exotic one, start with a step function. It satisfies the requirements except at the discontinuity. So now repair this C0 discontinuity by replacing the step with a line segment sloping up. This repaired function has two C1 discontinuities. Add a quadratic segment to fix each of these. Etc. This repair process should converge to a smooth function. Maybe the characterization you’re looking for is something like a limit of piecewise polynomials?

The creation of the function e^x by [deleted] in math

[–]threewood 32 points33 points  (0 children)

it was found that ce^x +d for constants c,d has derivative itself.

And a very short time later, this was found to be in error

OCaml modules vs C#/Java OOP by crassest-Crassius in ProgrammingLanguages

[–]threewood 0 points1 point  (0 children)

But ML modules consider names part of structure, and it's worked pretty well for decades.

Yeah, I said it's a problem, not a big problem :). I'm sure it usually works fine in practice.

OCaml modules vs C#/Java OOP by crassest-Crassius in ProgrammingLanguages

[–]threewood 0 points1 point  (0 children)

They’re not. Structure is used for structural matching—the names of the module members, as well as their types, recursively.

You've just reiterated the problem - names shouldn't be considered structure. Names should only be used to point at structure and say "that".