Logic in CS-1 and CS-2

Juris Reinfelds

Klipsch School of Electrical and Computer Engineering
New Mexico State University
P.O. Box 30001, Dept. 3-O,
Las Cruces NM 88003 U.S.A.
(505) 646-1231 fax: (505) 646-1002
juris@nmsu.edu

1.0 Introduction

If we believe that logic is the backbone formalism of computer science, then it seems logical that logic should shape the backbone of the foundation course for CS majors. Unfortunately most humans are not logical. As shown by the Reid survey [Reid 1994], far too many universities still teach a first course built around the syntax, semantics and sequential problem solving methodology of Wirth's elegant, but somewhat outdated, teaching language Pascal, while too many others are engaged in an irrelevant debate whether to replace Pascal with Ada or C++. Only a handful of universities have extended their first course to two paradigms (usually functional followed by imperative) [Joosten et al. 1993] [Lambert et al. 1993] and they have discovered that in this way more material can be taught because of the natural separation of the concern for "how an algorithm works" (functional view) from the concern for "how to implement it with pointers or arrays" (imperative view).

2.0 Our Course

In 1991 we obtained a NSF Curriculum Development Grant to go a step further and to include all three problem solving paradigms (logical, functional and imperative) into a two-semester, 4-credit hours per semester foundation course for CS majors. Initially we had planned to coordinate our two CS courses with two 3-credit hour discrete mathematics courses, but although we received a follow-up grant from NSF in 1992, it became unavoidably obvious that our mathematicians were content with small adjustments and reorganizations of the traditional material of their discrete mathematics courses while computer science needed dicrete mathematics courses with a strong emphasis on logic.

This dilemma ended our collaboration with the mathematics department and we proceeded on our own to restructure the foundation courses in CS. We observed that syntactic and semantic complexity increases from logic programming to functional programming to imperative programming and we decided to present the paradigms in this order. We chose a spiral approach with three five-week sections in each 15 week + exam week semester. More detailed descriptions of our course appear elsewhere [Reinfelds 1995a,b 1996a,b].

2.1 Spiral Approach

A spiral approach facilitates the transition from old to new courses, as the first week of each section of the second semester is obliged to review the corresponding section of the first semester. This also reinforces key concepts in the minds of relatively inattentive students who did not pay enough attention in the first semester to activate their long-term retention capabilities at that time.

2.2 Similarities Between Paradigms

We discovered surprising similarities between the paradigms so that most concepts learned in one section were reinforced in a subsequent section and no concepts were sufficiently contradictory to require re-learning. For example, the concept of guarded statements appears in different forms in all theree paradigms. Another example: a logic program consists of a database and a query; a functional program consists of a script and an expression and a C program consists of function and variable definitions and an expression that has to be evaluated: "main();" that is always the same and therefore is not written explicitly.

2.3 Equational Logic Applied to CS

One of our key problems was logic itself, which was to be taught in the discrete mathematics courses that fell by the wayside vey early in the project. We were rescued by the appearance of Equational Logic and the book [Gries & Schneider 1993] which presents introductory discrete mathematics in terms of equational logic. This was a brilliant and effective solution to our problem, but it was not possible to convince the Mathematics Department to change its traditional approach. Ideally, Mathematics Departments should teach discrete mathematics to computer science students in a framework that is essential to computer science. In practice such an insight might take a very long time. Hence we decided to include some equational logic into the logic section of our courses.

With very few lecture-minutes at our disposal, we had to be very selective to provide a tiny but non-trivial glimpse of the power and beauty of equational logic. First we decided to emphasize the separation of the truth-table "interpretation" approach from the "axiomatic" approach where inference rules control purely syntactic pattern matching of "well-formed-formulas". Unnecessary confusion arises if these independent approaches to logic are not clearly separated from the beginning. The first semester concentrates entirely on the truth-table approach. We practice truth-table skills with examples that have relevance to pre- and post-conditions of programs, functions and loops, to guarded statements, to assertions about the state of computation and about digital circuits. We then concretize these abstractions with logic programs that we implement in Prolog.

In the second semester we introduce axiomatics. Starting with the axioms of equivalence and with the inference rules of equational logic we can already apply the axiomatic method to the formalization of vague stories (e.g. Portia's dilemma Gries & Schneider p.86) to develop a skill that is of great importance in the shaping of vague, incomplete and often contradictory problem descriptions and requirements analyses into a consistent and clear specification. The software engineers have long claimed that CS foundation courses have neglected and ignored the creation of specifications and the design of programs. In this way we can turn our full attention to these matters and learn logic in the process.

In a good class we can introduce all axioms of equational logic. In a slower, weaker class we can stop at the most important logical connectives. In all cases we can awaken awareness and develop some skill in the application of logic formalism to clarify a vague story and to produce a concise and clear formal specification from that story. Again we use logic programming to concretize the otherwise very abstract exercises, axioms and rules of inference.

3.0 Our Experience and Some Results

It is almost impossible to do proper educational experiments to compare what effects two different courses have on the subsequent development of the students who take one or the other of these courses. First, it would take at least 10 years to follow a group of students through their university studies and for sufficiently long into their careers, to see if the foundation course made a difference and by then the course would be obsolete. Second, it is almost impossible to form two truly equivalent student groups as there are so many significant factors that bias student group composition [Reeves et al. 1995].

We first taught the first semester of our course in Spring 1992 and the second semester in Spring 1993. Today the CS department at NMSU has decided to teach all sections of the first two semesters of our first course in this way. A set of lecture and laboratory notes have been developed for each semester. Colleagues who have not been involved in our course development have successfully taught the course a number of times. As the following figures show, a long and steep decline of student enrolments into our first course has been stopped and reversed since the introduction of our course in spite of a university-wide decline in the freshman student intake over the last several years.

Since students pay substantial fees and invest large amounts of time into courses, an indirect measure of success is given by the number of students who choose to take the course. Both CS 171 and CS 272 are compulsory courses for students majoring in Computer Science, but in contrast to CS 171, which is often taken by students of other disciplines, CS 272 is taken mainly by students who are serious about majoring in Computer Science and who have tested their resolve by passing CS 171. CS 272 is therefore a better indicator of the number of subsequent Computer Science Major graduates than CS 171.

As shown by the bar chart with respect to the left-hand scale of Table 1, our student numbers were in a steep decline for five years from 1984 to 1988 at which time the number of students taking CS 272 stabilized at about 43 plus or minus a few students. This number is too low to sustain a viable major because some students will drop out or transfer to another major and the university administration insists on a minimum of at least 10 students in all undergraduate courses.

The numbers remained constant from 1988 to 1992 while we were teaching a 70's style CS-2 course based on the syntax and semantics of one imperative programming language. As soon as the new course was introduced and in spite of a university-wide decline of the overall freshman student intake (shown as a curve with respect to the right-hand scale), the new course has helped to create a significant turnaround in student numbers taking CS 272 to a more healthy 58 in 95/96.

For long forgotten historical reasons the numbering of compulsory computer science major courses started with CS 271. Quite recently the department renumbered the same course as CS 171 to better reflect its status as the first computer science course for students who have chosen to major in Computer Science.

CS 271/171 experienced an even steeper decline in student numbers than CS 272. Once again the introduction of the new course coincided with the turnaround of student enrolments that now have shown a modest increase for four years. It is of course impossible to say whether the new course had any decisive role in the student number improvement. Since the department is now considering a return to a program-guessing course based on the syntax of C or C++, it will be interesting to see how the student numbers evolve over the next five years.

Table 2 shows the Student numbers for CS 271/171 (bar chart with respect to the left-hand scale) and the new student intake for the whole university (curve with respect to the right-hand scale). With the pool of incoming first year students decreasing by about 100 per year, the increase in CS 271/171 enrollments is quite interesting.

In summary, there is an over 20% increase in student numbers in the first course and an over 40% increase in the student numbers in the second course since the new courses were first-taught. This is against an over 20% decrease in the yearly new student intake of the university over the same period of time. Most students agree that an exposure to more than one way of problem solving gives them a better foundation for subequent CS courses as well as for the workplace. It seems that logic, the formal backbone of our professional knowledge and reasoning ability, has found its proper place in the foundation course. As in other sciences, the foundation concepts of subsequent computer science courses can be introduced early. Most importantly, we have been able to show students that there are many important and powerful programming and problem solving methodologies in computer science, each of which applies best to a certain class of problems and our students have acquired some ability to recognize which methodology best applies to a given problem.

4.0 Teaching of Applied Logic.

There are two major problems that have to be solved if we want to make logic accessable and useful to computer scientists. First, as Dijkstra has claimed for many years, logicians learn, teach and explain logic in order to facilitate the study of logic itself. Computer scientists have to apply logic and as in any branch of mathematics, application skills are different from "pure mathematics" skills.

Secondly, most logic books skip over the overall structure of logic and assume equality either as a god-given additional axiom or as the consequence of implication in both directions. Both points of view slow down comprehension for a typical freshman student to whom implication is foregn and an understanding of equality is fuzzy. Equational logic is a delightful exception in the handling of equality.

With the exception of [Hogger 1990], most logic books do not clearly define the framework of logic as consisting of two separate and independent lines of enquiry. One is based on model theory with truth tables encapsulating all models of a wff. The other is based on proof theory where purely syntactic derivations using appropriately chosen axioms and inference rules surprisingly and amazingly give the same results as truth tables and interpretations. Some recent books [Grossman & Tremblay 1996] and [Hein 1995] have made an effort to remedy these problems, but a lot more work needs to be done before we can introduce logic to our students with the simplicity and elegance that it deserves.

5.0 Acknowledgements

The author is grateful to a number of colleagues for comments, suggestions, ideas and laboratory materials, especially to Mikhail Auguston, Hue McCoy, Ann Gates, Ming Sheu, Mannish Mamnani and Jay Turley. Many thanks to our students and teaching assistants who helped to make each subsequent version of the course a little better than its predecessor. Many thanks to the National Science Foundation for two research grants without which our course would not have gotten off the ground.

The two figures and their descriptions are taken from the author's paper at the Australasian Computer Science Education Comference, Sydney, Australia, July 2-6, 1996 [Reinfelds (1996b)].

6.0 References