Rick Astley and Church Encodings

This past week was both fun and stressful. In this newsletter, I'm gonna move back a bit to the format I had when I initially started writing, i.e. write about a topic I learned the past week. That said, I'll also include some details about my first UDLS (more on what that is later)

This week started the same way that every other week starts: the morning after a late and rather frustrating night of trying to finish more of the week's CPSC 509 homework. By Monday I was probably working on it for the fifth day in a row, and sadly I haven't made much progress on it. That's not to say that the homework itself is impossible to do; I just probably lack the same level of understanding that some of my other classmates have on the material. That said, the past week's homework was quite long, and included a flurry of concepts such as

* proof by coinduction * substitution and binding * alpha/aleph equivalence * call-by-value vs. call-by-reference

it was definitely one of the more difficult homeworks by far, and I think this was supported by the fact that an anonymous student in the class asked for an extension (which William surprisingly agreed to). The extra day meant that the homework was due November 12, and so my Remembrance Day was filled with 509.

Once that was finished, I began working on a joint presentation for 509 with my classmate. We had chosen Church Encodings for the topic of our presentation, and that's the topic that I'll also write a bit about today.

As it turns out, all you really need to express any form of computation are just 3 constructs, illustrated below

x         ; variables
t t       ; application
λx. t     ; abstraction

this was the result of the Church-Turing thesis, and has since been the plague of undergraduates and graduates alike taking a class in programming languages. But it turns out that we can take this even further and represent the set of Natural numbers (0 inclusive) with this λ-calculus. Here are some examples:

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f(f x)
3 = λf. λx. f(f(f x))
...

0 can be thought of a construct which consumes some function f and some value x, and simply evaluates to x, while 1 is the same, except that it evaluates to f x, or a single (1) application of f to the value x. You can probably see where this is going. These are called the church numerals or encodings. A general equation for the nth church numeral is given below:

n = λf. λx. f^n x
; where f^n means apply f, n times to an argument x

Of course, no system of numbers is complete without a way to manipulate them, and it turns out that there's a way to encode arithmetic operations of church encodings with the λ-calculus

succ(n)   = λn. λf. λx. f (n f x)
add(m, n) = λm. λn. λf. λx. m f (n f x)

I've left out some other operations, but I feel like the examples above really illustrate the abstraction afforded by the λ-calculus.

Our presentation is nearly complete, but I hope we're able to fit it all into 30min (or less).

Outside of schoolwork, on Friday I gave a UDLS talk. A UDLS (Un-Distinguished Lecture Series) is a series of talks held mainly by the Computer Science Graduate Student Association at UBC. It's a chance for grad students to give a talk about any topics of their choice (although giving a talk about their research area is considered a faux pas), and generally practice their public speaking.

Even after I've worked as a TA for a couple of years, and given a fair share of presentations, I still get incredibly anxious before any presentation. I would honestly dread giving an update on our team's work during company all-hands when I was on internships, and talking in front of a large crowd is something that I generally try to avoid. I realize that this is something I need to get more comfortable with, so I decided to give a talk on rickrolling.

I thought it went decently, considering I wasn't really able to practice for it, and people who attended the talk generally seemed to have enjoyed it. As it would turn out, I got immediately rickrolled by a prof who attended the talk

Imagine giving a presentation about rickrolling and then getting immediately rickrolled. I hate you @wilbowma pic.twitter.com/GWp2xUVCuA

— James Yoo (@yoo_hoo_yoo) November 14, 2020

I honestly couldn't believe it.

That's gonna be all for this week. I'm surprised I managed to keep this habit of writing a newsletter every week so far. Hopefully I keep it going.