Daniel al-Autistiqui schrieb:
> ;;; Rules begin here.
> (setf *rules* 'empty-stream)
>
> (remember-rule '(i
> ((? x) india)
> ((? x) india uniform)))
>
> (remember-rule '(ii
> (mike (? x))
> (mike (? x) (? x))))
>
> (remember-rule '(iii
> ((? l) india india india (? r))
> ((? l) uniform (? r))))
>
> (remember-rule '(iv
> ((? l) uniform uniform (? r))
> ((? l) (? r))))
>
> ;;; Rules end here.
>
> ;;; Assertions begin here.
> (setf *assertions* 'empty-stream)
>
> (remember-assertion '(mike india))
>
> ;;; Assertions end here.
>
> I understand what this is, but does anyone else? Help, please!
What part of it don't you understand?
You mention Hofstadter, who presented this kind of „logic system” in his
book.
He listed some axioms and here they are implemented in Lisp.
This program seems to be an automatic prover. Last year I also
programmed one for Hofstadters MUI.
André
--
On Mon, 12 Feb 2007 18:11:22 +0100, Andr� Thieme
<······························@justmail.de> wrote:
>Daniel al-Autistiqui schrieb:
>> ;;; Rules begin here.
>> (setf *rules* 'empty-stream)
>>
>> (remember-rule '(i
>> ((? x) india)
>> ((? x) india uniform)))
>>
>> (remember-rule '(ii
>> (mike (? x))
>> (mike (? x) (? x))))
>>
>> (remember-rule '(iii
>> ((? l) india india india (? r))
>> ((? l) uniform (? r))))
>>
>> (remember-rule '(iv
>> ((? l) uniform uniform (? r))
>> ((? l) (? r))))
>>
>> ;;; Rules end here.
>>
>> ;;; Assertions begin here.
>> (setf *assertions* 'empty-stream)
>>
>> (remember-assertion '(mike india))
>>
>> ;;; Assertions end here.
>>
>> I understand what this is, but does anyone else? Help, please!
>
>What part of it don't you understand?
>You mention Hofstadter, who presented this kind of �logic system� in his
>book.
>He listed some axioms and here they are implemented in Lisp.
>This program seems to be an automatic prover. Last year I also
>programmed one for Hofstadters MUI.
>
>
Well, for one thing, _GEB_ has in chapter VIII a more complex system
called "Typographical Number Theory" (with all its numerals,
variables, terms, etc.) How would that be rendered in LISP?
daniel mcgrath
--
Daniel Gerard McGrath, a/k/a "Govende":
for e-mail replace "invalid" with "com"
Developmentally disabled;
has Autism (Pervasive Developmental Disorder),
Obsessive-Compulsive Disorder,
& periodic bouts of depression.
[This signature is under construction.]
Daniel al-Autistiqui <·········@hotmail.invalid> writes:
> On Mon, 12 Feb 2007 18:11:22 +0100, Andr Thieme
> <······························@justmail.de> wrote:
>
>>Daniel al-Autistiqui schrieb:
[...]
>>> I understand what this is, but does anyone else? Help, please!
What kind of a question is that?
>>What part of it don't you understand?
[...]
> Well, for one thing, _GEB_ has in chapter VIII a more complex system
> called "Typographical Number Theory" (with all its numerals,
> variables, terms, etc.) How would that be rendered in LISP?
WTF?
[...]
> --
> Daniel Gerard McGrath, a/k/a "Govende":
> for e-mail replace "invalid" with "com"
>
> Developmentally disabled;
Pseudonym "Daniel al-Autistiqui" and then this:
> has Autism (Pervasive Developmental Disorder),
> Obsessive-Compulsive Disorder,
> & periodic bouts of depression.
> [This signature is under construction.]
So much nonsense in two postings. I'm gonna go out on a limb here and
call you a troll. But what are killfiles for?
--
Wolfram Fenske
A: Yes.
>Q: Are you sure?
>>A: Because it reverses the logical flow of conversation.
>>>Q: Why is top posting frowned upon?
Wolfram Fenske wrote:
> Daniel al-Autistiqui <·········@hotmail.invalid> writes:
>
>
>>On Mon, 12 Feb 2007 18:11:22 +0100, Andr Thieme
>><······························@justmail.de> wrote:
>>
>>
>>>Daniel al-Autistiqui schrieb:
>
>
> [...]
>
>
>>>>I understand what this is, but does anyone else? Help, please!
>
>
> What kind of a question is that?
>
>
>>>What part of it don't you understand?
>
>
> [...]
>
>
>>Well, for one thing, _GEB_ has in chapter VIII a more complex system
>>called "Typographical Number Theory" (with all its numerals,
>>variables, terms, etc.) How would that be rendered in LISP?
>
>
> WTF?
>
> [...]
>
>
>>--
>>Daniel Gerard McGrath, a/k/a "Govende":
>>for e-mail replace "invalid" with "com"
>>
>>Developmentally disabled;
>
>
> Pseudonym "Daniel al-Autistiqui" and then this:
>
>
>>has Autism (Pervasive Developmental Disorder),
>> Obsessive-Compulsive Disorder,
>> & periodic bouts of depression.
>>[This signature is under construction.]
>
>
> So much nonsense in two postings. I'm gonna go out on a limb here and
> call you a troll. But what are killfiles for?
And what is Google for?
http://alt-usage-english.org/McGrath.html
hth,kxo
--
Well, I've wrestled with reality for 35 years, Doctor, and
I'm happy to state I finally won out over it.
-- Elwood P. Dowd
In this world, you must be oh so smart or oh so pleasant.
-- Elwood's Mom
Ken Tilton <·········@gmail.com> writes:
> Wolfram Fenske wrote:
>> Daniel al-Autistiqui <·········@hotmail.invalid> writes:
>>
>>>On Mon, 12 Feb 2007 18:11:22 +0100, Andr Thieme
>>><······························@justmail.de> wrote:
[...]
>> So much nonsense in two postings. I'm gonna go out on a limb here
>> and call you a troll. But what are killfiles for?
>
> And what is Google for?
>
> http://alt-usage-english.org/McGrath.html
Alright, I take it back.
--
Wolfram Fenske
A: Yes.
>Q: Are you sure?
>>A: Because it reverses the logical flow of conversation.
>>>Q: Why is top posting frowned upon?
Daniel al-Autistiqui schrieb:
> Well, for one thing, _GEB_ has in chapter VIII a more complex system
> called "Typographical Number Theory" (with all its numerals,
> variables, terms, etc.) How would that be rendered in LISP?
Depends, there are several ways.
To gain more understanding it would help if you invested some time to
study mathematical logic to some degree.
This logic primer is very good: http://logic.tamu.edu/Primer/
Andr�
--
On Mon, 12 Feb 2007 20:04:16 -0800, S. Robert James wrote:
> Please post the complete code, including (defun remember-rule
>
Please post beneath what you are replying to and trim irrelevant portions.
--
My address happens to be com (dot) gmail (at) usenet (plus) chbarts,
wardsback and translated.
It's in my header if you need a spoiler.
Daniel al-Autistiqui <·········@hotmail.invalid> writes:
> ;;; Rules begin here.
> (setf *rules* 'empty-stream)
>
> (remember-rule '(i
> ((? x) india)
> ((? x) india uniform)))
>
> (remember-rule '(ii
> (mike (? x))
> (mike (? x) (? x))))
>
> (remember-rule '(iii
> ((? l) india india india (? r))
> ((? l) uniform (? r))))
>
> (remember-rule '(iv
> ((? l) uniform uniform (? r))
> ((? l) (? r))))
>
> ;;; Rules end here.
>
> ;;; Assertions begin here.
> (setf *assertions* 'empty-stream)
>
> (remember-assertion '(mike india))
>
> ;;; Assertions end here.
>
> I understand what this is, but does anyone else? Help, please!
Well, here is the description of the MIU given on this page
http://www.pitt.edu/~jns24/2006/04/hofstadters-miu-system-and-question.html
The MIU-System
- Vocabulary: M, I, U (that's all)
- Formation Rules: the only restriction on what constitutes a
well-formed formula (wff) is that, in order to be a wff, a string
must consist solely of combinations of the above vocabulary.
- Transformation Rules:
(1) If you possess a string whose last letter is I, you may derive
a new string that is the same with the addition of a U on the end
(deriving MIU from MI).
(2) If you have Mx (where x is a variable standing in for any wff
of the system), then you may derive Mxx (e.g., deriving MUMUM from
MUM).
(3) If III occurs in one of the strings, then you may derive a new
string with a U in place of III (e.g., deriving MU from MIII).
(4) If UU occurs in on of the strings, then you may derive a new
string dropping the UU (e.g., deriving MUIII from MUUUIII).
So, I see some problems with your formalization. You're using roman
numerals to number the rules. This is confusing, since i and i are
two different things: i is 1 in roman, and i is the symbol i in the
MIU formal system. Another problem is that the formal system speaks of
M, I and U, not of MIKE, INDIA, and UNIFORM. Lisp is a symbolic
programming language, not an encrypted programming language: we can
use directly the symbols we have in the problem statement.
So here is how I would write it:
(DEFSYSTEM MIU
(R1 ((? X) I) ((? X) I I))
(R2 (M (? X)) (M (? X) (? X)))
(R3 ((? L) I I I (? R)) ((? L) U (? R)))
(R4 ((? L) U U (? R)) ((? L) (? R))))
Now, this is just a transcription of the formal system description.
It doesn't do anything in itself.
In Lisp, you can write a DEFSYSTEM macro that will expand to whatever
you want. For example, you could generate a function that would take
a WFF (Well Formed Formula) and generate all the WFF that can be
deduced by the application of one rule step.
So you could start from the WFF MI, and apply recursively this
function until you find MU. This could take a long time, since the
closure of that function is infinite for most of the WFF, including
those who start with M. But doing a breadth-first search you can
write a function that will finish if there is such a reduction that
holds in the memory of your computer (and theorically loops infinitely
if not, or just breaks when the memory fills).
Here, I will represent the WFF as strings of letters #\M #\I or #\U
(one could as well use lists of symbols M I or U).
(defun nsubseq (sequence start &optional (end nil))
"Like subseq, but for vectors builds a displaced array instead
of copying the data."
(if (vectorp sequence)
(if (and (zerop start) (or (null end) (= end (length sequence))))
sequence
(make-array (- (if end
(min end (length sequence))
(length sequence))
start)
:element-type (array-element-type sequence)
:displaced-to sequence
:displaced-index-offset start))
(subseq sequence start end)))
(defun normalize-pattern (pattern)
"((? x) y) --> (X "Y")"
(let ((pattern (coerce pattern 'vector)))
(loop
:with i = 0
:with result = '()
:while (< i (length pattern))
:do (push (if (and (listp (aref pattern i))
(eq '? (first (aref pattern i))))
(prog1 (second (aref pattern i))
(incf i))
(with-output-to-string (*standard-output*)
(loop
:until (or (<= (length pattern) i)
(and (listp (aref pattern i))
(eq '? (first (aref pattern i)))))
:do (princ (aref pattern i)) (incf i))))
result)
:finally (return (nreverse result)))))
(defun make-pattern-matcher-expression (pattern
target-name index-name bindings-name)
"Builds an expression to bind the PATTERN, with
TARGET-NAME being the name of the string holding the formula,
INDEX-NAME being the name of the variable bound to the start index, and
BINDINGS-NAME being the name of the variable bound to a binding list.
BUG: Doesn't handle (... (? x) ... (? x) ...) in the PATTERN."
(cond
((null pattern)
`(when (= (length ,target-name) ,index-name)
(list ,bindings-name)))
((and (symbolp (first pattern))
(null (rest pattern)))
`(let ((,bindings-name (acons (quote ,(first pattern))
(nsubseq ,target-name ,index-name)
,bindings-name))
(,index-name (length ,target-name)))
,(make-pattern-matcher-expression (rest pattern)
target-name index-name bindings-name)))
((and (symbolp (first pattern))
(symbolp (second pattern)))
`(loop
:for end :from ,index-name :to (length ,target-name)
:nconc (let ((,bindings-name
(acons (quote ,(first pattern))
(nsubseq ,target-name ,index-name end)
,bindings-name))
(,index-name end))
,(make-pattern-matcher-expression
(rest pattern) target-name index-name bindings-name))))
((symbolp (first pattern))
(assert (stringp (second pattern)))
`(loop
:for end = (search ,(second pattern) ,target-name :start2 ,index-name)
:then (search ,(second pattern) ,target-name :start2 (1+ end))
:while end
:nconc (let ((,bindings-name
(acons (quote ,(first pattern))
(nsubseq ,target-name ,index-name end)
,bindings-name))
(,index-name (+ end ,(length (second pattern)))))
,(make-pattern-matcher-expression
(cddr pattern) target-name index-name bindings-name))))
((string (first pattern))
`(if (string= ,(first pattern) ,target-name :start2 ,index-name
:end2 (min (length ,target-name)
(+ ,index-name ,(length (first pattern)))))
(let ((,index-name (+ ,index-name ,(length (first pattern)))))
,(make-pattern-matcher-expression
(rest pattern) target-name index-name bindings-name))))
(t (error "Invalid token in pattern: ~S" pattern))))
(defun make-pattern-matcher (pattern)
"RETURN: a function that matches the PATTERN,
this function returns a list of binding lists."
(let ((variables (mapcan (lambda (item)
(when (and (listp item) (eq '? (first item)))
(list (second item))))
pattern))))
(compile nil
`(lambda (wff)
(let ((index 0)
(bindings '()))
,(make-pattern-matcher-expression
pattern 'wff 'index 'bindings)))))
(defun pattern-evaluate (pattern bindings)
(with-output-to-string (*standard-output*)
(loop
:for item :in pattern
:do (princ (if (symbolp item)
(cdr (or (assoc item bindings)
(error "Regexp group named ~S is not bound"
item)))
item)))))
(defmacro defsystem (name &rest rules)
`(defun ,name (wff)
(delete-duplicates
(append
,@(mapcar
(lambda (rule)
(let ((matcher (make-pattern-matcher
(normalize-pattern (second rule))))
(consequent (normalize-pattern (third rule))))
`(mapcar
(lambda (bindings) (pattern-evaluate ',consequent bindings))
(funcall ,matcher wff))))
rules))
:test (function string=))))
(DEFSYSTEM MIU
(R1 ((? X) I) ((? X) I I))
(R2 (M (? X)) (M (? X) (? X)))
(R3 ((? L) I I I (? R)) ((? L) U (? R)))
(R4 ((? L) U U (? R)) ((? L) (? R))))
(loop
:for closure = (list "MI") :then (mapcan (function miu) closure)
:do (print closure)
:until (member "MU" closure :test (function string=))
:finally (return 'success))
("MI")
("MII")
("MIII" "MIIII")
("MIIII" "MIIIIII" "MU" "MIIIII" "MIIIIIIII" "MUI" "MIU")
--> SUCCESS
Of course, you can write a better function in DEFSYSTEM, for example
to trace what rules were applied in the reduction to MU.
For example, with:
(defmacro defsystem (name &rest rules)
`(defun ,name (wff)
(append
,@(mapcar
(lambda (rule)
(let ((matcher (make-pattern-matcher
(normalize-pattern (second rule))))
(consequent (normalize-pattern (third rule))))
`(mapcar
(lambda (bindings)
(cons ',(first rule)
(pattern-evaluate ',consequent bindings)))
(funcall ,matcher wff))))
rules))))
;; You need to evaluate the DEFSYSTEM form again when you modify the macro:
(DEFSYSTEM MIU
(R1 ((? X) I) ((? X) I I))
(R2 (M (? X)) (M (? X) (? X)))
(R3 ((? L) I I I (? R)) ((? L) U (? R)))
(R4 ((? L) U U (? R)) ((? L) (? R))))
We can see that we can deduce MII from MI two different ways:
(miu "MI") --> ((R1 . "MII") (R2 . "MII"))
So you can write:
(defun prove (axiom target)
(loop
:for closure = (list (cons nil axiom))
:then (mapcan (lambda (item)
(mapcar (lambda (deduction)
(cons (cons (car deduction) (car item))
(cdr deduction)))
(miu (cdr item))))
closure)
:for found = (member target closure :test (function string=)
:key (function cdr))
:until found
:finally (return (reverse (car (first found))))))
(prove "MI" "MU") --> (R1 R1 R3)
You could read some book such as AIMA or PAIP, they cover a number of
algorithms to do such automatic proof, including algorithms such as
forward-chaining, back-chaining, etc.
PAIP = Paradigms of Artificial Intelligence Programming:
Case Studies in Common Lisp
AIMA = Artificial Intelligence: A Modern Approach
http://aima.cs.berkeley.edu
--
__Pascal Bourguignon__ http://www.informatimago.com/
NEW GRAND UNIFIED THEORY DISCLAIMER: The manufacturer may
technically be entitled to claim that this product is
ten-dimensional. However, the consumer is reminded that this
confers no legal rights above and beyond those applicable to
three-dimensional objects, since the seven new dimensions are
"rolled up" into such a small "area" that they cannot be
detected.
Pascal Bourguignon <···@informatimago.com> writes:
> Daniel al-Autistiqui <·········@hotmail.invalid> writes:
>
>> ;;; Rules begin here.
>> (setf *rules* 'empty-stream)
>>
>> (remember-rule '(i
>> ((? x) india)
>> ((? x) india uniform)))
> [...]
> Well, here is the description of the MIU given on this page
> http://www.pitt.edu/~jns24/2006/04/hofstadters-miu-system-and-question.html
> [...]
> So here is how I would write it:
>
> (DEFSYSTEM MIU
> (R1 ((? X) I) ((? X) I I))
> (R2 (M (? X)) (M (? X) (? X)))
> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
> (R4 ((? L) U U (? R)) ((? L) (? R))))
Sorry, it should be:
(DEFSYSTEM MIU
(R1 ((? X) I) ((? X) I U)) ;; <-- U not I...
(R2 (M (? X)) (M (? X) (? X)))
(R3 ((? L) I I I (? R)) ((? L) U (? R)))
(R4 ((? L) U U (? R)) ((? L) (? R))))
(prove "MI" "MUII") --> (R2 R2 R2 R1 R3 R3 R4)
> (prove "MI" "MU") --> (R1 R1 R3)
As http://planetmath.org/encyclopedia/HofstadtersMIUSystem.html
indicates, (prove "MI" "MU") will not terminate, since MU is not a
theorem deducible form the axiom MI in the MIU formal system.
Now to prove it automatically, you'd need to implement more
sophisticated techniques (described in AIMA and PAIP too), and you'd
need to formalize not only the MIU formal system, but also normal
logic and number theory, etc.
--
__Pascal Bourguignon__ http://www.informatimago.com/
The rule for today:
Touch my tail, I shred your hand.
New rule tomorrow.
On 2007-02-14, Pascal Bourguignon <···@informatimago.com> wrote:
>
>
> Pascal Bourguignon <···@informatimago.com> writes:
>
>> Daniel al-Autistiqui <·········@hotmail.invalid> writes:
>>
>>> ;;; Rules begin here.
>>> (setf *rules* 'empty-stream)
>>>
>>> (remember-rule '(i
>>> ((? x) india)
>>> ((? x) india uniform)))
>> [...]
>> Well, here is the description of the MIU given on this page
>> http://www.pitt.edu/~jns24/2006/04/hofstadters-miu-system-and-question.html
>> [...]
>> So here is how I would write it:
>>
>> (DEFSYSTEM MIU
>> (R1 ((? X) I) ((? X) I I))
>> (R2 (M (? X)) (M (? X) (? X)))
>> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
>> (R4 ((? L) U U (? R)) ((? L) (? R))))
>
> Sorry, it should be:
>
> (DEFSYSTEM MIU
> (R1 ((? X) I) ((? X) I U)) ;; <-- U not I...
> (R2 (M (? X)) (M (? X) (? X)))
> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
> (R4 ((? L) U U (? R)) ((? L) (? R))))
>
> (prove "MI" "MUII") --> (R2 R2 R2 R1 R3 R3 R4)
>
When R3 or R4 is used, there may be more than one way to use it;
(prove "MIIII" "MIU") and (prove "MIIII" "MUI") can both return (R3).
Is there a way to change prove so it returns unambiguous derivations?
Mark Tilford <·············@gmail.com> writes:
> On 2007-02-14, Pascal Bourguignon <···@informatimago.com> wrote:
>>
>>
>> Pascal Bourguignon <···@informatimago.com> writes:
>>
>>> Daniel al-Autistiqui <·········@hotmail.invalid> writes:
>>>
>>>> ;;; Rules begin here.
>>>> (setf *rules* 'empty-stream)
>>>>
>>>> (remember-rule '(i
>>>> ((? x) india)
>>>> ((? x) india uniform)))
>>> [...]
>>> Well, here is the description of the MIU given on this page
>>> http://www.pitt.edu/~jns24/2006/04/hofstadters-miu-system-and-question.html
>>> [...]
>>> So here is how I would write it:
>>>
>>> (DEFSYSTEM MIU
>>> (R1 ((? X) I) ((? X) I I))
>>> (R2 (M (? X)) (M (? X) (? X)))
>>> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
>>> (R4 ((? L) U U (? R)) ((? L) (? R))))
>>
>> Sorry, it should be:
>>
>> (DEFSYSTEM MIU
>> (R1 ((? X) I) ((? X) I U)) ;; <-- U not I...
>> (R2 (M (? X)) (M (? X) (? X)))
>> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
>> (R4 ((? L) U U (? R)) ((? L) (? R))))
>>
>> (prove "MI" "MUII") --> (R2 R2 R2 R1 R3 R3 R4)
>>
>
> When R3 or R4 is used, there may be more than one way to use it;
> (prove "MIIII" "MIU") and (prove "MIIII" "MUI") can both return (R3).
> Is there a way to change prove so it returns unambiguous derivations?
Short answer, yes, of course, there is.
I'm sorry I don't have time for the long answer right now.
I'll hope to be able to give it in a few weeks.
--
__Pascal Bourguignon__ http://www.informatimago.com/
Un chat errant
se soulage
dans le jardin d'hiver
Shiki
On Wed, 14 Feb 2007 01:34:07 +0100, Pascal Bourguignon
<···@informatimago.com> wrote:
>Daniel al-Autistiqui <·········@hotmail.invalid> writes:
>
>> ;;; Rules begin here.
>> (setf *rules* 'empty-stream)
>>
>> (remember-rule '(i
>> ((? x) india)
>> ((? x) india uniform)))
>>
>> (remember-rule '(ii
>> (mike (? x))
>> (mike (? x) (? x))))
>>
>> (remember-rule '(iii
>> ((? l) india india india (? r))
>> ((? l) uniform (? r))))
>>
>> (remember-rule '(iv
>> ((? l) uniform uniform (? r))
>> ((? l) (? r))))
>>
>> ;;; Rules end here.
>>
>> ;;; Assertions begin here.
>> (setf *assertions* 'empty-stream)
>>
>> (remember-assertion '(mike india))
>>
>> ;;; Assertions end here.
>>
>> I understand what this is, but does anyone else? Help, please!
>
>Well, here is the description of the MIU given on this page
>http://www.pitt.edu/~jns24/2006/04/hofstadters-miu-system-and-question.html
>
>
>The MIU-System
>
>- Vocabulary: M, I, U (that's all)
>
>- Formation Rules: the only restriction on what constitutes a
> well-formed formula (wff) is that, in order to be a wff, a string
> must consist solely of combinations of the above vocabulary.
>
>- Transformation Rules:
>
> (1) If you possess a string whose last letter is I, you may derive
> a new string that is the same with the addition of a U on the end
> (deriving MIU from MI).
>
> (2) If you have Mx (where x is a variable standing in for any wff
> of the system), then you may derive Mxx (e.g., deriving MUMUM from
> MUM).
>
> (3) If III occurs in one of the strings, then you may derive a new
> string with a U in place of III (e.g., deriving MU from MIII).
>
> (4) If UU occurs in on of the strings, then you may derive a new
> string dropping the UU (e.g., deriving MUIII from MUUUIII).
>
>
>So, I see some problems with your formalization. You're using roman
>numerals to number the rules. This is confusing, since i and i are
>two different things: i is 1 in roman, and i is the symbol i in the
>MIU formal system. Another problem is that the formal system speaks of
>M, I and U, not of MIKE, INDIA, and UNIFORM. Lisp is a symbolic
>programming language, not an encrypted programming language: we can
>use directly the symbols we have in the problem statement.
>
>
>So here is how I would write it:
>
>(DEFSYSTEM MIU
> (R1 ((? X) I) ((? X) I I))
> (R2 (M (? X)) (M (? X) (? X)))
> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
> (R4 ((? L) U U (? R)) ((? L) (? R))))
>
>
>Now, this is just a transcription of the formal system description.
>It doesn't do anything in itself.
>
>In Lisp, you can write a DEFSYSTEM macro that will expand to whatever
>you want. For example, you could generate a function that would take
>a WFF (Well Formed Formula) and generate all the WFF that can be
>deduced by the application of one rule step.
>
>So you could start from the WFF MI, and apply recursively this
>function until you find MU. This could take a long time, since the
>closure of that function is infinite for most of the WFF, including
>those who start with M. But doing a breadth-first search you can
>write a function that will finish if there is such a reduction that
>holds in the memory of your computer (and theorically loops infinitely
>if not, or just breaks when the memory fills).
>
>Here, I will represent the WFF as strings of letters #\M #\I or #\U
>(one could as well use lists of symbols M I or U).
>
>
>
>(defun nsubseq (sequence start &optional (end nil))
> "Like subseq, but for vectors builds a displaced array instead
>of copying the data."
> (if (vectorp sequence)
> (if (and (zerop start) (or (null end) (= end (length sequence))))
> sequence
> (make-array (- (if end
> (min end (length sequence))
> (length sequence))
> start)
> :element-type (array-element-type sequence)
> :displaced-to sequence
> :displaced-index-offset start))
> (subseq sequence start end)))
>
>
>(defun normalize-pattern (pattern)
> "((? x) y) --> (X "Y")"
> (let ((pattern (coerce pattern 'vector)))
> (loop
> :with i = 0
> :with result = '()
> :while (< i (length pattern))
> :do (push (if (and (listp (aref pattern i))
> (eq '? (first (aref pattern i))))
> (prog1 (second (aref pattern i))
> (incf i))
> (with-output-to-string (*standard-output*)
> (loop
> :until (or (<= (length pattern) i)
> (and (listp (aref pattern i))
> (eq '? (first (aref pattern i)))))
> :do (princ (aref pattern i)) (incf i))))
> result)
> :finally (return (nreverse result)))))
>
>
>(defun make-pattern-matcher-expression (pattern
> target-name index-name bindings-name)
> "Builds an expression to bind the PATTERN, with
>TARGET-NAME being the name of the string holding the formula,
>INDEX-NAME being the name of the variable bound to the start index, and
>BINDINGS-NAME being the name of the variable bound to a binding list.
>
>BUG: Doesn't handle (... (? x) ... (? x) ...) in the PATTERN."
> (cond
> ((null pattern)
> `(when (= (length ,target-name) ,index-name)
> (list ,bindings-name)))
> ((and (symbolp (first pattern))
> (null (rest pattern)))
> `(let ((,bindings-name (acons (quote ,(first pattern))
> (nsubseq ,target-name ,index-name)
> ,bindings-name))
> (,index-name (length ,target-name)))
> ,(make-pattern-matcher-expression (rest pattern)
> target-name index-name bindings-name)))
> ((and (symbolp (first pattern))
> (symbolp (second pattern)))
> `(loop
> :for end :from ,index-name :to (length ,target-name)
> :nconc (let ((,bindings-name
> (acons (quote ,(first pattern))
> (nsubseq ,target-name ,index-name end)
> ,bindings-name))
> (,index-name end))
> ,(make-pattern-matcher-expression
> (rest pattern) target-name index-name bindings-name))))
> ((symbolp (first pattern))
> (assert (stringp (second pattern)))
> `(loop
> :for end = (search ,(second pattern) ,target-name :start2 ,index-name)
> :then (search ,(second pattern) ,target-name :start2 (1+ end))
> :while end
> :nconc (let ((,bindings-name
> (acons (quote ,(first pattern))
> (nsubseq ,target-name ,index-name end)
> ,bindings-name))
> (,index-name (+ end ,(length (second pattern)))))
> ,(make-pattern-matcher-expression
> (cddr pattern) target-name index-name bindings-name))))
> ((string (first pattern))
> `(if (string= ,(first pattern) ,target-name :start2 ,index-name
> :end2 (min (length ,target-name)
> (+ ,index-name ,(length (first pattern)))))
> (let ((,index-name (+ ,index-name ,(length (first pattern)))))
> ,(make-pattern-matcher-expression
> (rest pattern) target-name index-name bindings-name))))
> (t (error "Invalid token in pattern: ~S" pattern))))
>
>
>(defun make-pattern-matcher (pattern)
> "RETURN: a function that matches the PATTERN,
> this function returns a list of binding lists."
> (let ((variables (mapcan (lambda (item)
> (when (and (listp item) (eq '? (first item)))
> (list (second item))))
> pattern))))
> (compile nil
> `(lambda (wff)
> (let ((index 0)
> (bindings '()))
> ,(make-pattern-matcher-expression
> pattern 'wff 'index 'bindings)))))
>
>
>(defun pattern-evaluate (pattern bindings)
> (with-output-to-string (*standard-output*)
> (loop
> :for item :in pattern
> :do (princ (if (symbolp item)
> (cdr (or (assoc item bindings)
> (error "Regexp group named ~S is not bound"
> item)))
> item)))))
>
>
>(defmacro defsystem (name &rest rules)
> `(defun ,name (wff)
> (delete-duplicates
> (append
> ,@(mapcar
> (lambda (rule)
> (let ((matcher (make-pattern-matcher
> (normalize-pattern (second rule))))
> (consequent (normalize-pattern (third rule))))
> `(mapcar
> (lambda (bindings) (pattern-evaluate ',consequent bindings))
> (funcall ,matcher wff))))
> rules))
> :test (function string=))))
>
>
>(DEFSYSTEM MIU
> (R1 ((? X) I) ((? X) I I))
> (R2 (M (? X)) (M (? X) (? X)))
> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
> (R4 ((? L) U U (? R)) ((? L) (? R))))
>
>
>(loop
> :for closure = (list "MI") :then (mapcan (function miu) closure)
> :do (print closure)
> :until (member "MU" closure :test (function string=))
> :finally (return 'success))
>
>("MI")
>("MII")
>("MIII" "MIIII")
>("MIIII" "MIIIIII" "MU" "MIIIII" "MIIIIIIII" "MUI" "MIU")
>
>--> SUCCESS
>
>
>Of course, you can write a better function in DEFSYSTEM, for example
>to trace what rules were applied in the reduction to MU.
>
>For example, with:
>
>(defmacro defsystem (name &rest rules)
> `(defun ,name (wff)
> (append
> ,@(mapcar
> (lambda (rule)
> (let ((matcher (make-pattern-matcher
> (normalize-pattern (second rule))))
> (consequent (normalize-pattern (third rule))))
> `(mapcar
> (lambda (bindings)
> (cons ',(first rule)
> (pattern-evaluate ',consequent bindings)))
> (funcall ,matcher wff))))
> rules))))
>
>;; You need to evaluate the DEFSYSTEM form again when you modify the macro:
>
>(DEFSYSTEM MIU
> (R1 ((? X) I) ((? X) I I))
> (R2 (M (? X)) (M (? X) (? X)))
> (R3 ((? L) I I I (? R)) ((? L) U (? R)))
> (R4 ((? L) U U (? R)) ((? L) (? R))))
>
>
>We can see that we can deduce MII from MI two different ways:
>
>(miu "MI") --> ((R1 . "MII") (R2 . "MII"))
>
>So you can write:
>
>(defun prove (axiom target)
> (loop
> :for closure = (list (cons nil axiom))
> :then (mapcan (lambda (item)
> (mapcar (lambda (deduction)
> (cons (cons (car deduction) (car item))
> (cdr deduction)))
> (miu (cdr item))))
> closure)
> :for found = (member target closure :test (function string=)
> :key (function cdr))
> :until found
> :finally (return (reverse (car (first found))))))
>
>(prove "MI" "MU") --> (R1 R1 R3)
>
>
>You could read some book such as AIMA or PAIP, they cover a number of
>algorithms to do such automatic proof, including algorithms such as
>forward-chaining, back-chaining, etc.
>
>PAIP = Paradigms of Artificial Intelligence Programming:
> Case Studies in Common Lisp
>
>AIMA = Artificial Intelligence: A Modern Approach
> http://aima.cs.berkeley.edu
I'll try to study this over my 3-day weekend. Thanks.
daniel mcgrath
--
Daniel Gerard McGrath, a/k/a "Govende":
for e-mail replace "invalid" with "com"
Developmentally disabled;
has Autism (Pervasive Developmental Disorder),
Obsessive-Compulsive Disorder,
& periodic bouts of depression.
[This signature is under construction.]