Prolog-style append

    Welcome to PowerLoom 3.0.1.beta

Copyright (C) USC Information Sciences Institute, 1997-2003.
PowerLoom is a registered trademark of the University of Southern California.
PowerLoom comes with ABSOLUTELY NO WARRANTY!
Type `(copyright)' for detailed copyright information.
Type `(help)' for a list of available commands.
Type `(demo)' for a list of example applications.
Type `bye', `exit', `halt', `quit', or `stop', to exit.


|= (demo 4)

Now reading from `PL:sources;logic;demos;append.ste'.
Type `?' at the pause prompt for a list of available commands.

;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

;;; Version: append.ste,v 1.14 2003/06/05 23:13:43 hans Exp

;;; Prolog-style `append' using implication rules
;;; =============================================

;;; This file demonstrates a Prolog-style definition of an `append'
;;; function using implication rules.  It also shows how to define
;;; and use total functions in PowerLoom.

;;; The best way to view this file is by calling `(demo)' and
;;; selecting it from the menu of example demos.  This demo assumes
;;; familiarity with some basic PowerLoom concepts which are described
;;; in the introductory demo (#1 on the demo menu) and other demos
;;; preceding this one.


;; Demo preamble:

|= (in-package "STELLA")
------ pause ------c


;; The module definition below is slightly different from the ones
;; seen previously, since it uses the `:shadow' keyword to shadow the
;; name `cons'.  This is necessary, since a STELLA class with the same
;; name is inherited from the STELLA module (PowerLoom's top-level
;; PL-KERNEL module currently :uses the STELLA module which causes
;; some name space pollution that will be eliminated in future
;; versions).  Without the shadowing declaration PowerLoom still would
;; have noticed the name conflict and asked the user whether to shadow
;; the name automatically.

|= (defmodule "PL-USER/PROLOG-APPEND"
  :shadow (cons))

|MDL|/PL-KERNEL-KB/PL-USER/PROLOG-APPEND

|= (in-module "PROLOG-APPEND")


|= (clear-module "PROLOG-APPEND")


|= (reset-features)

|l|(:EMIT-THINKING-DOTS :JUST-IN-TIME-INFERENCE)

|= (in-dialect KIF)

:KIF

;; We start by defining a logic concept to represent a Lisp-style cons
;; cell.  The concept is different from its Lisp analogue, since it
;; does not have any internal structure such as a `car' or `cdr' slot.
;; Instead, the semantics of constructing and appending cons-lists is
;; defined completely declaratively by the functions below and their
;; associated rules.

|= (defconcept Cons-Cell)

|c|CONS-CELL

;; Next we define a function `cons' that takes an arbitrary ?head
;; element and some pre-existing cons list ?tail and returns a new
;; cons list with ?head prepended to ?tail.

;; In a programming language such as Lisp or STELLA `cons' is a
;; constructor, i.e., for any set of legal input arguments, a new cons
;; cell gets allocated on the memory heap.  To reflect this
;; characteristic in PowerLoom, we have to define `cons' as a total
;; function.  This will allow PowerLoom to infer that for any legal
;; inputs ?h and ?t it follows that `(exists ?c (= (cons ?h ?t) ?c))'.
;; By default PowerLoom functions are not total (this is different
;; from Prolog) and the above inference is not warranted.  To specify
;; that `cons' is total we use the keyword axiom syntax `:total TRUE'
;; which simply expands to `(assert (total cons))'.  To specify a
;; keyword axiom for a unary relation such as `total' a value of TRUE
;; or FALSE must be specified.

|= (deffunction cons (?head (?tail Cons-Cell)) :-> (?cons Cons-Cell)
  :documentation "Add `?head' to the front of the cons-list `?tail'."
  :total TRUE)

|f|CONS

;; Next, we define the function `append'.  This function is not
;; specified as total, since it will be "computed" via a set of
;; implication rules:

|= (deffunction append ((?list1 Cons-Cell) (?list2 Cons-Cell)) :-> (?r Cons-Cell)
  :documentation "Append the cons-lists `?list1' and `?list2'.")

|f|APPEND

;; Let's start with creating the empty list:

|= (assert (Cons-Cell NIL))

|P|(CONS-CELL NIL)

;; Now we specify the rules that specify the semantics of `append'.
;; Each rule is a universally quantified KIF implication.  Top-level
;; free variables such as ?list1 and ?list2 are implicitly universally
;; quantified.

;; The first rule states that appending anything to the empty list NIL
;; simply returns the second list (similar to Prolog formulations, we
;; use `?result' as a kind of "output" variable):

|= (assert (=> (and (= ?list1 NIL)
                 (= ?list2 ?result))
            (= (append ?list1 ?list2) ?result)))

|P|(FORALL (?list1//NIL ?list2 ?list2)
   (<= (= (APPEND NIL ?list2) ?list2)
       TRUE))

;; The second rule handles the inductive case, where we split off a
;; head element of the first list and reduce the problem to appending
;; the shortened first list to the second:

|= (assert (=> (exists (?head ?tail ?rest)
              (and (= ?list1 (cons ?head ?tail))
                   (= ?rest (append ?tail ?list2))
                   (= ?result (cons ?head ?rest))))
            (= (append ?list1 ?list2) ?result)))

|P|(FORALL (?list1 ?list2 ?result)
   (<= (= (APPEND ?list1 ?list2) ?result)
       (EXISTS (?head ?tail ?rest)
          (AND (= (CONS ?head ?tail) ?list1)
               (= (APPEND ?tail ?list2) ?rest)
               (= (CONS ?head ?rest) ?result)))))

;; Various queries:

|= (retrieve all ?z
          (= ?z (append NIL NIL)))

There is 1 solution:
  #1: ?Z=NIL

;; The queries below generate actual cons-like structure with the help
;; of anonymous skolem individuals.  The generation of these skolems
;; is sanctioned, since `cons' was declared to be a total function:

|= (retrieve all ?z
          (= ?z (append (cons red NIL) NIL)))

There is 1 solution:
  #1: ?Z=(CONS RED NIL)

|= (retrieve all ?z
          (= ?z (append NIL (cons red NIL))))

There is 1 solution:
  #1: ?Z=(CONS RED NIL)

|= (retrieve all ?z
          (= ?z (append (cons red NIL) (cons blue NIL))))

There is 1 solution:
  #1: ?Z=(CONS RED (CONS BLUE NIL))

|= (retrieve all ?z
          (= ?z (append
                 (cons yellow (cons green NIL))
                 (append (cons red NIL) (cons blue NIL)))))

There is 1 solution:
  #1: ?Z=(CONS YELLOW (CONS GREEN (CONS RED (CONS BLUE NIL))))

;; Let's name a cons-cell (note, that our logic cons cells are different
;; from their programming languages analogues, since they are structure-
;; shared, i.e., whenever we mention `(cons green NIL)' we refer to the
;; same function term, while in the programming language there could be
;; multiple copies with identical structure):

|= (assert (= (cons green NIL) green-cons))

|P|(= (CONS GREEN NIL) GREEN-CONS)

;; Accessing the head element of green-cons:

|= (retrieve all ?m
          (exists (?t) (= (cons ?m ?t) green-cons)))

Processing check-types agenda...
There is 1 solution:
  #1: ?M=GREEN

;; Accessing both elements of green-cons: 

|= (retrieve all (?m ?t)
          (= (cons ?m ?t) green-cons))

There is 1 solution:
  #1: ?M=GREEN, ?T=NIL

|= 

Finished demo `PL:sources;logic;demos;append.ste'.

|=