Category Archives: Recreations

Some people are easily amused.

Philosophers make quick keyboardists

Posted on by

[17 December 2009]

A mnemonic for ACL2 induction

Lately I’ve been spending time working through a lot of exercises in ACL2. As a way of helping the user internalize the requirements for successful induction, several exercises ask for an explicit reformulation of a problem in terms of the ACL2 induction principle.

Don’t worry: I don’t want to try to explain the ACL2 induction principle here. It suffices for present purposes to observe that a fully explicit application of the ACL2 induction principle requires that you write down a number of things; you, dear reader, don’t need to understand what they are, only that they exist and need to be specified:

  • φ, the formula being proved
  • m, the measure to be used when computing the ‘size’ of a particular instance of the formula
  • qi (for 1 ≤ i ≤ k), the conditions which determine the different induction steps: one induction step for each qi
  • k, the number of induction steps (and thus of conditions)
  • σi,j (for 1 ≤ i ≤ k and 1 ≤ j ≤ hi), the substitutions applicable to condition qi; each condition qi may have up to hi hypotheses and corresponding substitutions
  • hi, number of induction hypotheses for each induction step qi
  • the measure conjectures for the case: (a) that the measure given always produces an ordinal value, and (b) that the measure decreases on each recursive call (i.e. in each induction hypothesis)

After a while, my evil twin Enrique got tired of watching me flip back and forth between the statement of the problem I was trying to solve and the page that showed all the things that needed to be written down; he said “Haven’t you memorized that list yet?” “No,” I said. “It’s not that simple a list, is it?”

“Sure it is,” he said. “Just use a mnemonic to remember it. The full list, with all subscripts, is

φ m, qi ≤ k, k, σi, j, hi, m c

“So just remember

Philosophers make quick keyboardists; strength in judgment helps improve mental capacity.

“Or if you can remember the subscripts by yourself, and just need (φ, m, q, σ):

Philosophy multiplies quizzical subtleties.

“Easy, see?”

Sometimes I think Enrique has too much time on his hands.

Metadata and search – a concrete example

Posted on by

[18 August 2009]

Here’s a concrete example of the difference between the metadata-aware search we would like to have, and the metadata-oblivious full-text search we mostly have today, encountered the other day at the Balisage 2009 conference in Montréal.

Try to find a video of the song “I don’t want to go to Toronto”, by a group called Radio Free Vestibule.

When I search video.google.com for “I don’t want to go to Toronto”, I get, in first place, a song called “I don’t want to go”, performed live in Toronto. When I put quotation marks around the title, it tells me nothing matches and shows me a video of Elvis Costello singing “I don’t want to go to Chelsea”.

It’s always good to have concrete examples, and I always like real ones better than made-up examples. (Real examples do often have a disconcerting habit of bringing in one complication after another and involving more than one problem, which is why good ones are so hard to find. But I don’t see many extraneous complications in this one.)

Mainframe terminal rooms and the oral tradition

Posted on by

[7 July 2009]

A number of XML experts I know use Emacs for editing XML, employing either James Clark’s nxml mode or Lennart Staflin’s psgml mode. But few people who don’t already know Emacs are eager to learn it.

My evil twin Enrique suggested a reason: “In the old days,” (he means thirty years ago, when he first learned to use computers), “using a computer mostly meant using a mainframe. Which meant, on most university campuses, using a public terminal room. Which meant there were usually other people around who might be able to help figure out how to make the editor do something. Emacs was able to spread widely in that culture because the written documentation was not the only available source of information. (Did Emacs even have written documentation in those days?) Emacs, and a lot of other tools, were propagated by oral tradition.

“Nowadays, however, the oral traditions of the public terminal room are mostly dead. What the user cannot figure out how to use from the user interface and (perhaps) a glance at the documentation, might as well not be in the program. Fewer and fewer users will trouble to learn Emacs.

“I predict that when the people who first learned computing in a mainframe terminal room are dead, Emacs will be effectively dead, too. Its natural method of propagation is by looking over someone’s shoulder at what they are doing and asking ‘How did you do that?’ That doesn’t happen when computing almost always happens in private places.

“R.I.P., Emacs,” he intoned mournfully. “And probably TeX and LaTeX, too.”

“Well, hang on,” I said. “Neither Emacs nor TeX is dead yet.”

“Maybe not, but it’s only a matter of time. They’ll end up in the Retro-Computing Museum.” I could have sworn I saw a tear in his eye.

“But, you know, it’s only a matter of time for all of us. And besides, you’re wrong in at least some ways. I did indeed spend the first few years of my computing life haunting university terminal rooms. I got a lot of help from other people, and I passed it on. But I didn’t use TeX or Emacs until years later. The oral traditions of the terminal room, if they ever actually existed, had nothing to do with it. Both Emacs and TeX are perfectly capable of acquiring new users without oral transmission.”

He looked up. “You mean, there’s hope yet?”

“There’s always hope. But no, I’m still not going to help you debug that self-modifying 360 Assembler program you brought over. I’ve got work to do.”

For collectors of headline ambiguities …

Posted on by

[22 April 2009; unintended injection of draft notes for other postings removed 18 November 2017]

Linguists (and others) like to collect cases in which the compressed, telegraphic style of newspaper headlines lead to unexpected syntactic ambiguities.

The Albuquerque Journal and the Santa Fe New Mexican both carried stories yesterday about the results of a new University of New Mexico study on the incidence of spinal injuries in the U.S.

I showed them to Enrique, who glanced at the headline in the Journal:

Paralysis More Widespread Than Thought

and asked “When did the Albuquerque Journal start covering W3C and ISO Working Groups?”

Enrique and the printer

Posted on by

[18 February 2009]

Enrique isn’t speaking to me just now.

He phoned this morning, fuming. “I installed some new OS update the other day, and now my printer won’t print.” “I’m sorry to hear that,” I said. I was, too: when Enrique’s printer doesn’t work, he always wants to use mine. “Did you try to fix the problem?” “Well, I went to the Web and found some advice to try deleting the printer and re-adding it. So I deleted it. And now the [expletive deleted] machine can’t see the printer at all!” “Ouch,” I said, wondering whether the toner we have on hand would get us through the week, if Enrique descended on us with hundreds of pages to print. “So I ran Software Update again, and it took forty-five minutes to download yet another security update for the OS. And it still couldn’t find the printer. So then I went to the Apple site and downloaded the packet of HP printer drivers … and it’s still not finding the driver.“

“Is the USB cable seated securely?” “What kind of amateur do you take me for? Of course. I checked, it’s secure both at the machine end and at the printer end.“

“Did you unplug and replug the power cord, too?”

There was a brief pause, before the call was cut off. Like I say, he’s not talking to me today. I’ll try to use the quiet time to get some other work done.