Short-Circuits in the Lambda Calculus

I recently gave a talk at Lambda Jam on building compilers/interpreters for a version of the lambda calculus extended with integers, booleans, if expressions, and binary arithmetic and relation operators. The list of binary operators included “or” and “and” for boolean values and of course this brought up the question of whether or not they do short-circuiting evaluation.

So what exactly is short-circuiting evaluation? Consider the expressions:

(let (x 1)
    (or (= x 1) (= x 2)))

This simple expression will return True is x is either 1 or 2, and False otherwise, but the idea of short-circuit evaluation is that the “or” operation should not evaluate it’s second argument if the first one returns True. This is because the expression (or True x) is always True, so there is no need to evaluate the x argument. In my implementation “or” and “and” do not perform short-circuit evaluation, as we can see if we print at different points in the evaluation.

(print
    (let (x 1)
        (or (print (= x 1))
            (print (= x 2)))))

This will prints: True False True.

Clearly this isn’t what we really want to happen, because if the second argument to or were a more complicated expression because it would waste a lot of time and processing power just to return an already evaluated True.

So how can we fix this? In my implementation there is one operator that already performs a sort of short-circuiting, the if expression. Consider the following code:

(let (x 1)
    (if (= x 1)
        (print (+ x 1))
        (print (- x 1))))

This expression just prints: 2. So how is short circuiting handled here, but not in the case of the “and” and “or” operators. The answer is that binary operations and if expressions are handled entirely differently by the CEK machine that evaluates expressions. In the case of is expressions it intentionally leaves code for the true and false branches unevaluated until after the condition has been evaluated, the way that this happens by building continuations is not important to understand why it behaves differently from the binary operations. In the case of binary operators such as “and” and “or”, all arguments are evaluated before the operation is applied, thus there is no opportunity for short-circuiting to occur.

How can we fix this? Desugaring. In many lisp or scheme like languages “or” and “and” are implemented as macros in order to deal with this short circuit evaluation, so how can a similar thing be done in our small extension of the lambda calculus.

Well we already have an if expression which can perform short circuit evaluation so consider the similarities between the following two snippets of code:

;; example with or
(let (x 1)
    (or (= x 1)
        (= x 2)))

;; short-circuiting with if
(let (x 1)
    (if (= x 1)
        (= x 1)
        (= x 2)))

Well that’s a little better, now the (= x 2) expression isn’t evaluated unless (= x 1) turns out to be false, but this still has a problem we evaluate the (= x 1) expression twice which is still wasteful.

We can fix that extra step of evaluation if we pull out the expression into a let so putting everything we’ve done so far together we finally have the following:

;; or desugaring
(or x y)
--->
(let (z x)
    (if z z y))

;; and desugaring
(and x y)
--->
(let (z x)
    (if z y z))

Taking this one step further, the core language implemented in my talk did not include let expressions, they were desugared in applications of lambda abstractions, so the final desugaring of these expressions will actually be

;; desugared or
(or x y)   --->   ((lambda z (if z z y)) x)

;; desugared and
(and x y)   --->   ((lambda z (if z y z)) x)

Thus as long as we have if expressions that correctly defer the evaluation of their arguments, then we can easily define the “or” and “and” operations without needing them to be built in as binary operations.

Better late than never… Teaching Languages.

I apologize for not posting in quite a while, I’ve been extremely busy with robotics for the past couple months. I was quite surprised to see that I had 9 pageviews today since I haven’t even checked this blog since probably mid September.

I have a handful of project ideas I’ve been trying to find the time to work on, and hopefully I will be able to blog about a few of them soon. I’ve been thinking a lot about a pure JavaScript implementation of C as both a cool compiler project, and potentially a very useful teaching tool. Speaking of teaching, I’ve also been trying to design a programming curriculum for the second semester of robotics. I’ve been tossing around several ideas about which languages I would like to introduce, and which directions I would like to take the class.

As far as language choices go, the students are learning RobotC in the first semester which is mostly similar to C, but programming for this year’s game doesn’t expose them to very much of C. So what should I try to teach in the second semester? The languages that I  have in mind are C, Haskell, Python, and Racket, possibly JavaScript. Let’s take a look at what each has to offer in both pros and cons.

C

Pros: C is a pretty standard first language in some sense, many modern languages take C’s syntax as a starting point. Students already have some familiarity with C from using RobotC.

Cons: Pointers seem to be notoriously difficult to learn. C is very low level, and not the easiest language to teach in a Windows environment. I think C will require a high cost of effort in teaching and learning for low returns in what the students will be able to program at the end of the semester.

Haskell

Pros: I love Haskell, it’s probably my favorite programming language. Pure functional language, makes reasoning about programs easier. Good environment to teach recursion.

Cons: Can be very theoretical in places. I don’t think I know how to motivate concepts such as monads or typeclasses.

Python

Pros: Pretty clean indentation based syntax. Batteries included, there’s a library for almost anything I think I would teach over the course of the semester. When treated as an imperative language, it is pretty similar to C semantically, building on stuff the students already know.

Cons: Still have to motivate and teach about objects, and the OOP paradigm, although this might not be such a bad thing. Might be too high level, and abstract away too many details, but this might not be so important if the goal is to teach programming.

Racket

Pros: SImilar to Python, very batteries included. Extremely minimal syntax. Multi-paradigm, allowing introductions to functional and OOP paradigms. Tons of educational materials available.

Cons: Minimal syntax, too many parens could be confusing. Functional programming might be weird coming from an imperative background.

Javascript

Pros:  Looks a lot like C. Sort of functional core language. Good for web stuff. Many interactive tutorials available online.

Cons: Prototype based object system. Weird scoping things.

My current line of thinking is to teach C alongside another language comparing and contrasting as we go. Right now I’m leaning towards Python or Racket as the second language, but haven’t made a decision. I think I’ll end up letting the students decide by giving a few examples of programs in each language and having them vote on which they would rather learn. I’d like to teach Racket because I have some ideas for cool projects that I’d like to implement in Racket, so teaching Racket at the same time would be nice, but Python is a great language too, so no decision quite yet.

As I put together a more concrete set of lecture notes, exercises, and projects I will be posting those and hopefully get back to posting more often. If anyone has opinions or ideas about this programming class for the new year please let me know, I’d love to hear others’ experience or thoughts on the situation.

Working with Joysticks.

This post will introduce the basics of programming for the logitech joysticks in RobotC. I will talk about include files in another post, but for now you need to know that whenever you want to use a joystick with RobotC you need to include the following line in your program.

#include "JoystickDriver.c"

Adding this line to your program gives you access to all of the functions and variables that RobotC needs to communicate with the logitech controllers.  So what do we need to know in order to use the joystick? The most important function you need to be familiar with is called getJoystickSettings,what it does is read in the current information from a joystick to your program each time you call it. The most important variable we need to deal with joysticks is named joystick, this variable is an example of what is called a struct* in C, but for now all you need to know is that it bundles together a set of variables that deal with the current state of the joystick. Let’s look at a simple example of this:

#include "JoystickDriver.c"

task main() {
    getJoystickSettings(joystick);
    motor[left] = joystick.joy1_y1;
    motor[right] = joystick.joy1_y2;
}

Now I’m sure you are wondering what joystick.joy1_y1, and joystick.joy1_y2 are, and the answer is that they are examples of those variables I mentioned above that are bundled up in joystick. Specifically the value joystick.joy1_y1 corresponds to the y-value of the left joystick on the logitech controller, and respectively the value joystick.joy1_y2 corresponds to the y-value of the right joystick. It is worth noting that joystick.joy1_y1 and joystick.joy1_y2 take on integer values between -128 and 127 (I will talk about types in RobotC in another post).

Now let’s walk through this program line by line and figure out what it does. We already know what lines 1-3 do since we already talked about #include, and we know what task main() is for, so we can start by looking at line 4.

    getJoystickSettings(joystick);

What does this line do? Well it looks sort of like a function call, and that’s exactly what it is, we are applying the getJoystickSettings function to the value joystick, and remember that joystick is one of those struct things that encapsulate a bunch of information about the state of the joysticks we are using. The result of calling the getJoystickSettings function is that the program looks at the current state of the joystick(s) you are using (which buttons are pressed, what value are the joysticks set at, etc…) and stores all of that data inside the joystick struct. For example if we are pushing the right joystick on our controller all the forward then getJoystickSettings(joystick)will cause joystick.joy1_y2 to take on the value -127 (this is just how the joysticks happen to work, and unfortunately it doesn’t quite match up with our expectations). Let’s look at the last lines of the program.

motor[left] = joystick.joy1_y1;
motor[right] = joystick.joy1_y2;

We learned about controlling motors in this post so we know what is happening here is that we are setting the speed of the motors (in percentage) based on the values of the left and right joysticks on the controller (joystick.joy1_y1 and joystick.joy2_y2 respectively).

What happens next in the program?

Nothing, actually. The program just ends after the second motor assignment, clearly this isn’t what we would like to happen, we would prefer if we could continually update the motor speeds based on whether or not we are moving the joysticks. To handle this we will need a new programming construct called a loop. The next post in this series will pick up with a discussion of making things in a program repeat using loops.

*: When I say that joystick is a struct here, what I actually mean is that the documentation doesn’t list the actual type of joystick, but a struct is the only thing that makes sense.

RobotC, What does it all mean?

In my last post on RobotC, I introduced programing in RobotC with the following piece of code:

 task main() {
     motor[left] = 100;
     motor[right] = 100;
     wait1Msec(1000);
 }

This time I want to examine this program line by line and explain exactly what each line is doing. I will do my best to explain this program in the simplest way possible, but unfortunately some things are best explained in comparison to programming in C. Here are two resources I’ve used in the past for details on C

1. Programming in C.

2. Learn C the Hard Way.

Don’t be afraid of the title of the second link, while it does eventually go into some more advanced topics it starts nearly from scratch, but it does assume some previous programming experience.

Now back to RobotC, starting with line 1:


task main() {

This declares the main “task”, this is in contrast to standard C where main is a function and is declared as


int main() {

In this piece of code “int” is short for integer a positive or negative whole number (or 0) with a range that depends on the computer you are using, but typically from −2,147,483,648 to 2,147,483,647.

In C main is a function that roughly contains all of the work that your program will do, in RobotC main serves the same purpose except that it is declared as a task. The opening brace ({) just indicates the beginning of the body of the main task/function, which ends on line 5 with a corresponding closing brace (}).

Remember I mentioned last time that we are assuming that we have already used the RobotC IDE to setup the motors on our robot, so that we have two motors one labelled left and one labelled right. Moving on to lines 2 and 3:

     motor[left] = 100;
     motor[right] = 100;

In this snipped of code motor[left] indicates that motor is what is called an array in C, I will first give a brief and very basic discussion of arrays in C and then tie that back in with RobotC. In C we can declare an array (say of integers) like this:


int an_array_of_ints[5] = {0,1,2,3,4};

In this we declare an array called “an_array_of_ints” (similar to “motor” in the RobotC example) which can hold 5 integers (ints). An array is sort of like a list of things (in this case ints) that will hold a specific and predetermined number of them (in this case 5). The braces here are the items that we are storing in the array. We can access an item in an array as follows, suppose we want an expression which will add together all the things in our array of ints.


an_array_of_ints[0] + an_array_of_ints[1] + an_array_of_ints[2] + an_array_of_ints[3] + an_array_of_ints[4];

This expression is identical to 1+2+3+4+5; notice that the first item of the array begins at index 0 and the last at index 4, this is just the way that the C programming language was designed, so all arrays are 0-indexed (begin at 0). We can also change the value of one of our array items say the third (that would be index 2, not 3!) like


an_array_of_ints[2] = 7;

So now our array contains these five numbers {0,1,7,3,4}.

I think we know enough now to explain what is going on in the Robot C example.

     motor[left] = 100;
     motor[right] = 100;

So motor is an array that is declared for us by the RobotC programming environment to allow it’s values to alter the power level of the motors attached to our robot. When we assign the value 100 to motor[left] and motor[right] when we compile and run our program on the NXT motors left and right will run at 100% power.

So last, but not least let’s address line 4 of our program:


wait1Msec(1000);

In this lat bit of code “wait1Msec” is a function applied to the argument 1000, I will cover functions, and how you can define your own in a later post, but they are (mostly) similar  to functions from math. In this case “wait1Msec” is a function that waits or pauses the program for it’s argument value in miliseconds, in this case 1000 miliseconds or 1 second. This allows the program to run for long enough to allow the motors to actually be set to 100% power. Without this function call everything happens so quickly that it will appear as if the program is doing nothing, this wait enables you to see that the motors do run and everything will work correctly.

After the function call above, the program ends with a closing brace (}) corresponding to the opening brace denoting the body of the main task. This concludes the program ending its run causing the motors and anything else to cease running.

Hopefully this post gives a better look into the specific workings and details of RobotC. I will continue this series on RobotC programming introducing “if-statements”, loops, servos, and functions.
If you have any questions please don’t hesitate to ask, and please point them out if you notice any errors in either my code or explanations.

Hello, RobotC

I’m going to start a series of posts on RobotC, which is the language we use to program robots for the First Tech Challenge (FTC) robot competition. As a preliminary note, there will be some things I do not cover in this blog mainly because they are particular details of the RobotC IDE (Integrated Development Environment) which we use to compose our programs, specifically all of my example programs on this blog will likely leave out any motor and sensor setup which is not an easy thing to write out from memory, and best done with the help of the RobotC IDE.

Here is an example of a first RobotC program:

 task main() {
     motor[left] = 100;
     motor[right] = 100;
     wait1Msec(1000);
 }

This is a simple program for a robot which we assume has two motors one called left and one called right. The program sets the motors to run at 100% speed for one second (1000 miliseconds) after which the program ends and the motors will stop.

In the next post we will analyze this program in a bit more detail, and explain exactly what each line in the program means.

Making a Racket

It’s about time for a new blog post, I haven’t been keeping up with this blog as well as I would like to, but I’ve been busy trying to get things in order for the coming semester. I volunteer as a programming mentor with a local high school’s robotics team, but I also have been trying to start grad school in computer science with the intention to study programming languages so I’ve been giving a lot of though recently to the issue of how to best teach programming languages to students who have never programmed before.

I’ve known about Racket for a while now, several of my friends used it in their first CS classes when I was in college, but I’ve never spent more than a few days at a time looking at it or playing around with it. I think I’ve finally decided to really take it seriously this time after finding out that Shriram Krishnamurthi will be offering an online version of his programming languages course at Brown for the first time starting on September 5th. As someone who wants to end up in grad school studying programming languages this is the first online course I’ve seen pop up that really excites me, and it gives me the incentive to start taking Racket seriously again.

I own a copy of the first edition of Essentials of Programming Languages (EOPL), and have been meaning to work through the book before starting grad school, so I think I will take the next month to start working through the book using Racket in order to prepare for the programming languages course in September and to get better acquainted with Racket. Hopefully I will keep to my word and start posting more regularly, I will try to post my solutions to the exercises in EOPL using Racket as I work my way through the book.

Tautology in Haskell

Just figured out how to turn on literate haskell mode in aquamacs, so I’m going to try this literate blogging thing again, by walking through the construction of a tautology checker in Haskell. I mentioned in my first post that I would be attending the Oregon Programming Languages Summer School (OPLSS), but I never made the time to blog about any of it, so this is the start of an attempt to rectify that.

Robert Constable gave a series of three lectures on the topic of "Proofs as Processes", and while I didn’t quite have the background to understand much of his talk, in his first lecture he mentioned a book "First Order Logic" by Raymond M. Smullyan. I managed to find the books at Powell’s in Portland and I will be basing the tautology checker in this post on the method of tableaux that is introduced early in Smullyan’s book.

For now all symbols used will be ascii renditions of what they are meant to look like.

 ~X should be read as "not" X.

 X /\ Y should be read as X "and" Y or the "conjunction" of X and Y.

 X \/ Y should be read as X "or" Y or the "disjunction" of X and Y.

 X => Y should be read as X "implies" Y.      

Smullyan begins his presentation of analytic tableaux by making note of certain relations that hold amongst these operators that hold for any interpretation. These rules are

If ~X is true then X is false.

If ~X is false then X is true.

If X /\ Y is true then X is true and Y is true.

If X /\ Y is false then either X is false or Y is false.

If X \/ Y is true then either X is true or Y is true.

If X \/ Y is false then X is false and Y is false.

If X => Y is true then either X is false or Y is true.

If X => Y is false then X is true and Y is false.

(needed citation)

Before introducing the notion of a signed formula, which Smullyan uses to introduce analytic tableaux, we will first need to come up with a Haskell datatype to represent logical formulas, but this follows fairly easily from the description of the opertators above.

> data Formula = Var String
>              | Not Formula
>              | And Formula Formula
>              | Or Formula Formula
>              | Implies Formula Formula
>              deriving (Read,Show)

This is a pretty straightforward definition of a logical formula in Haskell. A formula can be either a variable (Var) represented by a string, the negation (Not) of another formula, the conjunction (AND) of two formulas, thedisjunction (Or) of two formulas, or the statement that one formula implies another (Implies).

Now let’s get to work and introduce signed formulas which will end up being the driving force behind this tautology checker.

> data Signed = T Formula
>             | F Formula
>             deriving (Read,Show)

That is to say a signed formula is the same as a regular logical formula as defined above, except that we will now mark it with either a T or an F. These signed formulas must obey some rules in order to be useful though, specifically we will have that if X is a formula then the following hold:

TX is true whenever X is true, and false when X is false.

FX is true whenever X is false, and false when X is true.

Now we can write down the rules above using this new notion of a signed formula.

T~X -> FX

F~X -> TX

T(X /\ Y) -> TX, TY

F(X /\ Y) -> FX | FY

T(X \/ Y) -> TX | TY

F(X \/ Y) -> FX, FY

T(X => Y) -> FX | TY

F(X => Y) -> TX, FY

A brief note on the notation here, I am using the arrow (->) to roughly mean reduces to or something vaguely equivalent to that, similarly the bar (|) is the same symbol used in Smullyan’s book to represent the disjunction of the two options, that either could hold so we must consider each seaparately, and lastly the comma (,) also used in Smullyan’s book denotes that both of these conditions will hold if the left hand side of the arrow holds.

We can try to represent this using the datatypes we just defined.

> -- x :: Formula
> -- y :: Formula
> -- F (Not x) ...

Well we run into a problem pretty quick trying that, we need something to represent what’s going on the right hand side of the rules we just defined. Well everything on the right hand side of the rules above is either a signed formula, the notion that two formulas hold, or the notion that the formula branches into two signed formulas. Let’s come up with a new datatype to deal with this.

> data Tableaux = SF Signed 
>               | Both Signed Signed
>               | Branch Signed Signed
>               deriving (Read,Show)

This will allow us to express the branching and both notions that occur when reducing complex signed formulas, and now we could write a function to reduce a signed formula (SF) using the rules we just devised.

> reduce :: Signed -> Tableaux
> reduce (T f) = case f of
>              Not x -> SF (F x)
>              And x y -> Both (T x) (T y)
>              Or x y -> Branch (T x) (T y)
>              Implies x y -> Branch (F x) (T y)
> reduce (F f) = case f of 
>              Not x -> SF (T x)
>              And x y -> Branch (F x) (F y)
>              Or x y -> Both (F x) (F y)
>              Implies x y -> Both (T x) (F y)

I’m going to leave off here for now, and pick it up after I read a little further into the book. Check back soon for more updates to this post.