This is Bill Farmer again, and welcome back to McMaster University course, Computer Science 1JC3, Introduction to Computational Thinking. We're continuing with the topic of logic. And we talked about the need for Boolean expressions.
Boolean expressions allow us to make decisions without being able to make decisions. We can't skip code. And this would mean that we would have programs that really...
would be very inflexible. So we're going to talk first about conditional expressions. A conditional expression is an expression that depends on the value of a Boolean expression. That's simply what it is. And in Haskell We write conditional expressions as if-then-else expressions.
So we say if c, then e1, else e2. Now e1 and e2 should have the same type. and C will be a condition. So it will be a Boolean expression.
And the meaning of this is, if C is true, we return the value of E1. If C is false, we get the value of E2. That's basically how it works. And these expressions allow us to skip code, which is crucial.
So here's a simple example down here. It's the absolute value function for integers. And what we've done here is we've defined the app's integer of n.
It's going to be equal to the value of this conditional expression. And that value depends on the value of the input n. If n is non-negative, we return n. Otherwise, we return minus n, just like you would expect for an absolute value function. Okay, another useful construct in Haskell are guarded function definitions.
So this is a way of defining a function in a compact form where we don't have to use a bunch of if-then-else statements. Basically, the way it works in Haskell is if we have a set of arguments here, inputs, We return these values, e1 or up to en, depending on the values of certain guards. So here we have a guard, g1, and if this guard turns out to be true, then the definition of f applied to these x's will be e1.
Likewise, if the guard is true, then the definition of f applied to these x's will be e1. Where g is true, then the definition of f applied to these x's will be e and so forth for all the different guards. You can have any number of guards. So that's basically what a guarded function definition is.
And down here we have an example. It's the same function as before, but now we're going to define it without an if-then-else statement. And we have two guards. One, n is negative.
The other, n is non-negative. And as we know, when n is negative, we want to return minus n. And when n is...
non-negative we return n. So in both cases we're always returning a positive value. So those are guarded function definitions. Another very useful statement is a case statement.
It is a generalization of a conditional statement. So a Haskell case statement looks like this. And we have an expression E. And we check the value, or ASCO will check the value of E. And then it will try to match it against certain patterns.
We'll be talking a lot more about patterns as we go along. It will try to match it against these patterns, and the first pattern it matches, then it will return the corresponding value. So if it matches the pattern P2, it will return the value of E2, whatever that expression is. And here's an example.
This is a function that maps a bool to an int. Remember, int is the type of machine integers, and we're going to map... false to zero and true to one and so right here is our case expression we have b will be our boolean expression which happens to be just the input the input is a boolean value boolean a variable boolean value and if b is false this is our pattern this is a pattern that matches false we get zero if it matches the pattern true we get one okay so that's That's pretty simple. That's what a case statement is. Case statements are quite useful.
And now I want to take a little break, talk about someone we've already mentioned. His name is... is Alonzo Church. He was an American logician, mathematician, computer scientist. We've already run across him because he's the person who first showed that there are undecidable decisions.
problems. So he's a person who first showed that Leibniz's dream that we can solve basically any problem with computation is not possible. But he's most famous for developing a model of computation called the Lambda Calculus.
And this is based on lambda application and function abstraction. And he used this lambda calculus, remember this is a model of computation, to show that there is a function. there is an undecidable decision problem. And the problem he showed that was undecidable is that first-order logic is undecidable. This is called Church's theorem.
So the decidability problem for first-order logic is if you have a first-order formula, can you decide if that formula is always true or not? In other words, is it valid or not? And he showed that there is basically no program.
No programming his model of computation or no, for him, no lambda expression, which will allow us to solve that problem. Now, another person who also showed that there were undecidable decision problems was Alan Turing. He did this almost in the same time.
Alan Turing was one of the students of church, and he did it using a different model of computation. which we now call Turing machines. And so he actually, his way of doing it is closer to computing than we would say Alonzo Church's.
But Alonzo Church's model of lambda calculus and Turing... model of Turing machines are both full models of computation. They're both equivalent and they capture what we believe is computation. And so he's known for the Church-Turing thesis and basically this thesis says that what we consider to be an intuitive computation, what we can do intuitively in terms of computation is is captured by either Church's or Turing's model.
He's also known for the Church-Rosser theorem, and he had an extraordinary number of very influential PhD students. So I just wanna point out something. If we look at Church up here, So here's Church.
He had an extraordinary number of PhD students. One of them was Turing. Another very famous student he had is Dana Scott. And Dana Scott had a student named Ken Coonan.
And Ken Coonan had a student named Bill Farmer. Ken Coonan is my PhD supervisor. Unfortunately, and sadly, I must say he died about a month ago. Dana Scott is still alive. Of course, Turing and Church are no longer with us.
Okay, so one of the things... Church did, because he developed this lambda calculus, and in many ways, his ideas of lambda calculus we see today in Haskell and in other forms. Functional programming languages.
So he originated what we call lambda notation. So this is a very precise and convenient way to specify anonymous functions. Here's what the notation looks like.
I'll basically circle it here. So I'll write it again here. We have lambda.
This is a Greek letter. It tells us we're going to be defining a lambda expression, which denotes a function. Then it has the input, which is we have a variable of type alpha, and then we have a dot here.
We don't really need a dot, but it's helpful to have a separator between the input and the output. The output is given by an expression, and this expression is... type beta and that defines a function like this a function from values of type alpha to values of type beta and when we apply that function to a basically take the body b right here and we replace all the x's with a that's how we do function application so here's an example Here's the lambda expression.
This defines a function that squares a real number. And so if I apply this function, we call it f, we apply it to 2, that's what it's like, and then we take 2 here, let me use a different, we're going to put 2 in for this x. and this x and that gives us 2 times 2 which is equal to 4. Okay so f denotes a squaring function and let me clean up things a little bit. If we look at how we define the function using the lambda expression here it is. Notice we defined the function without naming it.
We did name it, in fact, but we didn't have to name it. Okay, so in Haskell we have lambda expressions, but they're written like this. The backslash here is supposed to represent lambda. And x1 through xn are the variables.
E is the body. That's this. And we don't give the types. You don't have to give the types. So basically it says if we give it n inputs, it's going to return.
the value of that expression. So here is the same function I defined up here, defined in Haskell, backslash x, and then we have arrow x times x. And it's very useful to have these these lambda expressions these anonymous functions because sometimes you're doing programming and you want to manipulate a value you just create a function you feed that value into the function and you get the output and that's all you care about you never want to think about that function again so it's useful just to write down a function as a lambda expression Okay, so now we have a question.
I have a question for you. Consider the following lambda expression. Or, excuse me, following Haskell function. There it is.
It's a function that takes x and y and returns the square root of x minus y. So the question is, what is the value of f applied to 7? So you have a number of choices here. I will give you a moment to think about this. So if you want, you can stop your video.
Okay, I'm back. So let's remember this is a curried function. So f applied to 7 makes sense and it's going to be a function.
And so if we look at a here, this is wrong. This is not a function. This is not a function. It's going to be the value we get if we knew what the value y was. Now we have a function b.
And b takes an x and gives back the square root of x minus 7. But since 7 here is being applied to x, we want actually c. We want the function that takes y and gives back 7 minus y. The x gets filled in by 7. So this is correct. But this is also correct. Because this is a lambda expression that gives a function.
This is a function application which gives a function. And you can see what we have in parentheses is the same as f. In other words, what we have in parentheses is another way of writing down f.
So both of those are correct. Okay, so that completes our lecture, and that also completes this topic on logic. Thank you very much.
See you next time.