agalunar

X-rays! not gamma rays.

Perhaps worth noting that the number of lines in a cache is often different than the number of rows, which can be relevant for some workloads.

The size of an ordinary cache is rows × ways × size(line), where rows = 2 ↑ num-idx-bits. For example, most Intel 64 and AMD 64 processors use log₂(size(page)) − log₂(size(line)) = 12 − 6 = 6 index bits for the L1 cache*, so an L1 cache with 8-way associativity is 64 sets × 8 lines/set × 64 bytes/line = 32 KB large, and an L1 cache with 12-way associativity is 64 × 12 × 64 = 48 KB large. I remember being surprised to learn that most processors have only 64 rows in the L1 cache!

*So that virtual indexes and physical indexes are identical (so that retrieval of the row can happen in parallel with TLB lookup).

There’s an analysis of the Schraudolph approximation of the exponential function (along with an improvement upon it) that someone might find interesting at https://typ.dev/attention#affine-cast

SPRT is used religiously in engine development today. There is enormous incentive to test efficiently.

https://github.com/official-stockfish/fishtest/wiki/Fishtest...

You may want to ask in the Stockfish discord: https://discord.com/invite/GWDRS3kU6R

I believe Peano dot notation works the other way ’round;

  A . B : C :. D

would be, as I understand it, equivalent to:

  ((A B) C) D

The “general principle” is that a larger number of dots indicates a larger subformula.¹

What if you need to nest parentheses? Then you use more dots. A double dot (:) is like a single dot, but stronger. For example, we write ((1 + 2) × 3) + 4 as 1 + 2 . × 3 : + 4, and the double dot isolates the entire 1 + 2 . × 3 expression into a single sub-formula to which the + 4 applies.²

A dot can be thought of as a pair of parentheses, “) (”, with implicit parentheses at the beginning and end as needed.

In general the “direction” rule for interpreting a formula ‘A.B’ will be to first indicate that the center dot “works both backwards and forwards” to give first ‘A).(B’, and then the opening and closing parentheses are added to yield ‘(A).(B)’. The extra set of pairs of parentheses is then reduced to the formula (A.B).³

So perhaps one way of thinking about it is that more dots indicates more separation.

¹ https://plato.stanford.edu/entries/pm-notation/dots.html

² https://blog.plover.com/math/PM.html

³ https://plato.stanford.edu/entries/pm-notation/dots.html

See also https://plato.stanford.edu/entries/pm-notation/index.html and https://muse.jhu.edu/article/904086.

I may be wrong, but I believe the name of the type family is simply Times New; the name of the italic face would then be Times New Italic rather than the contradictory Times New Roman Italic. It’s strange that the name of the roman face specifically is always used; I’d suppose it’s merely because that’s how the digital fonts were inadvertently named? Times New Roman has been the name in dropdown menus, and most laypeople are unfamiliar with roman as a term of art, so there’s no reason people wouldn’t use that name. But I wonder how the digital fonts came to be named Times New Roman rather than Times New.

> A data race occurs any time two threads access the same memory location concurrently and non-deterministically when at least one of the accesses is a write.

From what I understand of the C++ memory model (shared by C and Rust), this is not the definition of data race – a data race occurs when two or more threads access memory concurrently where at least one access is a write and the accesses are unsynchronized. However, synchronized accesses may not have a deterministic ordering, in which case a race condition occurs.

(Confusing as it may be, I believe this is standard terminology.)

I’d argue there’s a very big difference between “x: y” and “x : y”. I can only see the former as assignment and the latter as the has-type relation.

(I find it baffling in the extreme that in many mainstream languages the convention is to write type annotations as “x: T”, both prima facie and because in those languages the notation then collides with field assignment!)

A small nit: the development of Unix began on the PDP-7 in assembly, not the PDP-11.

(The B language was implemented for the PDP-7 before the PDP-11, which are rather different machines. It’s sometimes suggested that the increment and decrement operators in C, which were inherited from B, are due to the instruction set architecture of the PDP-11, but this could not have been the case. Per Dennis Ritchie:¹

> Thompson went a step further by inventing the ++ and -- operators, which increment or decrement; their prefix or postfix position determines whether the alteration occurs before or after noting the value of the operand. They were not in the earliest versions of B, but appeared along the way. People often guess that they were created to use the auto-increment and auto-decrement address modes provided by the DEC PDP-11 on which C and Unix first became popular. This is historically impossible, since there was no PDP-11 when B was developed. The PDP-7, however, did have a few “auto-increment” memory cells, with the property that an indirect memory reference through them incremented the cell. This feature probably suggested such operators to Thompson; the generalization to make them both prefix and postfix was his own.

Another person puts it this way:²

> It's a myth to suggest C’s design is based on the PDP-11. People often quote, for example, the increment and decrement operators because they have an analogue in the PDP-11 instruction set. This is, however, a coincidence. Those operators were invented before the language [i.e. B] was ported to the PDP-11.

In any case, the PDP-11 usually gets all the love, but I want to make sure the other PDPs get some too!)

[1] https://www.bell-labs.com/usr/dmr/www/chist.html

[2] https://retrocomputing.stackexchange.com/questions/8869

I’ve noticed that, besides the magnetism and drive for sex (which would be sufficient for a species to propagate), many people also experience the biological imperative (wanting their genes replicated) as its own separate feeling.

This makes no sense to me – it’s not a feeling I can personally relate to. I’d like to raise kids because I’d enjoy getting to teach them and share things with them, but I don’t care whether they are my biological children or not.

So it’s something I’ve wondered about. The likely why makes sense, but I don’t really get the what.

At some point in my life I unconsciously decided that charisma (in this sense) was something I did not want to exercise, and was perhaps even wrong to exercise.

In so many facets of our lives already, our wants are being manipulated for the benefit of others. And who am I to decide what is important? For things that involve other people, I’d rather make that decision collectively. I want the thoughts, opinions, and feelings of people who don’t possess or exercise charisma to have space and weight.

People may also be interested in the Tako shell, which is a fork of Xonsh that “sacrifice[s] some of the ‘fancy stuff’ so that basic shell operations work as expected, the codebase is small, and things are as performant as can be expected from a shell written in Python.”

(Homepage) https://takoshell.org/index.html

(Differences from Xonsh) https://takoshell.org/xonsh.html

You’d perhaps be better off using U+2002 EN SPACE (or the canonically equivalent U+2000 EN QUAD).

From what I recall, the size of a typical interword space is ⅓ of an em, and traditionally a bit more than this is inserted between sentences (but less than ⅔ of an em). The period itself introduces a fair amount of negative space, and only a skosh more is needed if any.

Belying the name somewhat, I believe U+3000 is specifically meant for use with Sinoform logographs, having the size of a (fullwidth character) cell, and so it makes little sense in other contexts.

“Imitation without understanding”, “imitating but misconstruing”, “mindless imitation”, “superficial emulation”, &c.

I think “cargo culting” in the popular sense means little more than that (whereas actual cargo culting is much more complex, as the featured article describes).

I've always been mystified by that expansion. "The featured article" seems to me to make much more sense.

Perhaps “The Typefaces of Wall·E”, plural?

To save someone the lookup, this is:

    U+00B7 MIDDLE DOT = midpoint (in typography); Georgian comma; Greek middle dot (ano teleia) • also used as a raised decimal point or to denote multiplication; for multiplication 22C5 is preferred

But note there is a separate Unicode scalar value for the dot operator:

    U+22C5 DOT OPERATOR • preferred to 00B7 for denotation of multiplication

Those aren’t syllable divisions, they’re hyphenation points!

From the footnote on page 219 of Word by Word by Kory Stamper (formerly a lexicographer at Merriam-Webster):

> Here is the one thing that our pronunciation editor wishes everyone knew: those dots in the headwords, like at “co·per·nic·i·um,” are not marking syllable breaks, as is evident by comparing the placement of the dots with the placement of the hyphens in the pronunciation. Those dots are called “end-of-line division dots,” and they exist solely to tell beleaguered proof-readers where, if they have to split a word between lines, they can drop a hyphen.

The title of the submission should be changed to “Type in Wall·E”, “Typesetting in Wall·E”, or “Typography in Wall·E”; the word “typeset” is a verb or past participle, not a noun.

My line of thinking roughly was, "each type system corresponds to a particular logic system and vice versa; in a proof by induction, the different cases correspond to the type constructors, but what does the necessary axiom schema or second-order axiom of induction correspond to? (in order to avoid the problem of nonstandard elements). And proof by infinite descent seems to require something other than induction, so where does well-foundedness come from?"

I realize these questions may not even be posed sensibly; maybe the answer is as simple as, "the naturals are defined constructively here; of course they are the naturals and therefore are well-founded". As I said, it's been a while, so things are hazy in my mind.

How does infinite descent work using a proof assistant? It's been quite a while, so I may be remembering incorrectly, but this is my understanding:

Coq uses an inductive type like "N = 0 : N | S : N → N", and a first-order theory with integers axiomatized this way admits nonstandard models (whose prefixes are isomorphic to the naturals but have elements not reachable by repeated application of S, defeating infinite descent). But universal quantification in system F (inherited by the calculus of inductive constructions) corresponds to a fragment of second-order logic, where there is only one model (– the theory is categorical).

Is that right?

> Research has generally linked economic inequality to political and social instability, including revolution, democratic breakdown and civil conflict.

https://en.m.wikipedia.org/wiki/Economic_inequality

It's a familiar concept to most people, though: most people understand that people have parents, grandparents, greatgrandparents, and so on.

(Maybe a bad example; I feel like it shows that people are familiar with coinduction.)

For the curious: I assume the parent is referring to Pasch's axiom.

https://math.stackexchange.com/questions/1901133/euclids-ele...

Using indices is a (slight) improvement over pointers, since in Rust you will benefit from bounds checking (restricting you to the memory allocated for that tree).

(If you use u32 for the indices, you also save some space.)

This is beside the point, but the only way an engine can possibly search to depth 20 is by being extremely selective, using heuristics to guess move quality (such as static exchange analysis, the killer move heuristic, history tables, countermove tables, follow-up tables, late move reductions, &c). The discovery was that it's often better to guess move quality dynamically, based on the observed utility of similar moves in similar contexts, rather than statically. But this is not especially "simple", and it still (necessarily!) involves judging up front a few moves as likely-good and the vast majority of moves as unworthy of further examination.

Both type A engines (to use Shannon's terminology) and type B engines are relatively weak. The strong engines are all hybrids.

Or https://looo.lol/?x=1, https://looo.lol/?x=2, or https://looo.lol/?x=-1 (good luck!), or https://looo.lol/?x=10...0 ("Infinity", if you replace the ellipsis with 306 zeroes or so).

That's what I figured! but thought the derivation would be fun to share with people reading the comments.