P-Normal Pixley

P-Normalization is a technique for simplifying Pixley programs. It is related to A-Normalization, but quite a bit simpler.

A Pixley program is in P-Normal form if and only if:

• All let* forms bind a single expression to a single symbol; and
• All cond forms have a single test branch and a single else branch.

The Pixley 2.0 distribution contains a P-Normalizer, written in Pixley. It converts arbitrary Pixley programs into P-Normal form.

Motivation

There are several reasons why I wrote the P-Normalizer.

One was simply to write a non-trivial program in Pixley besides the Pixley interpreter itself.

Another is that an implementer might find it easier to write an interpreter or compiler for P-Normal Pixley; this gives them the option of P-Normalizing the Pixley source before input. Certainly, when I was implementing Pixley in C (for AmigaOS 1.3), I would have found the continuation code easier to formulate if the input program was in P-Normal form.

Yet another is to effectively criticize the design choice of putting let* and cond in Pixley, instead of let and if. My belief is that, if only these simpler forms were included in Pixley, the Pixley interpreter would be larger. P-Normalizing the interpreter, then (as a trivial second step), converting the P-Normal let*s and conds to lets and ifs, would allow one to check this belief -- however, I have not gotten so far as to actually do that, yet.

And the last reason I will mention here is that it is a step towards true A-Normalization of Pixley programs. This would be useful for my purposes, as one of my long-held goals for Pixley was to write a totality checker for Pixley programs, in Pixley, much as I have done in the past with Scheme.

However, useful A-Normalization requires that non-trivial expressions (such as calls to defined functions) occur let-bound in other expressions. For example, the first element of a list which represents a function application must be a symbol which is bound to the lambda being applied, rather than a literal lambda. Pixley is not really capable of converting expressions to such a form, because it lacks the ability to create new symbols.

There are a couple of ways around this, but they each have drawbacks.

The normalizer could be supplied with a list of symbols to be used during bound-conversion, but the user would need to provide a sufficient supply of symbols, and ensure that they don't clash with symbols in the program.

Or, a creative bending of the language could allow expressions to be bound to, not just symbols, but entire S-expressions, which we could generate in an infinite supply. While the resulting program could, e.g., be statically analyzed for totality, it would not be a Pixley program (because Scheme doesn't allow that kind of binding.)

Or, instead of converting to normal form, the program could simply check the input Pixley program and evaluate to a boolean indicating whether the program is in normal form or not. However, this would offload the work of doing the actual conversion to programmer, which is less than ideal.

Or, the normalizer could be written in some language besides Pixley, but given Pixley's "bootstrappability" roots, I'm not even going to consider that unless all else fails.

The thing is, I haven't decided how to approach the problem yet, so I will save "P-Normalization 2.0" for a later date. (Although, now that I've wriiten them all out, option #2 seems most appealing.)

Tests for the P-Normalizer

-> Tests for functionality "P-Normalize Pixley Program"

-> Functionality "P-Normalize Pixley Program" is implemented by
-> shell command "script/tower.sh src/pixley.pix dialect/p-normal.pix %(test-body-file)"

let* gets expanded into a series of nested, one-binding, let*s.

| (let* ((a (quote a)) (b (quote b))) (cons a b))
= (let* ((a (quote a))) (let* ((b (quote b))) (cons a b)))

cond gets expanded into a series of nested, one-test, conds.

| (cond ((equal? a b) a) ((equal? b c) b) (else c))
= (cond ((equal? a b) a) (else (cond ((equal? b c) b) (else c))))

Expressions in a let* binding get P-Normalized.

| (let* ((g (let* ((a (quote a)) (b (quote b))) (cons a b)))) g)
= (let* ((g (let* ((a (quote a))) (let* ((b (quote b))) (cons a b))))) g)

Expressions in a let* body get P-Normalized.

| (let* ((c (quote c)))
|        (car (let* ((a (quote a)) (b (quote b))) (cons a b))))
= (let* ((c (quote c))) (car (let* ((a (quote a))) (let* ((b (quote b))) (cons a b)))))

Expressions in a cond test get P-Normalized.

| (cond
|   ((eq? (let* ((a (quote a)) (b (quote b))) a) (quote a))
|    (quote yes))
|   (else
|    (quote no)))
= (cond ((eq? (let* ((a (quote a))) (let* ((b (quote b))) a)) (quote a)) (quote yes)) (else (quote no)))

Expressions in a cond branch get P-Normalized.

| (cond
|   ((eq? (quote a) (quote a))
|    (let* ((a (quote a)) (yes (quote b))) yes))
|   (else
|    (quote no)))
= (cond ((eq? (quote a) (quote a)) (let* ((a (quote a))) (let* ((yes (quote b))) yes))) (else (quote no)))

Expressions in a cons get P-Normalized.

| (cons (quote x) (let* ((a (quote a)) (b (quote b))) (cons a b)))
= (cons (quote x) (let* ((a (quote a))) (let* ((b (quote b))) (cons a b))))

Expressions in a car get P-Normalized.

| (car (let* ((a (quote a)) (b (quote b))) (cons a b)))
= (car (let* ((a (quote a))) (let* ((b (quote b))) (cons a b))))

Expressions in a cdr get P-Normalized.

| (cdr (let* ((a (quote a)) (b (quote b))) (cons a b)))
= (cdr (let* ((a (quote a))) (let* ((b (quote b))) (cons a b))))

Expressions in a list? get P-Normalized.

| (list? (let* ((a (quote a)) (b (quote b))) (cons a b)))
= (list? (let* ((a (quote a))) (let* ((b (quote b))) (cons a b))))

Expressions in a quote do not get P-Normalized.

| (quote (let* ((a (quote a)) (b (quote b))) (cons a b)))
= (quote (let* ((a (quote a)) (b (quote b))) (cons a b)))

Expressions in a lambda body get P-Normalized.

| (let* ((a (lambda (x) (let* ((r (quote r)) (p (quote p))) x))))
|   (a (quote d)))
= (let* ((a (lambda (x) (let* ((r (quote r))) (let* ((p (quote p))) x))))) (a (quote d)))

Arguments of a function application get P-Normalized.

| (let* ((f (lambda (x) x)))
|        (f (let* ((a (quote a)) (b (quote b))) (cons a b))))
= (let* ((f (lambda (x) x))) (f (let* ((a (quote a))) (let* ((b (quote b))) (cons a b)))))