Natural Deduction and Language Semantics

Topics

• Natural Deduction
• Language Semantics via Natural Deduction
• From natural semantics to interpreters

Lecture notes in Racket (.rkt)

Natural Deduction

Natural deduction is a style of mathematical reasoning which has an especially close relationship with computing. We will use natural deduction in this class to write proofs, specifications, and define the semantics of programming languages which we build.

Our goal today is to learn the format of natural deduction proofs. We define natural deduction as a method for defining both specifications and proofs of propositions (rigorous statements).

We will learn natural deduction in a way which also introduces the upcoming homework on transitive closure.

Defining the Natural Numbers

Let’s start by defining proofs for natural numbers. There are two ways to build any natural number:

1. The constant 0 is a natural number.
2. If n is a natural number, (S n) is also a natural number.

We saw how to define the natural numbers via a term algebra over signature {0 ↦ 0, S ↦ 1}. Now we’ll see another way: using natural deduction rules.

In natural deduction, rules have the following format:

         Assumption 0, Assumption 1, ...
  Name  -----------------------------------
                    Conclusion

The rule says: “If we can prove Assumption 0, Assumption 1, …, then applying rule Name allows us to prove the Conclusion.” Some rules have no assumptions above the line – we call these “axioms,” because they represent statements we can make without requiring any proof.

The assumptions and conclusions are “propositions:” mathematical statements. In this case, propositions are of the form _ : nat which means “some object has type nat.” You should read : as “has type” and nat as “natural number.”

Example: Proving (S (S (S 0))) : nat

Let’s use these rules to prove that (S (S (S 0))) : nat (i.e., “3 is a natural number”):

Reading Rules Forward and Backward

The tricky part about natural deduction is that rules can be read either forward or backward. Consider the Add1 rule:

• (Reading “forward,” top-to-bottom): “If we have a proof of n : nat, then we can apply Add1 and prove (S n) : nat.”

• (Reading “backward,” bottom-to-top): “If we want to prove (S n) : nat for some n, then we can apply Add1 and simplify our task to proving n : nat – which may or may not be possible.”

To build a complete proof using natural deduction, we need two things:

1. (Local correctness) Each rule must be applied correctly
2. (Completeness) All leaves of the proof tree must be axioms

Here is an example that breaks local correctness:

This is not a valid usage of Add1: if we have (S n) on the bottom, we need n on the top. Here the top is 0, so the bottom should be (S 0) – instead, it has (S (S (S 0))).

Here is an example that breaks completeness:

The top of this proof is incomplete: (S B) : nat has not been proven. Each local application of Add1 is correct, but we’d eventually need to prove B : nat, which is not possible by any rule.

Exercise 1

Exercise 2

Exercise 3

Booleans

Let’s do another short example. We’ll define rules for constructing boolean expressions:

Exercise 4

Language Semantics via Natural Deduction

We will use natural deduction to specify the semantics (meaning) of programming languages. This will allow us to rigorously make clear exactly how programs are evaluated, to a degree that we could rigorously test or even prove properties about programs in our language.

Programming language semantics is a core topic in CIS352. There are several methods for specifying semantics:

1. Reference interpreter: “The semantics is whatever Python does.”
   • Upside: scales to complex languages
   • Downside: the host language may not have a well-defined meaning itself (e.g., C++ has undefined behavior)
2. Denotational semantics: Map the program into a mathematical domain.
   • Upside: mathematics is well-developed
   • Downside: complex for nontrivial features like loops
3. “Big-step” / natural semantics: Specify semantics via natural deduction.
   • Upside: we can often take the specification and directly build an interpreter (or compiler)
   • Downside: requires fully specifying the language, which may be impractical for truly production-grade languages

A Small Boolean Language

When we specify a language by natural deduction, we define a “reduction relation:”

e ⇓ v   “expression e evaluates to value v”

where e is an expression (something to be evaluated) and v is a value (a result). As our first example, consider a small boolean language:

(define (expr? e)
  (match e
    ['true #t]
    ['false #t]
    [`(&& ,(? expr? e0) ,(? expr? e1)) #t]
    [`(|| ,(? expr? e0) ,(? expr? e1)) #t]
    [_ #f]))

This is the term algebra over {true arity 0, false arity 0, && arity 2, || arity 2}. For example:

(expr? '(&& (|| false true) (|| true false))) ;; => #t

Values will be Racket’s booleans (#t and #f). Now we define the semantics – precisely when we can prove e ⇓ v:

Notice how in the And/Or rules we assume that there is a definition of and/or above the line. We are implicitly assuming a definition in the metalanguage (the language we use to define the language). In this case, we use Racket’s and/or as the metalanguage, but in general the metalanguage will be “mathematics.”

Exercise 5

Exercise 6

From Natural Semantics to Interpreters

A key insight of this course is that big-step natural deduction rules can be read as a recursive function. Each rule tells us: “to evaluate this kind of expression, evaluate the subexpressions and combine the results.” This is exactly what an interpreter does.

For our boolean language, the interpreter follows directly from the rules:

;; interp : Expr → Value
(define (interp e)
  (match e
    ['true  #t]
    ['false #f]
    [`(&& ,e0 ,e1)
     (and (interp e0) (interp e1))]
    [`(|| ,e0 ,e1)
     (or (interp e0) (interp e1))]))

Notice the direct correspondence:

• The True rule says true ⇓ #t – the interpreter returns #t for 'true.
• The And rule says: evaluate e0 to v0, evaluate e1 to v1, return (and v0 v1) – the interpreter does exactly that with recursive calls.

This pattern – writing natural deduction rules, then translating them directly into an interpreter – is the central technique we will use throughout the rest of CIS352. In our lecture on closure-creating interpreters, we extend this idea to a much richer language with variables, lambdas, closures, and environments.