logical

I didn't get this so strongly before, but there's a correspondence between the language and structures of first-order logic, and the signatures and units of PLT Scheme (as well as the signatures and structures of ML). I guess the analogy is something like: "language::signature as structure::unit."

As a concrete example, a first-order language might just have equality (=), and a 2-arity P relation. Once we have a language, we can start writing statements in that language. Here are two statements using the language:

• for all x, y, z: P(x, y) and P(x, z) implies y = z


• for all x: there exists y: P(x, y)

These two sentences, taken together, are trying to say "P must be a relation that represents a total function". These sentences don't have a true or false value without being evaluated in the context of some structure. A structure tells us what domain of thingies (the universe) we're iterating over when we say "for all" or "there exists", and also provides a concrete definition for the relations of the language.

There are some structures that might satisfy this, and other structures that don't. Structures that satisfy the sentences we care about are called "models". One example of such a model for those two sentences might be the natural numbers (0, 1, 2, ...), where the interpretation of P is:

P(x, y) if and only if y = square(x)

But an example of a similar structure that wouldn't fit the above conditions would be natural numbers under a P that's not a function relation, like:

P(x, y) if and only if x < y

and so we'd say that this structure isn't a model of those sentences.

Programmers have an intuitive idea about this: it's similar to the distinction between "interface" and "implementation": the language provides the interface, and the structures provide implementations for that language. And when we have an interface, we usually have some implicit idea of how that interface should behave; if we have an interface called Stack, we have an expectation about what it should do. We can make those assumptions explicit by writing contracts or predicates with that interface: the things that satisfy our expectations are good implementations.

Again, to make this concrete, when we're programming with signatures and units, we first have to specify the things we're going to be fiddling with. For example, a signature like:

  ;; A function^ model consists of a universe of elements,
  ;; and a 2-place predicate P between elements.
  (define-signature function^ (universe
                               P))

gives us a language for talking and using units that implement this signature. For example, to build a unit where P is the squaring relation, we can do this:

  (define-unit squaring@
    (import)
    (export function^)
    (define universe (list 0 1 2 3 4 '>4))
    (define (P x y)
      (cond 
        [(equal? x '>4)
         (equal? y '>4)]
        [(> (* x x) 4)
         (equal? y '>4)]
        [else
         (equal? y (* x x))])))

(I'm defining the P function a bit peculiarly since I want the universe of elements to be finite.)

But again, not all implementations of the function^ signature will do the right thing. Here's a structure that doesn't satisfy the intent of the function^ signature.

  (define-unit less-than@
    (import)
    (export function^)
    (define universe '(1 2 3))
    (define (P x y)
      (< x y)))

How do we capture intent? We want to be able to catch implementations that don't do what we expect, and one way is to write code to exercise the units. Here's one example:

  ;; function-model?: function@ -> boolean
  ;; Checks to see if the given unit satisfies what we
  ;; expect out of functions, that their domain is total
  ;; and that each element of the domain maps to
  ;; just one element of the range.
  ;;
  ;; In first-order logic:
  ;;    (for all x, y, z: P(x, y) and P(x, z) implies y = z)
  ;;    and
  ;;    (for all x: there exists y: P(x, y))
  (define (function-model? model@)
    (local ((define-unit-binding a-model@
              model@ (import) (export function^))
            
            (define-unit function-tester@
              (import function^)
              (export)
              (and (for-all* (lambda (x y z)
                               (implies? (and (P x y) (P x z))
                                         (equal? y z)))
                             universe universe universe)
                   (for-all* (lambda (x)
                               (exists? (lambda (y) (P x y))
                                        universe))
                             universe))))
      (invoke-unit
       (compound-unit/infer
        (import)
        (export)
        (link a-model@ function-tester@)))))

(There are a few definitions I've left out here; see logic-practice.ss for the other definitions.)

Once we have this, we can now check to see if squaring@ and less-than@ satisfy the function-model? predicate.

> (function-model? squaring@)
#t
> (function-model? less-than@)
#f