bollu

Lambda calculus talks about computable functions, where the types of the inputs are typically something discrete, like `Bool` or `Nat`. Here, the domain is the real numbers.

please send me an email <siddu.druid@gmail.com>. I'm a PhD student at cambridge, and might be able to put you in touch with folks who have positions to hire you as an RA if your research profile fits. even if there isn't an immediate fit, I'm happy to scout around and see if anything pops up. Best, Sid

how does one get to conversational level in a week? I would love to know!currently anki-flashcarding my way through italian...

Having similar reasoning, I would up writing a tiny-optimizing-compiler tutorial that only explains how to write a middle and back end of a compiler: https://github.com/bollu/tiny-optimising-compiler

That's really neat, I hadn't seen the black hole argument before, that's really cute

yes, Lean is executable, and the proof of natural numbers runs with arbitrary width integers. they're stored as tagged pointers, with upto 63bit numbers being normal numbers, and larger numbers become GMP encoded.

How does one formally define a spinor? I've seen the definition of a spinor field as "things that transform like a spinor", and a spinor as a "representation of the spin group" (which representation), but I would like to know a canonical mathsy definition of what the heck a "spinor" is! May I please have one? :)

How'd you recommend I learnt to paint? I've not really done much painting in my life at all, and I'd love a breakdown.

I'm curious, which solver did you work on? And yeah, I've been working on formally verifying bitblasting in Lean (https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%...), and it's genius --- the algorithms, the reductions, the heuristics, it's all so deep.

Can you elaborate on the batching part for me? I don’t see it

what definition of "fair" was reached upon?

Nice! As someone who understands very little CSS, could you explain why this works?

I've written about [this explanation of tensors](https://pixel-druid.com/articles/tensor-is-a-thing-that-tran...) before, and it seems worthwhile to write it down again:

There are two ways of using linear maps in the context of physics. One is as a thing that acts on the space . The other is a thing that acts on the coordinates . So when we talk about transformations in tensor analysis, we're talking about coordinate transformatios , not space transformations . Suppose I implement a double ended queue using two pointers:

``` struct Queue {int memory, start, end; } void queue_init(int size) { memory = malloc(sizeof(int) size); start = end = memory + (size - 1) / 2; } void queue_push_start(int x) { start = x; start--; } void queue_push_end(int x) { end++; end = x; } int queue_head() { return start; } int queue_tail() { return end; } void queue_deque_head() { start++; } void queue_deque_tail() { tail--; } ```

See that the state of the queue is technically three numbers, { memory, start, end } (Pointers are just numbers after all). But this is coordinate dependent , as start and end are relative to the location of memory. Now suppose I have a procedure to reallocate the queue size:

``` void queue_realloc(Queue q, int new_size) { int start_offset = q->memory - q->start; int end_offset = q->memory - q->end; int oldmem = q->memory; q->memory = realloc(q->memory, new_size); memcpy(q->memory, oldmem + q->start, sizeof(int) * (end_offset - start_offset); q->start = q->memory + start_offset; q->end = q->memory - end_offset; }

```

Notice that when I do this, the values of start and end can be completely different! However, see that the length of the queue, given by (end - start) is invariant : It hasn't changed!

---

In the exact same way, a "tensor" is a collection of numbers that describes something physical with respect to a particular coordinate system (the pointers start and end with respect to the memory coordinate system). "tensor calculus" is a bunch of rules that tell you how the numbers change when one changes coordinate systems (ie, how the pointers start and end change when the pointer memory changes). Some quantities that are computed from tensors are "physical", like the length of the queue, as they are invariant under transformations. Tensor calculus gives a principled way to make sure that the final answers we calculate are "invariant" / "physical" / "real". The actual locations of start and end don't matter, as (end - start) will always be the length of the list!

---

Physicists (and people who write memory allocators) need such elaborate tracking, to keep track of what is "real" and what is "coordinate dependent", since a lot of physics involves crazy coordinate systems , and having ways to know what things are real and what are artefacts of one's coordinate system is invaluable. For a real example, consider the case of singularities of the Schwarzschild solution to GR, where we initially thought there were two singularities, but it later turned out there was only one "real" singularity, and the other singularity was due to a poor choice of coordinate system:

Although there was general consensus that the singularity at r = 0 was a 'genuine' physical singularity, the nature of the singularity at r = rs remained unclear. In 1921 Paul Painlevé and in 1922 Allvar Gullstrand independently produced a metric, a spherically symmetric solution of Einstein's equations, which we now know is coordinate transformation of the Schwarzschild metric, Gullstrand–Painlevé coordinates, in which there was no singularity at r = rs. They, however, did not recognize that their solutions were just coordinate transform

I am curious why you feel that way.

Does the temperature actually change discontinuously in a physical system from -infty to +infty, or is it a theoretical artifact that does not show up experimentally?

I have a very well documented implementation of rete, that also produces nice looking SVGs of the state of the rete algorithm here: https://github.com/bollu/rete

It's a really interesting algorithm, and allows one to get O(1) incremental pattern matching (ie, when one adds a pattern, one is told of a matching pattern in O(1) time) at the cost of O(npattern * nitems) memory usage. I was trying to use it in the context of pattern matching within a compiler, but I never went anywhere since I had COVID, then a PhD to get to :)

Neat! do you have a resource that explains this perspective further?

Yes, lilypond generates SVG that rescales smoothly

You're right on one count: no library implements forward mode. Hence, you're correct that no autodiff library (including pytorch) implement autodiff this way.

However, *you're wrong* that forward mode cannot be written in terms of dual numbers. The point is that the addition and multiplication operation for dual numbers correspond exactly to rules of the derivative of addition and the derivative of the product.

You are very wrong.

Many of the key results of theoretical CS is to prove impossibility. There is no code to be written when you show that something is not possible.

- Halting problem: impossibility of TM to determine if other TMs halt. - crypto: impossibility for a Turing machine to break a cryposystem in polytime - sorting lower bounds: impossibility to sort objects given only a less_than operator on them in time less than O(n log n)

and so on. There is no code to be written for these, because they are mathematical theorems.

computer science is about computers as much as astronomy is about telescopes ~Dikjstra.

Could you link to your code? I am interested in the API design of meshing a layout system with immediate mode GUIs

How do you define the curvature for a cone when it has a singularity at the apex? From the definion that I know (angle defect), the tip of the cone will have curvature

Surely you’re joking. Polya pioneered so much combinatorics I don’t even know where to begin. Heck, a lot of counting problems reduces to polya’s enumeration theorem. The page of “references” to stuff named after him should be a clue to you.

I am super confused. Why can't I take this purely classical circuit and run it on a classical computer? Somewhere, there should be some blowup into exponential time?

I do not believe this. What will one do about intermetidate computations which can have complex coefficients? In general, you'd need some way to change the gates/ unitary matrices themselves to be purely real. So you'd need to find an isomorpism from U(n) into a subgroup of SO(poly(n)) for this claim to work. Why does such an isomorphism exist?

Could you provide a link to some more reading about this? i do not know what a wada property is, nor why it is topological

Got any chewey bread recipes?

What's the RPN based calculator you use on your terminal? I'd love to learn!

What is an anaphoric function and why would I want it?

What is an anaphoric function / macro? I've seen this term floating around and I don't know what it means!