# Support some students!

I’ve been terrible about updating the blog lately. Personal life interferes sometimes, but I’m trying to build up a backlog of posts so that I can get the blog moving again without too much pressure.

In the meantime, I’ve got a request for you folks.

Through this blog, I met a really great SFF writer named Catherine Asaro. Catherine both writes, and also teaches math. She’s running a GoFundMe for her students, who participate in extracurricular math activities – clubs, classes and competitions.

They need money to cover travel expenses for going to math league competitions.

These kids are us: they’re the math geeks of the future. They need help from the math geeks of today. So go, give them a couple of bucks, help them out!

An extra little bit of incentive: the first five people who donate more than $25 can pick a topic, from either math or computer science, and I’ll write a blog post about it. Send me a copy of the thank-you letter you get from GoFundMe to show that you contributed, along with the topic you’d like me to write about. These thank-you posts for contributing will skip to the top of my priority queue, so you’ll see them soon! # Recipe: Za Jiang Mien, aka “Chinese Spaghetti” This is a traditional chinese dish. It’s affectionately known as chinese spaghetti. My wife has been telling me about it for years, and I’ve been trying to reproduce it for years. I’ve finally gotten it to the point where she’s happy with it. It’s a fun dish: it’s a make-your-own. You prepare the noodles and sauce and a bunch of toppings, and then each guest adds sauce and toppings to their own taste. I’ve seen a couple of variations on the set of toppings you can serve with it: cucumbers, carrots, raw onions, shredded ginger, sliced garlic, and bean sprouts all work. I’ve also seen one version that served it with black chinese vinegar, which was really strange. Ingredients • 4 chicken thighs, ground coarsely. • 2 tablespoons tobanjiang (chinese spicy bean sauce, available at asian groceries.) • 1/4 plus a couple of tablespoons cup soy sauce. • 1 cup chicken stock. • 1/2 cup sake or shaoshing wine. • 1 large onion, minced. • 2 cloves garlic, minced. • 1 large slice ginger, crushed and minced. • 1 cucumber • 1 carrot • 2 eggs • 2 scallions, green sliced, and whites finely minced. • 1 tablespoon sugar. • 1 tablespoon cornstarch mixed with some water. • 1/2 teaspoon sesame oil. 1. Prepare the toppings 1. Peel the cucumber, cut it in half, scrape out the seeds, and then cut it into thin sticks. Toss with salt, and set aside for 30 minutes, and then pour off the water that comes out. 2. Peel the cucumber, and cut into thin sticks. Toss it with salt, and set aside for 30 minutes. Pour off the water that comes out. 3. Finely slice the greens of the scallions, and set aside. 4. Beat the two eggs with a bit of soy sauce. Put some oil into a hot non-stick pan, and pour in the eggs. Spread then into a thin layer that covers the pan. Cook until it’s mostly solid, then flip it. When it’s all cooked, move it to a cutting board, and cut into thin ribbons. Set aside. 2. Make the sauce: 1. Mix the ground chicken thighs with a tablespoon of soy sauce. 2. Put 1 tablespoon of oil into a hot wok. Add the chicken, and stir fry until it starts to brown. Then remove it. 3. Put 1 tablespoon of oil into a hot wok. Add the garlic and ginger, and stir fry until fragrant. Then add the onions and scallion whites, and stir until they soften and just barely start to brown. 4. Scrape the onions to the sides of the pan, then add the tobanjiang to the oil that collects of the bottom of the pan. Stir it around for 30 seconds. 5. Add the chicken back in, and then add the sake. 6. When most of the sake has cooked off, add the chicken stock, soy sauce, sugar, and a cup of water. 7. Reduce the heat to a simmer, and then let it cook for about 20 minutes. 8. Thicken with some cornstarch, and add the sesame oil. Remove from heat, put into a bowl, and set aside. 3. Cook some noodles. This will work with a variety of different types of asian noodles: fresh ramen, lo mien, shanghai noodle. Cook according to the instructions on the package. It’s best if it’s a bit undercooked. Drain them, and then toss with a bit of oil to stop them from sticking together. To serve, you put the sauce into a bowl, and put it and all of the toppings onto the table. Then put a pile of noodles onto each persons plate. Then have each guest add as much sauce and toppings as they want, and dig in. # One plus one equals Two? My friend Dr24hours sent me a link via twitter to a new piece of mathematical crackpottery. It’s the sort of thing that’s so trivial that I might lust ignore it – but it’s also a good example of something that someone commented on in my previous post. This comes from, of all places, Rolling Stone magazine, in a puff-piece about an actor named Terrence Howard. When he’s not acting, Mr. Howard believes that he’s a mathematical genius who’s caught on to the greatest mathematical error of all time. According to Mr. Howard, the product of one times one is not one, it’s two. After high school, he attended Pratt Institute in Brooklyn, studying chemical engineering, until he got into an argument with a professor about what one times one equals. “How can it equal one?” he said. “If one times one equals one that means that two is of no value because one times itself has no effect. One times one equals two because the square root of four is two, so what’s the square root of two? Should be one, but we’re told it’s two, and that cannot be.” This did not go over well, he says, and he soon left school. “I mean, you can’t conform when you know innately that something is wrong.” I don’t want to harp on Mr. Howard too much. He’s clueless, but sadly, he’s a not too atypical student of american schools. I’ll take a couple of minutes to talk about what’s wrong with his stuff, but in context of a discussion of where I think this kind of stuff comes from. In American schools, math is taught largely by rote. When I was a kid, set theory came into vogue, but by and large math teachers didn’t understand it – so they’d draw a few meaningless Venn diagrams, and then switch into pure procedure. An example of this from my own life involves my older brother. My brother is not a dummy – he’s a very smart guy. He’s at least as smart as I am, but he’s interested in very different things, and math was never one of his interests. I barely ever learned math in school. My father noticed pretty early on that I really enjoyed math, and so he did math with me for fun. He taught me stuff – not as any kind of “they’re not going to teach it right in school”, but just purely as something fun to do with a kid who was interested. So I learned a lot of math – almost everything up through calculus – from him, not from school. My brother didn’t – because he didn’t enjoy math, and so my dad did other things with him. When we were in high school, my brother got a job at a local fast food joint. At the end of the year, he had to do his taxes, and my dad insisted that he do it himself. When he needed to figure out how much tax he owed on his income, he needed to compute a percentage. I don’t know the numbers, but for the sake of the discussion, let’s say that he made$5482 that summer, and the tax rate on that was 18%. He wrote down a pair of ratios:

$\frac{18}{100} = \frac{x}{5482}$

And then he cross-multiplied, getting:

$18 \times 5482 = 100 \times x$

$98676 = 100 \times x$

and so $x = 986.76$.

# Skirt Steak with Shoyu Gastrique

I made an amazing dinner tonight, out of a total ad-lib. So I want to write it down so I’ll remember it. This turned out to be the best steak I’ve ever made.

### The Steak

• 1 pound skirt steak
• Kombu leaves
• 1 teaspoon finely minced garlic
• 1 teaspoon finely minced ginger
• 1/4 cup soy sauce
• 1/4 cup mirin
• 1/4 cup sake
1. Mix together the liquid ingredents in a baking dish. dip the steak into it, to coat both sides.
2. Press kombu leaves into both sides of the steak, and then put it in the dish, and leave it in the fridge for a couple of hours.
3. Take the steak out, pat dry.
4. Toss the steak on a very hot grill, and cook for 2 minutes on one side, and about one minute on the other.
5. Let rest for a few minutes, then slice on the bias. (Save any juices that drip off while it’s resting, and add them to the sauce!)

### The Sauce

• 1/4 cup sugar
• 1/4 cup water
• 1/4 cup apple cider vinegar
• 1/4 cup sake
• 1 tablespoon shoyu
1. Mix together the sugar and water, and cook on high heat, whisking until the sugar is dissolved.
2. Keep cooking on high heat until all the water evaporates, the sugar starts to caramelize, and turns amber.
3. Add the cider and sake, and reduce the heat. Then whisk vigorously until everything is dissolved. (When you add the liquids to the caramel, it will seize up; you need to whisk until it’s redissolved.
4. Turn off the heat, then add the shoyu and any juices that dripped off the steak.

That’s it. Best damned steak ever.

# Truth in Type Theory

Now, we’re getting to the heart of type theory: judgements. Judgements are the basic logical statements that we want to be able to prove about computations in type theory. There’s a basic set of judgements that we want to be able to make.

I keep harping on this, but it’s the heart of type theory: type theory is all about understanding logical statements as specifications of computations. Or, more precisely, in computer science terms, they’re about understanding true logical statements as halting computations.

In this post, we’ll see the ultimate definition of truth in type theory: every logical proposition is a set, and the proposition is true if the set has any members. A non-halting computation is a false statement – because you can never get it to resolve an expression to a canonical value.

So remember as we go through this: judgements are based on the idea of logical statements as specifications of computations. So when we talk about a predicate P, we’re using its interpretation as a specification of a computation. When we look at an expression 3+5, we understand it not as a piece of notation that describes the number 8, but as a description of a computation that adds 3 to 5. “3+5” not the same computation as “2*4” or “2+2+2+2”, but as we’ll see, they’re equal because they evaluate to the same thing – that is, they each perform a computation that results in the same canonical value – the number 8.

In this post, we’re going to focus on a collection of canonical atomic judgement types:

$A \text{set}$
This judgement says that A is a set.
$A = B$
A and Bare equal sets.
$a \in A$
a is an element of the set A
$a_1 == a_2 \in A$
$a_1$ and $a_2$ are equal members of the set $A$.
$A$ is a proposition.
The proposition $A$ is true.

The definition of the meanings of judgements is, necessarily, mutually recursive, so we’ll have to go through all of them before any of them is complete.

An object $A$ is a Set
When I say that $A$ is a set in type theory, that means that:

• I know the rules for how to form the canonical expressions for the set;
• I’ve got an equivalence relation that says when two canonical members of the set are equal.
Two Sets are Equal

When I say that $A$ and $B$ are equal sets, that means:

• $A$ and $B$ are both sets.
• If $a$ is a canonical member of $A$, then $a$ is also a canonical member of $B$, and vice versa.
• If $a$ and $b$ are canonical members of $A$, and they’re also equal in $A$, then $a$ and $b$ are also equal canonical members of $B$ (and vice versa).

The only tricky thing about the definition of this judgement is the fact that it defines equality is a property of a set, not of the elements of the set. By this definition, tt’s possible for two expressions to be members of two different sets, and to be equal in one, but not equal in the other. (We’ll see in a bit that this possibility gets eliminated, but this stage of the definition leaves it open!)

An object is a member of a set
When I say $a \in A$, that means that if I evaluate $a$, the result will be a canonical member of $A$.
Two members of a set are equal
If $a \in A$ and $b \in A$ and $a = b$, that means when if you evaluate $a$, you’ll get a canonical expression $a$; and when you evaluate $b$, you’ll get a canonical expression $b$. For $a == b$ to be true, then $a$, that is, the canonical expressions resulting from their evaluation must also be equal.

This nails down the problem back in set equivalence: since membership equivalence is defined in terms of evaluation as canonical values, and every expression evaluates to exactly one canonical expression (that’s the definition of canonical!), then if two objects are equal in a set, they’re equal in all sets that they’re members of.

An object $A$ is a proposition
Here’s where type theory really starts to depart from the kind of math that we’re used to. In type theory, a proposition is a set. That’s it: to be a proposition, $A$ has to be a set.
The proposition $A$ is true
And the real meat of everything so far: if we have a proposition $A$, and $A$ is true, what that means is that $a$ has at least one element. If a proposition is a non-empty set, then it’s true. If it’s empty, it’s false.

Truth in type theory really comes down to membership in a set. This is, subtly, different from the predicate logic that we’re familiar with. In predicate logic, a quantified proposition can, ultimately, be reduced to a set of values, but it’s entirely reasonable for that set to be empty. I can, for example, write a logical statement that “All dogs with IQs greater that 180 will turn themselves into cats.” A set-based intepretation of that is the collection of objects for which it’s true. There aren’t any, because there aren’t any dogs with IQs greater than 180. It’s empty. But logically, in terms of predicate logic, I can still say that it’s “true”. In type theory, I can’t: to be true, the set has to have at least one value, and it doesn’t.

In the next post, we’ll take these atomic judgements, and start to expand them into the idea of hypothetical judgements. In the type-theory sense, that means statements require some other set of prior judgements before they can be judged. In perhaps more familiar terms, we’ll be looking at type theory’s equivalent of the contexts in classical sequent calculus – those funny little $\Gamma$s that show up in all of the sequent rules.