#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
;; Matt Kaufmann
;; Here are some games with "partial functions".....

Event: Start with the initial nqthm theory.

Definition: s-plus (x, y) = if x

then if y then x + y

else f endif else f endif

Event: Introduce the function symbol apply of 2 arguments.

;; Example 1:  a simple total reflexive function that's actually
;; the identity function on natural numbers.

;; dcls, add-axioms, and rewrite rules for g-cost and g (6 events)

Event: Introduce the function symbol g-cost of one argument.

Event: Introduce the function symbol g of one argument.

Axiom: g-defn g (x) = if g-cost (x)

then if x ≃ 0 then 0

else 1 + g (g (x − 1)) endif else apply ('g, list (x)) endif

Axiom: g-cost-defn g-cost (x) = if x ≃ 0 then 1

else s-plus (1, s-plus (g-cost (x − 1), g-cost (g (x − 1)))) endif

Theorem: g-cost-opener ((x ≃ 0) → (g-cost (x) = 1)) ∧ ((x ≄ 0)

→ (g-cost (x) = s-plus (1, s-plus (g-cost (x − 1), g-cost (g (x − 1))))))

Theorem: g-opener ((x ≃ 0) → (g (x)

= if g-cost (x) then 0

else apply ('g, list (x)) endif))

∧ ((x ≄ 0)

→ (g (x)

= if g-cost (x) then 1 + g (g (x − 1)) else apply ('g, list (x)) endif))

Theorem: g-theorem g-cost (x) ∧ (g (x) = fix (x))

;; Example 2:  Silly factorial

Definition: isub1 (x) = if negativep (x) then − (1 + negative-guts (x))

else x − 1 endif

;; dcls, add-axioms, and rewrite rules for fact-cost and fact (5 events).
;; Note that we don't try to make a rewrite rule for the nonterminating
;; case.  Also, since our function isn't reflexive and we are only interested
;; in termination, we only bother to prove a rewrite rule for opening up
;; fact-cost, not one for opening up fact.

Event: Introduce the function symbol fact-cost of one argument.

Event: Introduce the function symbol fact of one argument.

Axiom: fact-defn fact (x) = if fact-cost (x)

then if x = 0 then 1

else fact (isub1 (x)) endif else apply ('fact, list (x)) endif

Axiom: fact-cost-defn fact-cost (x) = if x = 0 then 1

else s-plus (1, fact-cost (isub1 (x))) endif

Theorem: fact-cost-opener-numberp ((x = 0) → (fact-cost (x) = 1)) ∧ ((x ≄ 0) → (fact-cost (x) = s-plus (1, fact-cost (x − 1))))

;; Now let's first note when fact IS defined.

Theorem: fact-defined-numberp (x ∈ N) → fact-cost (x)

Theorem: fact-defined-other ((x ≃ 0) ∧ (¬ negativep (x))) → fact-cost (x)

;; Next, let's show that fact is undefined on the negatives by
;; showing that the cost is arbitrarily high (the usual trick
;; used for analogous v&c$ proofs).

Definition: fact-undefined-ind (x, n) = if n ≃ 0 then t

else fact-undefined-ind (1 + x, n − 1) endif Theorem: fact-undefined-numberp-lemma-inductive-step ((n ≄ 0) ∧ fact-cost (− x) ∧ (fact-cost (− (1 + x)) → ((n − 1) ≤ fact-cost (− (1 + x))))) → ((fact-cost (− x) < n) = f)

Theorem: fact-undefined-negativep-lemma fact-cost (− x) → ((fact-cost (− x) < n) = f)

Theorem: fact-undefined-negativep negativep (z) → (fact-cost (z) = f)

;; finally, we put this all together

Theorem: fact-domain fact-cost (x) ↔ (¬ negativep (x))

;; Example 3:  triple reverse
;; First, ordinary reverse, and proper list recognizer

Definition: rev (x) = if listp (x) then append (rev (cdr (x)), list (car (x)))

else nil endif

Definition: plistp (x) = if listp (x) then plistp (cdr (x))

else x = nil endif

Definition: length (x) = if listp (x) then 1 + length (cdr (x))

else 0 endif

;; dcls, add-axioms, and rewrite rules for rev3-cost and rev (6 events)

Event: Introduce the function symbol rev3-cost of one argument.

Event: Introduce the function symbol rev3 of one argument.

Axiom: rev3-defn rev3 (x) = if rev3-cost (x)

then if listp (cdr (x))

then cons (car (rev3 (cdr (x))),

rev3 (cons (car (x), rev3 (cdr (rev3 (cdr (x)))))))

else x endif else apply ('rev3, list (x)) endif

Axiom: rev3-cost-defn rev3-cost (x) = if listp (cdr (x))

then s-plus (1,

s-plus (rev3-cost (cdr (x)),

s-plus (rev3-cost (cdr (rev3 (cdr (x)))), rev3-cost (cons (car (x),

rev3 (cdr (rev3 (cdr (x)))))))))

else 1 endif

Theorem: rev3-cost-opener (listp (cdr (x)) → (rev3-cost (x)

= s-plus (1,

s-plus (rev3-cost (cdr (x)),

s-plus (rev3-cost (cdr (rev3 (cdr (x)))), rev3-cost (cons (car (x),

rev3 (cdr (rev3 (cdr (x)))))))))))

∧ ((cdr (x) ≃ nil) → (rev3-cost (x) = 1))

Theorem: rev3-defn-opener (listp (cdr (x)) → (rev3 (x)

= if rev3-cost (x)

then if listp (cdr (x))

then cons (car (rev3 (cdr (x))),

rev3 (cons (car (x), rev3 (cdr (rev3 (cdr (x)))))))

else x endif else apply ('rev3, list (x)) endif))

∧ ((cdr (x) ≃ nil) → (rev3 (x) = x))

Definition: rev3-induction (x, n) = if (n ≃ 0) ∨ ((n − 1) ≃ 0) then t

else rev3-induction (cdr (x), n − 1) ∧ rev3-induction (cdr (rev3 (cdr (x))), (n − 1) − 1)

∧ rev3-induction (cons (car (x), rev3 (cdr (rev3 (cdr (x))))), n − 1) endif

Theorem: length-0 ((length (x) = 0) = (¬ listp (x))) ∧ ((0 = length (x)) = (¬ listp (x)))

Theorem: rev3-length-and-definedness-lemma (length (x) = n) → (rev3-cost (x) ∧ (length (rev3 (x)) = n))

Theorem: rev3-defined rev3-cost (x)

;; Now, just for fun, we'll show in the rest of these "rev" events
;; that rev3 is rev.  Note that we've already shown that rev3 is
;; "total" in the event just above.

Event: Disable rev3-cost-opener.

Theorem: app-assoc append (append (x, y), z) = append (x, append (y, z))

Theorem: rev-rev plistp (x) → (rev (rev (x)) = x)

Theorem: plistp-rev plistp (rev (x))

Theorem: plistp-append plistp (append (x, y)) = plistp (y)

Theorem: plistp-cdr (plistp (x) ∧ listp (x)) → plistp (cdr (x))

Theorem: listp-append listp (append (x, y)) = (listp (x) ∨ listp (y))

Theorem: rev-prop plistp (x) → (rev (x)

= if listp (cdr (x))

then cons (car (rev (cdr (x))),

rev (cons (car (x), rev (cdr (rev (cdr (x)))))))

else x endif)

Theorem: rev-prop-rewrite plistp (x) → ((listp (cdr (x))

→ (rev (x)

= cons (car (rev (cdr (x))),

rev (cons (car (x), rev (cdr (rev (cdr (x)))))))))

∧ ((cdr (x) ≃ nil) → (rev (x) = x)))

Event: Disable rev.

Theorem: listp-rev listp (rev (x)) = listp (x)

Theorem: length-rev3 length (rev3 (x)) = length (x)

Theorem: rev3-nil (rev3 (x) = nil) = (x = nil)

Theorem: length-cdr-rev3 listp (x) → (length (cdr (rev3 (x))) = (length (x) − 1))

Theorem: rev3-rev-lemma (plistp (x) ∧ (length (x) = n)) → (rev3 (x) = rev (x))

Theorem: rev3-rev plistp (x) → (rev3 (x) = rev (x))

Index

app-assoc, 6 apply, 1–3, 5

fact, 3 fact-cost, 3, 4 fact-cost-defn, 3 fact-cost-opener-numberp, 3 fact-defined-numberp, 3 fact-defined-other, 3 fact-defn, 3 fact-domain, 4 fact-undefined-ind, 3 fact-undefined-negativep, 4 fact-undefined-negativep-lemma, 4 fact-undefined-numberp-lemma-in

ductive-step, 4

g, 2 g-cost, 2 g-cost-defn, 2 g-cost-opener, 2 g-defn, 2 g-opener, 2 g-theorem, 2

isub1, 2, 3

length, 4, 6, 7 length-0, 6 length-cdr-rev3, 7 length-rev3, 7 listp-append, 6 listp-rev, 7

plistp, 4, 6, 7 plistp-append, 6 plistp-cdr, 6 plistp-rev, 6

rev, 4, 6, 7 rev-prop, 6 rev-prop-rewrite, 7 rev-rev, 6 rev3, 4–7 rev3-cost, 4–6 rev3-cost-defn, 5 rev3-cost-opener, 5 rev3-defined, 6 rev3-defn, 5 rev3-defn-opener, 5 rev3-induction, 5, 6 rev3-length-and-definedness-lem

ma, 6 rev3-nil, 7 rev3-rev, 7 rev3-rev-lemma, 7

s-plus, 1–3, 5