Lecture 3: Conditionals, Recursion and Lists

* This document is in preparation *

Remember - all expressions in this file can be evaluated
Special Forms are not evaluated in the usual way.
Boolean valued functions usually begin with is_
POP2000 Types.
The if expr₁ then expr₂ else expr₃ end if
Arithmetic in POP2000
The factorial function - an example of recursion
POP2000 evaluates expressions in an Eager way.
Lists are Compound Data.
The empty list
Making Lists.
Two Identities which hold for POP2000 Lists

Remember - all expressions in this file can be evaluated

You will find it worthwhile to read these notes on-line using UMASS POP2000 as a browser because every POP2000 expression occurring on a line by itself can be run. You can then try changing it and seeing what happens. Do not be afraid of playing with the machine - you cannot break it!

Special Forms are not evaluated in the usual way.

As we have seen the standard way to evaluate a POP2000 expression is to evaluate the function and arguments and then to apply the function to the arguments.

This rule does not hold for certain special forms. Examples of special forms we have seen so far are:

Lambda Abstraction

An expression such as \x. x*x is an example of the lambda abstraction special form. We can think of this as having a pattern described by:

   \ formals . body

You can think of this as evaluating to itself, with a rule for applying it to arguments (strip off \ and formals and substitute...) In the Lambda Calculus, there is only ONE special form, namely lambda abstraction. Having a small number of special forms is mathematically desirable, since the number of different cases to consider in mathematical analysis is reduced. However, in creating a practical programming language, certain other special forms are usually introduced. Where possible, these are made exactly equivalent to forms that can be expressed just using the Lambda Calculus.

Defining a variable

   Definition variable = expression End;

This special form evaluates the expression and binds the variable to the resulting value.

Conditional Expressions - the `if` construct.

POP2000 provides conditional expressions in which a condition (an expression which can have a boolean value) or conditions are used to choose which of a number of other expressions is to be evaluated. The simplest form of conditional in POP2000 is the special form:

 if condition then expr₁ else expr₂ end if

It evaluates condition. If condition evaluates to true the result is obtained by evaluating expr₁. If condition evaluates to false then the result of the if expression is obtained by evaluating expr₂.

In POP2000 it is an error for the condition to evaluate to anything other than true or false.

[WHY does it have to be a special form? Could it NOT be a special form? ].

Boolean valued functions

Functions which return a boolean value (true or false ) are often called "predicates". By convention, predicates have a name which begins with is_. Certain common predicates like '<' are exceptions to this rule.

Symbols

An isolated POP2000 identifier can be quoted, for example 'a. As such, it is called a symbol, and is a member of one of the basic datatypes of POP2000.

  'CaT'

is a symbol distinct from

  'cat'

This reflects the fact that in POP2000 case is significant, as it is in C, but not in Scheme or Pascal.

The form expr.symbol is an expression.

In POP2000 the construct

    expr.symbol

is an expression exactly equivalent to expr 'symbol'. Why does the language support this minor syntactic variant? This was done to provide syntactic continuity between POP2000 classes, which are functions mapping from symbols to values and constructs of other languages (Java, SML, Modula...) which play a similar role, though with a more restricted semantics.

POP2000 Types.

Objects which can exist in an implementation of POP2000 belong to exactly one basic type. The built-in types are:

    Boolean,Char,Null,Number,Pair,
    Procedure,String,Symbol,Vector,Application,Theorem

With each of these basic types there is associated a class. In POP2000 a class is a function which provides a basic collection of capabilities for recognising, creating and manipulating members of a type or types. Each type-name above has a corresponding class-variable which is bound to a class-function which provides basic support for members of that type, so that Boolean is the class-function associated with the type Boolean. To recognise whether a particular datum d belongs to a given type, we have the following construct Class . ? d

    Boolean.? d       is d a boolean?
    Char.? d          is d a character?
    Composite.? d     is d a composite expression?
    Null.? d          is d null?
    Number.? d        is d a number?
    Pair.?  d         is d a pair?
    Procedure.? d     is d a procedure, that is a function object.
    String.? d        is d a string, e.g. `the fat cat`
    Symbol.? d        is d a symbol, e.g. 'x'
    Theorem.? d       is d a the member of type Theorem?
    Vector.? d        is d a vector of values, e.g. {2,3,4}

You will doubtless recall that the form Class.? is shorthand for for Class '?'.

For any Class, the expression Class.? is a predicate for recognising members of that class.

There is a convention in POP2000 that identifiers beginning with an upper-case letter are the names of classes (a concept related to type). The predicates listed above, which recognise members of the basic types of POP2000 which do not overlap, that is for a given datum d, Class.? d will only evaluate to true for precisely one of the basic classes. There may be others basic types, e.g. files, and, in some environments, the widgets or windows which support graphical user interfaces.

The POP2000 language system "knows" quite a lot about the types of data that the built-in functions can operate on, and is able to detect certain errors as you compile code you have written. For example if you try to compile

Definition funny =
    \x. x + (y>z)
End

you will get an error message, because the system knows that y > z is a boolean, and you can't do arithmetic on a boolean. POP2000 has a limited built-in ability to infer the types which a user-defined function can manipulate.

Subdivisions of the Number Type

. The type Number has a number (some pun intended..) of sub-types.

    Int         Fixed precision integers, at least 30 bits of precision
    Integer     Arbitrary precision integers.
    Rational
    Float
    Double
    Complex

If "<" means "set inclusion", then the following hold:

    Int < Integer < Rational < Number
    Float  < Number
    Double < Number
    Complex < Number

These inclusion relations are necessitated by closure requirements. The sum of the rationals 1/2+1/2 is the integer 1, so the set of POP2000 Integers actually must be included in the POP2000 rationals. This is not true of the Float type - the sum 0.5+0.5 is the Float 1.0, and not the integer 1.

We shall not be concerned with vector and char

. In this class we shall not be concerned with the types vector, char.

Arithmetic in POP2000

Arithmetic operations are denoted by the conventional symbols:

There are also the usual algebraic and trancendental functions. They operate on integers, rationals, floating-point representation of reals, complex numbers. Try:

    sqrt -1;

the answer is the complex number:

    0.0+1.0i

Comparisons between numbers are denoted by the conventional symbols.

 < > <= >=

The factorial function - an example of recursion

The well known factorial function can be defined using the recurrence relations:

    0! = 1
    n! = n(n-1)!

These translate into POP2000 as follows:

Definition factorial =
    \n. if n=0 then 1 else n*factorial(n-1) end if
End;

factorial 5;

120

Try evaluating factorial 1000 , and factorial 1000 / factorial 999.

POP2000 evaluates expressions in an Eager way.

The rule that POP2000 evaluates the arguments of an expression before applying the function is called eager evaluation, or call-by-value. Some functional languages, such as Haskell, are lazy, and evaluate no expression unless it is actually needed. They have a better logical structure (e.g. if does not need to be a special form in these languages), but are hard to make efficient.

Lists are Compound Data.

So far we have seen that POP2000 has numbers, booleans and functions as objects that a program can use. These are simple data-types, which we can regard as having no internal structure to be explored. POP2000 provides a general-purpose compound data-type, the List. A sequence of expressions, separated by commas, and enclosed in square brackets is itself an expression, whose value is a list. For example:

    [1,2,3,4]

is a list.

The empty list

The empty list, denoted by [] has no elements in it. It is the only member of a distinct class, Null The predicate:

    Null.?

recognises the empty list. It is an error to apply the functions front or back to the empty list.

    front [];

Error: PAIR NEEDED
Culprits: (),
In file: /users/users3/fac/pop/poplocal/local/POP2000/lean3.lam

Calling sequence:
    front
This error report was prepared for Robin Popplestone
 by Jeremiah Jolt, your compile-time helper.

Making Lists.

Quotation allows us to make constant lists. However we also want to allow a program to make lists that the programmer has not explicitly created. This is done with the function cons

     cons x y

makes a list whose front is x and whose back is y . So to make a list containing just the number 23 we do:

   cons 23 []

    [23]

Now let's define a function to make a "sandwich" list:

Definition sandwich =
    \ x y. cons x (cons y (cons x []))
End;

This could be written, equivalently but more conveniently, as

Definition sandwich =
    \ x y. [x,y,x]
End;

So:


    sandwich 1 2;

evaluates to:

    [1, 2, 1]

Two Identities which hold for POP2000 Lists

POP2000 is subject to the mathematical laws:

    front (cons x y) = x
    back (cons x y) = y

The Theorem Type

We can't use the theorem type until we have a considerably more sophisticated understanding of the language, but in essence a theorem is a statement that is guaranteed to be true in a correctly implemented POP2000 system.

As an example, the theorem

    |- All x y.  front (cons x y) = x

follows immediately from the built-in axioms of POP2000.

The only theorem-constructing functions available in POP2000 are guaranteed to create valid theorems. So, the predicate-call

    Theorem.?  x

is not asking if x is true - it's asking if x is a member of the type Theorem. If it is it's guaranteed to be true - the good news. The bad news is that the built-in functions for constructing theorems only make very simple steps in proof. So that it is not easy or automatic to make theorems of any profundity.

A comparison with the SML and Java languages.

The Class concept in POP2000 has some superficial syntactic resemblence to the Class concept of Java and the structure and type concepts of SML. It differs from both these language in that POP2000 classes are first-class objects. In Java a class cannot be the value of a variable of the language. Likewise in SML a class can only be the value of a compile-time variable in a functor.

The built-in type-inference of POP2000 is much more restricted than is the Hindley-Milner type system of SML. However, this deficiency is made up for by the existence of theorems, which, following Milner, are a data-type all of whose members are guaranteed to express facts valid in a correctly-implemented POP2000 system.

Our approach to theorem-proving is not foundational, since there is a rich set of axioms which say, for example, that POP2000 contains a correctly implemented representation of the integers. In this we differ from the HOL system, which creates its theories from very the simple foundation of the lambda-calculus itself.