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

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@
(export function^)
(define universe (list 0 1 2 3 4 '>4))
(define (P x y)
[(equal? x '>4)
(equal? y '>4)]
[(> (* x x) 4)
(equal? y '>4)]
(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@
(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^)
(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))
(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@)
> (function-model? less-than@)


It finally feels like spring has arrived here in Worcester. The flowers are blooming from the trees, in great white poofy and pink blossoms. After my first winter here on the East Coast, it feels glorious to stand outside and just soak in the sun.

This semester is finally over. I still feel a little unsatisifed with my performance in Dan‘s logic class; the simplest things trip me up. Ever time I do a logic session, I come out feeling mentally pummeled. Brain squish just like grape! But not because the material’s necessarily difficult, but just that I come in with so much mental confusion.

For example, I got confused with the concepts of Skolem Hull and the Herbrand universe, which are different concepts. The Skolem Hull submodel only contains points that are interpretations of all the nameable elements of a language. A Herbrand universe, on the other hand, is a set containing only the nameable terms themselves. A hash collision.

We talked about models that include “junk” (elements that can’t be named by terms) and “confusion” (named terms that go to the same element). It’s funny, though, how the terms of logic are adopted by other subcultures, things like “compactness” and the “no junk, no confusion” properties, and in ways that are totally different from the definitions in mathematical logic.

I should probably spend a few more days in the sun and try to weed out the junk and confusion in myself, the ill-formed and redundant thoughts.