Formal Methods of Software Design, Eric Hehner, segment 5 page 1 out of 2
[1] Functions. Here’s what a function looks like. This notation is not standard. I was using a notation involving lambda because I thought it was standard, but my students all said they had never seen it, so I guess it isn’t standard any more, and I might as well use a notation that looks nice and serves its purpose well. A function introduces a new local variable, or you could call it a parameter if you want. And that’s really the one and only purpose of a function. The angle brackets show the scope of that local variable, so we could call them scope brackets. D is the domain of the function, or you could say the domain of the variable, or the type of the variable. Variables are for substitution, and the domain says what expressions can be substituted for the variable. The body is any expression whatever. The only thing different about it is that it can make use of the new local variable. All the normal rules of proof apply within the body, plus [2] one extra rule, namely v colon D, which says the variable is in the domain. [3] Here’s an example function, and a picture of it. It introduces local variable n with domain nat, and the body or result is n plus 1. In the picture, the domain is the left column, and the result is the right column, and the arrows are saying that each domain element is mapped to its successor. This is called the successor function. Now it doesn’t really matter what name you choose for the variable. [4] If you rename the variable to some fresh name, it’s an equivalent function. [5] There’s a domain operator that gives the domain of a function, so [6] if we apply it to the successor function, we get nat. A function can be [7] applied to any element of its domain. We say f applied to x or [8] just f of x. x is called the argument or operand. Some people like to put [9] parentheses around the argument, and you can if you like. You could [10] put them around the function if you like. But they’re not necessary unless [11] the precedence requires them. A function is really just an operator that you define yourself, like [12] minus, or [13] negation, and we don’t put parentheses around the operand there, although we could. When we [14] apply the successor function to 3 we [15] substitute 3 for n in the body, [16] and get 4. A function of [17] 2 variables is really just a function of 1 variable whose body is a function of 1 variable. You can [18] see that max here is a function by the scope brackets and arrow, and its [19] variable is x, and its [20] domain is xrat. And its [21] body is a function of 1 variable. [22] So we can apply max to an argument, [23] say 3, and since the result is a function, we can [24] apply it to an argument, say 5, and [25] find out that the max of 3 and 5 is 5. Now a warning. [26] You might be used to writing function application like this, with parentheses and commas. In this course, that’s a bunch of arguments, and [27] you get a bunch of results, and that’s probably not what you meant.
[28] If a function has a binary result, we call it a predicate. This function tells whether its argument is even or not. And if a [29] function has a predicate result, we call it a relation. So a relation is a function of two variables that has a binary result. The divides function here tells whether its first argument divides into its second argument with no remainder. That makes the [30] even function equal to the divides function applied to the single argument 2.
[31] There’s an operator called selective union that takes two functions and produces a new function. The [32] domain of the new function is the union of the domains of the two operands. The [33] result of the new function, when applied to argument x, is the following. If x is in the domain of f, then the result is what f would give. If not, the result is what g would give. So f otherwise g is mostly like f, except when f doesn’t apply, and then it’s like g.
[34] Next I want to give you some abbreviations you can use for functions. [35] The first one is for functions of 2 or more variables that all have the same domain. [36] Just group the variables and write the domain once. That’s like programming languages where you can declare several variables of the same type together. For the next abbreviation, I’ll use the [37] successor function as an example. The abbreviation is [38] to leave out the domain. We do that only if everyone knows what the domain is, maybe because we say all
Formal Methods of Software Design, Eric Hehner, segment 5 page 2 out of 2
domains today are nat. So then we don’t need to write them. Or, sometimes the domain doesn’t matter for the point being made, and we can leave it out. In [39] the next example, we have a very small domain, just the number 2, but that’s irrelevant for the example. What’s relevant is that the body doesn’t use the variable. That’s called a constant function. And then there’s no need to [40] write a variable. And you don’t need scope brackets to show the scope of a variable if you don’t write any variable. So 2 arrow 3 is a little function with domain 2 and result 3. It maps 2 to 3. And finally, [41] we could abbreviate so much that we leave out both the variables and the domains. In this example, that would be [42] just x plus 3. Sometimes people say an expression is a function of its variables. But you might not be able to see all the variables, and you don’t know what order they come in, so you can’t apply an expression like this.
[43] The final topic this lecture is scope and substitution. A function introduces a local variable, which the body of the function can refer to. But the body can also refer to other variables, which are nonlocal. Some people use the word [44] global instead of nonlocal. Some people call them [45] bound and free variables. Some people call them [46] hidden and visible variables. Some people call them [47] private and public variables. That’s a lot of terminology. I’ll just stick with local and nonlocal. [48] A variable is local to an expression if the variable is introduced, using the function notation, within the expression. Otherwise it’s nonlocal. [49] In this example, I’ve just shown the variables, and left out the other parts of the expression. [50] There is one local variable introduction, introducing local variable x, and that local variable occurs once. [51] There are two nonlocal variables. One of them is also named x, but it’s not the same variable as the local x. It occurs once. The other nonlocal variable is y and it occurs twice. [52] Now [53] here’s an example in which x is introduced locally, twice. The [54] outer function’s x is used twice. That outer function is being applied to 3, so 3 should replace the outer function’s x at both its occurrences. Like [55] this. But it doesn’t replace the inner function’s x. [56] And one last example. [57] Again there’s a function within a function. The outer function [58] introduces variable y, and it occurs 3 times. This outer function is being applied to argument [59] x, which is a nonlocal variable. So this x has to replace all 3 occurrences of y. The problem is [60] this y. The nonlocal x has to replace it, but putting nonlocal x here will make it look like the local x of the inner function. We won’t be able to tell them apart, so we must not do that. Before we can apply the outer function to its argument, [61] we have to rename the inner x to something that won’t cause confusion. [62] Now we can apply the outer function, and replace all occurrences of y with x.
I’ll have a little more to say about functions later, but that’s enough for now.