Ok, So you're taking a class in Propositional Logic / Sentential
Calculus. Maybe because you're interested in it, maybe because it's a
requirement of your major, or maybe because it's a detail of your
parole...
One dark Friday your professor walks in with a stack of symbolized
transcripts from the OJ Simpson trial and says "determine the validity
of all the symbolized arguments used by the defense by Monday".
Shoot! It looks like this weekend's debacherous sojurn to Vegas is off.
Better call up the girls and tell them you won't be gallavanting with
them around the strip with them because instead you'll be hunched over
your desk madly sketching truth trees and tables for the entire
weekend, right?
Wrong! You're know Lisp and writing a program to do your homework for
you should be a snap.
Being a Lisp hacker, you know the first step is to build the language
up to suit your new problem. What are the basic axioms of logic you'll
need? Conjunction, disjunction, not/negation, material equivalence, and
material implication...
hm... If you use Common Lisps T and NIL, then your can probubly make
use of a few of CL's built in operators:
Conjunction - AND
Disjunction - OR
Not - NOT
Material equivalence - EQL
Material implication - ????
But what about material implication?
Extend the language already!
(defun then (1st 2nd)
(or 2nd (not 1st)))
Now (then t t) evaluates to T:
(then t t)
=>
T
(then nil nil)
=>
T
(then nil t)
=>
T
(then t nil)
=>
NILL
Now you've got a rudimentary little system for determining the truth
value of a form:
(and (or t nil) (then nil t))
=>
T
But you're not exactly going to get to Sin City this weekend by typing
T and NIL for every possible truth value of every possible
propositional variable, are you?
Since code is data in Lisp, it's trivial for you to write code that
writes code (with macros).
(defmacro with-prop-vars (varlist &body body)
(if varlist
`(dolist (,(first varlist) '(t nil))
(with-prop-vars ,(rest varlist) ,@body))
`(progn ,@body)))
The form
(with-prop-vars (a b c)
(print (list a b c)))
now expands to
(dolist (a '(t nil))
(dolist (b '(t nil))
(dolist (c '(t nil))
(print (list a b c)))))
and (PRINT (LIST A B C)) is executed for every possible true/false
combination of A, B, and C. Thus
(with-prop-vars (a b c)
(print (list a b c)))
=>
"(T T T)"
"(T T NIL)"
"(T NIL T)"
"(T NIL NIL)"
"(NIL T T)"
"(NIL T NIL)"
"(NIL NIL T)"
"(NIL NIL NIL)"
NIL
Now, that's all well and good, but you can't be bothered to type in
(with-prop-vars...) with every argument! You just want to type in a
form, get back the necessary information, and go to Vegas. What's with
all this typing?
Luckily this is Lisp, the lazy person's language. You write a function
PROP-VARS-IN to pull all the variables out of a form:
(defun prop-vars-in (form)
(let (varlist)
(labels ((rfn (xx)
(etypecase xx
(symbol (pushnew xx varlist))
(list (mapc #'rfn (rest xx))))))
(rfn form)
varlist)))
(prop-vars-in '(and (or a b) (then c a)))
=>
(c b a)
Then hack a quick macro that uses PROP-VARS-IN to do your neferious
bidding without having to type WITH-PROP-VARS
(defmacro tautologyp (prop-form)
(let ((g (gensym)))
`(block ,g
(with-prop-vars ,(prop-vars-in prop-form)
(progn (unless ,prop-form
(return-from ,g nil))
t)
t))))
(tautologyp (or a (not b)))
=>
NIL
(tautologyp (or a (not a)))
=>
T
Now you just have to type in the corresponding conditional of each
argument in Lisp and it will quickly proven valid or not...
What?!?!?! You don't want to have to convert everything to prefix
notation? Don't you understand the beauty and superiority of infix
notation! Are you that lazy?!?!
Well... you're right, you might make a mistake translating it from
infix to prefix syntax yourself.
Thus you define a facility for defining infix functions:
(defvar *infix-fns* nil)
(defmacro def-infix (infix prefix)
`(progn
(push '(,infix ,prefix) *infix-fns*)
',infix))
and a function for looking up which prefix operators the infix
functions are associated with:
(defun prefix (infix)
(second (assoc infix *infix-fns*)))
Now you can define your infix logic language:
(def-infix v or)
(def-infix & and)
(def-infix => then)
(def-infix == eql)
and lookup the prefix function associated with each infix operator
(prefix '&)
=>
AND
The function INFIX->PREFIX takes a form and converts it from infix to
prefix syntax
(defun infix->prefix (infix-form)
(if (atom infix-form)
infix-form
(let ((in infix-form)
out
infix-seen)
(labels ((pop-infix ()
(let* ((xx (pop in))
(p (prefix xx)))
(cond (p (setq infix-seen t)
(list p
(pop out)
(infix->prefix (pop in))))
(t (etypecase xx
(list (infix->prefix xx))
(symbol xx)))))))
(loop (unless in (return))
(push (pop-infix) out))
(if (rest out)
(if infix-seen
out
(reverse out))
(first out))))))
(infix->prefix '(a v (b & (d == c))))
=>
(OR A (AND B (EQL D C)))
But what about NOT/negation?
You know what would be *really* cool? If you could define your own
syntax so that the tilde (~) was a special operator that could be
prepended to anything and would always be interpreted as (NOT
whatever)... yeah that would be real cool... too bad you're restricted
to the sexp syntax... quit dreaming, man...
Wait! What the hell are you whining about? This is Lisp! Even the
syntax is extendible! Quit whining!
Simply define a function:
(defun tilde-reader (stream char)
(declare (ignore char))
`(not ,(read stream t nil t)))
associate it to the desired character:
(set-macro-character #\~ #'tilde-reader)
Now:
~t
=>
NIL
~NIL
=>
T
Cool! So now using our ~ syntax and the new macro INFIX-TAUTOLOGY-P
determing if a form is a tautology or not is easier than ever!
(defmacro infix-tautology-p (&rest infix-form)
`(tautologyp ,(infix->prefix infix-form)))
(infix-tautology-p (a => b) v (b => ~a))
=>
T
Wait... Crap. Stop the party. Your professor just called to tell you he
also wants truth values of the form to the truth values of the
variables. What to do? You're already knee deep in code and your
problem description changed...
Well, back to the drawing board...
Heck no! You're not going through all that effort again! You're a
functionall programmer, you're code is made up of small independent
pieces held together by functional glue. Simply redefine a small piece
(WITH-PROP-VARS) to provide the new behavior and you'll be on your way:
(defmacro with-prop-vars (varlist &body body)
(labels ((rfn (vl)
(if vl
`(dolist (,(first vl) '(t nil))
,(rfn (rest vl)))
(let ((prints (mapcar #'(lambda (v)
`(format t "~5s" ,v))
varlist)))
`(progn
(progn (fresh-line) ,@prints)
(princ ,@body))))))
`(progn
(format t "~%~{~5s~}~%" ',(append varlist '(form)))
(princ (make-string ,(* 5 (1+ (length varlist))) :initial-element
#\-))
,(rfn varlist))))
now
(infix-tautology-p (a => b) v (b => ~a))
=>
"B A FORM
---------------
T T T
T NIL T
NIL T T
NIL NIL T"
T
...and yet... there's *something* missing.
It's still not EASY enough.
Why should you have to convert each argument to it's corresponding
conditional? Shouldn't it do it itself?
Damn right!
(defvar *infer* :.)
(defmacro validp (&rest argument)
(let ((xx (mapcar #'infix->prefix (remove *infer* argument))))
(setf (first (last xx))
`(not ,(first (last xx))))
`(progn
(print "Remember `FORM' is the *NEGATION* of the conjunction of
all the premises and the negation of the conclusion")
(let ((% (contradictionp (and ,@xx))))
(format t
"~%~%FORM IS ~A~%~%"
(if %
"VALID"
"INVALID"))
%))))
Now you can just type an infix argument into VALIDP:
(validp (a => b)
~b
:.
~a)
=>
"Remember `FORM' is the *NEGATION* of the conjunction of all the
premises and the negation of the conclusion
B A FORM
---------------
T T NIL
T NIL NIL
NIL T NIL
NIL NIL NIL
FORM IS VALID"
T
But...
hrm...
Could it be even EASIER? Why should you have to write VALIDP? Why can't
you just type in arguments into the computer and have the computer tell
you if they're valid and then go to Las Vegas?
Why not?
(defvar *magic-exit-form* :exit)
(defun validator ()
(let (collected
infer-seen)
(loop (unless collected
(format t
"~%Please enter an argument to be validated or ~s to exit~%"
*magic-exit-form*))
(let ((in (read nil nil nil)))
(cond ((eq in *magic-exit-form*) (return-from validator 'thanks))
((eq in *infer*) (setq infer-seen t))
(t (push in collected)
(when infer-seen
(eval (macroexpand `(validp ,@(reverse (remove-if #'stringp
collected)))))
(setq infer-seen nil
collected nil))))))))
;note to self: never ever write code this bad again...
Now you have this program VALIDATOR. It asks you for a form, you type
on in, and tells you if it is valid or not and asks you for another.
(validator)
=>
"Please enter an argument to be validated or :EXIT to exit
(a => b)
(b => c)
(c == ~d)
a
:.
~d
Remember `FORM' is the *NEGATION* of the conjunction of all the
premises and the negation of the conclusion
D C B A FORM
-------------------------
T T T T NIL
T T T NIL NIL
T T NIL T NIL
T T NIL NIL NIL
T NIL T T NIL
T NIL T NIL NIL
T NIL NIL T NIL
T NIL NIL NIL NIL
NIL T T T NIL
NIL T T NIL NIL
NIL T NIL T NIL
NIL T NIL NIL NIL
NIL NIL T T NIL
NIL NIL T NIL NIL
NIL NIL NIL T NIL
NIL NIL NIL NIL NIL
FORM IS VALID
Please enter an argument to be validated or :EXIT to exit
:exit"
THANKS
You'll be in Sin City in no time. Vegas here you come, baby!
You know, it's a good thing that
(a) you go to MIT and you were forced to sit through the (freely
available online) Structure and Interpretation of Computer Programs
lectures:
http://swiss.csail.mit.edu/classes/6.001/abelson-sussman-lectures/
(b) you're just getting into programming and you're reading David
Touretzky's (freely available online) book "A Gentle Introduction into
Symbolic Computation":
http://www.cs.cmu.edu/~dst/LispBook/book.pdf
(c) you already know how to brogram and you've baught a copy of Peter
Seibel's (freely available online) book Practical Common Lisp:
http://www.gigamonkeys.com/book/
(d) you're an experianced programmer and you're graduating to
Functional Programming by reading Paul Graham's (freely available
online) book On Lisp:
http://www.paulgraham.com/onlisp.html
(e) you've never heard of Lisp before and you're just beggining to
explore the plethora of (freely available online) recorces:
http://www.cl-user.net/
good luck
hth
Nick
the code in this post is available more readably at:
http://paste.lisp.org/display/30005
I guess I forgot this function, which is used by VALIDP
(defmacro contradictionp (prop-form)
(let ((g (gensym)))
`(block ,g
(with-prop-vars ,(prop-vars-in prop-form)
(when ,prop-form
(return-from ,g nil)))
t)))
········@gmail.com writes:
> [...]
> Conjunction - AND
> Disjunction - OR
> Not - NOT
> Material equivalence - EQL
Not exactly. EQL tests for identity, not equivalence.
In Lisp, NIL is false, all the rest is true.
(defun equiv (&rest args)
(or (null args)
(loop :for p :in (cdr args) :always (eql (not (car args)) (not p)))))
Mind that AND and OR are short-cutting and return the first or last
non NIL value.
> Material implication - ????
> [...]
> (defun then (1st 2nd)
> (or 2nd (not 1st)))
>
> Now (then t t) evaluates to T:
or (==> a b) or (implies a b)
You can also have fun with unicode:
(defmacro ∧ (&rest args) `(and ,@args))
(defmacro ∨ (&rest args) `(or ,@args))
(defun ⋀ (args) (every (function identity) args))
(defun ⋁ (args) (some (function identity) args))
(defun ¬ (arg) (not arg))
(defun ⇒ (&rest args) (loop :with r = T :for p :in args :while (or r (not p))
:do (setf r (not (not p))) :finally (return r)))
(defun ⇔ (&rest args) (or (null args)
(loop :for p :in (cdr args)
:always (eql (not (car args)) (not p)))))
(defun ⇎ (&rest args) (not (apply (function ⇔) args)))
(def-infix ∧ ∧)
(def-infix ∨ ∨)
(def-infix ⋀ ⋀)
(def-infix ⋁ ⋁)
(def-infix ⇒ ⇒)
(def-infix ⇔ ⇔)
(defun symbol-char-p (ch)
(and (not (member ch '(#\space #\newline
#\tab #\linefeed #\return #\page #\vt)))
(multiple-value-bind (mcp ntp) (get-macro-character ch)
(not (and mcp (not ntp))))))
(defun tilde-reader (stream char)
(declare (ignore char))
(values
(if (symbol-char-p (peek-char nil stream nil nil t))
`(not ,(read stream t nil t))
(intern "¬"))))
(set-macro-character #\¬ (function tilde-reader) t)
'( ¬ a¬b a¬ ¬b ) --> (|¬| A¬B A¬ (NOT B))
(defun prop-vars-in (form)
(delete-duplicates
(cond ((null form) '())
((symbolp form) (list form))
((consp form) (mapcan (function prop-vars-in) (cdr form))))))
You can also take the name of the truth values:
(defmacro with-prop-vars (varlist &optional truth-values-or-first-form &body body)
(let* ((truth-values (if (and (consp truth-values-or-first-form)
(= 2 (length truth-values-or-first-form))
(every (function stringp) truth-values-or-first-form))
truth-values-or-first-form
'("F" "T")))
(body (if (and (consp truth-values-or-first-form)
(= 2 (length truth-values-or-first-form))
(every (function stringp) truth-values-or-first-form))
body
(cons truth-values-or-first-form body)))
(width (1+ (max (reduce (function max)
(mapcar (lambda (x) (length (string x))) varlist))
(reduce (function max)
(mapcar (function length) truth-values)))))
(boolformat (format nil "~~:[~VA~~;~VA~~]"
width (first truth-values)
width (second truth-values))))
(labels ((rfn (vl)
(if vl
`(dolist (,(first vl) '(t nil))
,(rfn (rest vl)))
(let ((prints (mapcar #'(lambda (v)
`(format t ,boolformat ,v))
varlist)))
`(progn
(progn (fresh-line) ,@prints)
(format t ,boolformat ,@body))))))
`(progn
(format t ,(format nil "~~%~~{~~~AA~~}~~%" width) ',(append varlist '(form)))
(princ (make-string ,(* width (1+ (length varlist))) :initial-element #\-))
,(rfn varlist)))))
[398]> (with-prop-vars (a b) ("Faux" "Vrai") (and a b))
A B FORM
---------------
Vrai Vrai Vrai
Vrai Faux Faux
Faux Vrai Faux
Faux Faux Faux
NIL
[399]> (with-prop-vars (a b) ("0" "1") (and a b))
A B FORM
------
1 1 1
1 0 0
0 1 0
0 0 0
NIL
(defconstant +magic-exit-form+ :exit) ; constants can be symbols.
(defun validator ()
(let (collected
infer-seen)
(loop (unless collected
(format t
"~%Please enter an argument to be validated or ~s to exit~%"
+magic-exit-form+))
(let ((in (read nil nil nil)))
(cond ((eq in +magic-exit-form+) (return-from validator 'thanks))
((eq in *infer*) (setq infer-seen t))
(t (push in collected)
(when infer-seen
(eval `(validp ,@(reverse (remove-if #'stringp collected))))
(setq infer-seen nil
collected nil))))))))
[396]> (validator)
Please enter an argument to be validated or :EXIT to exit
(a ⇒ b)
(b ⇒ c)
a
:.
c
"Remember `FORM' is the *NEGATION* of the conjunction of all the premises and the negation of the conclusion"
B A C FORM
--------
T T T F
T T F F
T F T F
T F F F
F T T F
F T F F
F F T F
F F F F
FORM IS VALID
Please enter an argument to be validated or :EXIT to exit
((a1 ∨ a2) ⇒ b)
(b ⇒ c)
(c ⇔ ¬d)
(a ⇔ (a1 ∨ a2))
a
:.
¬d
"Remember `FORM' is the *NEGATION* of the conjunction of all the premises and the negation of the conclusion"
B C A1 A2 A D FORM
---------------------
T T T T T T F
T T T T T F F
T T T T F T F
T T T T F F F
T T T F T T F
T T T F T F F
T T T F F T F
T T T F F F F
T T F T T T F
T T F T T F F
T T F T F T F
T T F T F F F
T T F F T T F
T T F F T F F
T T F F F T F
T T F F F F F
T F T T T T F
T F T T T F F
T F T T F T F
T F T T F F F
T F T F T T F
T F T F T F F
T F T F F T F
T F T F F F F
T F F T T T F
T F F T T F F
T F F T F T F
T F F T F F F
T F F F T T F
T F F F T F F
T F F F F T F
T F F F F F F
F T T T T T F
F T T T T F F
F T T T F T F
F T T T F F F
F T T F T T F
F T T F T F F
F T T F F T F
F T T F F F F
F T F T T T F
F T F T T F F
F T F T F T F
F T F T F F F
F T F F T T F
F T F F T F F
F T F F F T F
F T F F F F F
F F T T T T F
F F T T T F F
F F T T F T F
F F T T F F F
F F T F T T F
F F T F T F F
F F T F F T F
F F T F F F F
F F F T T T F
F F F T T F F
F F F T F T F
F F F T F F F
F F F F T T F
F F F F T F F
F F F F F T F
F F F F F F F
FORM IS VALID
Please enter an argument to be validated or :EXIT to exit
:exit
THANKS
[397]>
--
__Pascal Bourguignon__ http://www.informatimago.com/
Grace personified,
I leap into the window.
I meant to do that.
········@gmail.com wrote:
> Ok, So you're taking a class in Propositional Logic / Sentential
> Calculus. Maybe because you're interested in it, maybe because it's a
> requirement of your major, or maybe because it's a detail of your
> parole...
>
> One dark Friday your professor walks in with a stack of symbolized
> transcripts from the OJ Simpson trial and says "determine the validity
> of all the symbolized arguments used by the defense by Monday".
>
> Shoot! It looks like this weekend's debacherous sojurn to Vegas is off.
> Better call up the girls and tell them you won't be gallavanting with
> them around the strip with them because instead you'll be hunched over
> your desk madly sketching truth trees and tables for the entire
> weekend, right?
>
> Wrong! You're know Lisp and writing a program to do your homework for
> you should be a snap.
>
> Being a Lisp hacker, you know the first step is to build the language
> up to suit your new problem. What are the basic axioms of logic you'll
> need? Conjunction, disjunction, not/negation, material equivalence, and
> material implication...
>
Very good idea, a program that automatically "translates" common
language arguments into "predicate-logic" arguments.
Make your lisp function perform all the common language translations at
these links below and you'll cause a revolution. Microsoft is currently
devoting most of its research to verbally controlling the entire
computer and all changes a keyboard input can cause.
Translation Tips
http://www.earlham.edu/~peters/courses/log/transtip.htm
http://www.nku.edu/~garns/165/ppt6_1.html
http://www.philosophypages.com/lg/e09.htm
1. Fallacy of Four Terms (Quaeternio Terminorum),
2. Fallacy of the Undistributed Middle Term
3. Fallacy of the Illicit Major Term or Fallacy of the Illicit Minor
Term
4. Fallacy of Exclusive Premises ( Two negative premises)
5. Fallacy of Affirming a positive conclusion from a negative premise
6. Fallacy of a Particular conclusion inferred from two Universal
premises ( Existential Fallacy)
http://www.markmcintire.com/chapter6supnotes2.htm
http://tinyurl.com/ufti
> Make your lisp function perform all the common language translations at
> these links below and you'll cause a revolution. Microsoft is currently
> devoting most of its research to verbally controlling the entire
> computer and all changes a keyboard input can cause.
>
> Translation Tips
> http://www.earlham.edu/~peters/courses/log/transtip.htm
> http://www.nku.edu/~garns/165/ppt6_1.html
> http://www.philosophypages.com/lg/e09.htm
Hum. Three years ago I wrote a Qi-YACC program to translate
English into first order logic. Its 350 lines long and I got to the
point of being able to translate some fairly complex sentences.
I moved on after that. Here's a sample.
Mark
(time (logic [the tall man loves the fat girl with the dead duck]))
Real time: 0.015625 sec.
Run time: 0.015625 sec.
Space: 138476 Bytes
[some x
[some x457
[[[[man x] & [tall x]] &
[[[girl x457] &
[some x458 [[[duck x458] & [dead x458]] & [with x457 x458]]]]
& [fat x457]]]
& [love x x457]]]]
Hi
What happens if you say: The fat and slim girl?
Is there an easy way to find out that fat and slim
are refering to the attribute of the girl?
Thus that the sentences is contradictory?
The point I want to put forward is, that working
with language involves not only parsing sentences
from words, i.e. grammatikal knowledge, but also
knowledge about the meaning of the words, i.e.
semantical knowledge.
Nice book: L�bner, S.: Understanding Semantics,
Arnold Publishers, 2002
Bye
Mark Tarver wrote:
>>Make your lisp function perform all the common language translations at
>>these links below and you'll cause a revolution. Microsoft is currently
>>devoting most of its research to verbally controlling the entire
>>computer and all changes a keyboard input can cause.
>>
>>Translation Tips
>>http://www.earlham.edu/~peters/courses/log/transtip.htm
>>http://www.nku.edu/~garns/165/ppt6_1.html
>>http://www.philosophypages.com/lg/e09.htm
>
>
> Hum. Three years ago I wrote a Qi-YACC program to translate
> English into first order logic. Its 350 lines long and I got to the
> point of being able to translate some fairly complex sentences.
> I moved on after that. Here's a sample.
>
> Mark
>
> (time (logic [the tall man loves the fat girl with the dead duck]))
>
> Real time: 0.015625 sec.
> Run time: 0.015625 sec.
> Space: 138476 Bytes
> [some x
> [some x457
> [[[[man x] & [tall x]] &
> [[[girl x457] &
> [some x458 [[[duck x458] & [dead x458]] & [with x457 x458]]]]
> & [fat x457]]]
> & [love x x457]]]]
>
Jan Burse wrote:
> Hi
>
> What happens if you say: The fat and slim girl?
>
(6-) (time (logic [the tall man loves the fat slim girl with the dead
duck]))
Real time: 0.015625 sec.
Run time: 0.015625 sec.
Space: 145804 Bytes
[some x
[some x179
[[[[man x] & [tall x]] &
[[[girl x179] &
[some x180 [[[duck x180] & [dead x180]] & [with x179 x180]]]]
& [[fat x179] & [slim x179]]]]
& [love x x179]]]]
> Is there an easy way to find out that fat and slim
> are refering to the attribute of the girl?
> Thus that the sentences is contradictory?
Your knowledge base would have to contain the assertion
as a semantic rule.
[all x [[slim x] => [~ [fat x]]]]
The inference engine could raise an inconsistency by trying to
derive the negation of the assertion from its database of semantic
rules. Any assertion that could be thus refuted could be said to
be false apriori. Its quite doable.
Mark
oops, omission, it should read:
.. are refering to the SAME attribute of the girl?
Jan Burse wrote:
> Hi
>
> What happens if you say: The fat and slim girl?
>
> Is there an easy way to find out that fat and slim
> are refering to the attribute of the girl?
> Thus that the sentences is contradictory?
>
> The point I want to put forward is, that working
> with language involves not only parsing sentences
> from words, i.e. grammatikal knowledge, but also
> knowledge about the meaning of the words, i.e.
> semantical knowledge.
>
> Nice book: L�bner, S.: Understanding Semantics,
> Arnold Publishers, 2002
>
> Bye
>
> Mark Tarver wrote:
>
>>> Make your lisp function perform all the common language translations at
>>> these links below and you'll cause a revolution. Microsoft is currently
>>> devoting most of its research to verbally controlling the entire
>>> computer and all changes a keyboard input can cause.
>>>
>>> Translation Tips
>>> http://www.earlham.edu/~peters/courses/log/transtip.htm
>>> http://www.nku.edu/~garns/165/ppt6_1.html
>>> http://www.philosophypages.com/lg/e09.htm
>>
>>
>>
>> Hum. Three years ago I wrote a Qi-YACC program to translate
>> English into first order logic. Its 350 lines long and I got to the
>> point of being able to translate some fairly complex sentences.
>> I moved on after that. Here's a sample.
>>
>> Mark
>>
>> (time (logic [the tall man loves the fat girl with the dead duck]))
>>
>> Real time: 0.015625 sec.
>> Run time: 0.015625 sec.
>> Space: 138476 Bytes
>> [some x
>> [some x457
>> [[[[man x] & [tall x]] &
>> [[[girl x457] &
>> [some x458 [[[duck x458] & [dead x458]] & [with x457 x458]]]]
>> & [fat x457]]]
>> & [love x x457]]]]
>>
Hi Jans,
Alternatively you can do it this way - which is very elegant.
The theory of transduction into FOL being used in this Qi program
is based on Aristotle's theory of truth which loosely paraphrased
says "to say of what is that it is or what is not that it is not, is
true."
You can look for the full quote in http://en.wikipedia.org/wiki/Truth.
To put the matter in this idiom, an Aristotelian theory of truth for
natural languages (NLs) says that a sentence is true if the verb
phrase (VP) correctly applies to the subject of the noun phrase
(NP). "Mark is bald" is true just when "bald" is correctly applied
to the denotation of "Mark". Tarski's Semantic Theory of Truth
is really Aristotle brought up to date by being released from the
constraints of Aristotelean logic and applied to FOL.
You can use the same idea to elegantly parse NLs by transducing
the VP into a lambda abstraction and the NP into a term. The
correct translation is then produced by applying the transduction of
the VP to the transduction of the NP - i.e. by beta reduction.
So "Mark is bald" becomes ((/. X [bald X]) Mark) (/. is lambda in Qi)
and this reduces to [bald Mark]. Something like this is going on in
the Qi program I cited.
Now to answer your question about the computer recognising the
absurdity of fat slim girls etc. This does require an inference
engine.
But if you use the approach above, you can actually place the
semantic rules into the transduction rather than into the domain of
the inference engine. This has the advantage of being very
efficient.
How can you do this? OK; lets take "Mark is slim". We transduce to
((/. X (slim X)) Mark)
Notice that we are actually applying a function slim here to Mark.
(In Qi [ ] forms lists and ( ) applies functions). So Qi will say
'Hey! What is this 'slim' function?'. So what we do is define it.
(define slim
Subject -> [~ [fat Subject]])
Here 'fat' is a semantic primitive. But it need not be. We could
define it as another function.
(define slim
Subject -> [~ (fat Subject)])
(define fat
Subject -> [> [bmi Subject] 35])
and so on. Hence your NLP system will automatically place the
transduction into a canonical form using demodulation (rewriting)
in which only your chosen semantic primitives appear. This
forestalls the use of many semantic rules which inevitably pose
computational overheads to the inference engine.
Qi makes this sort of stuff very easy. Its an extremely powerful
system.
OK, I'm supposed to be doing meditation and yoga. But this
came to mind.
bw
Mark
Mark Tarver wrote:
> Hi Jans,
>
> Alternatively you can do it this way - which is very elegant.
>
> The theory of transduction into FOL being used in this Qi program
> is based on Aristotle's theory of truth which loosely paraphrased
> says "to say of what is that it is or what is not that it is not, is
> true."
>
> You can look for the full quote in http://en.wikipedia.org/wiki/Truth.
>
> To put the matter in this idiom, an Aristotelian theory of truth for
> natural languages (NLs) says that a sentence is true if the verb
> phrase (VP) correctly applies to the subject of the noun phrase
> (NP). "Mark is bald" is true just when "bald" is correctly applied
> to the denotation of "Mark". Tarski's Semantic Theory of Truth
> is really Aristotle brought up to date by being released from the
> constraints of Aristotelean logic and applied to FOL.
>
Can you show how your LISP system would work with two other theories of
truth besides Aristotle's theory (1) Coherence theory and (2) The
Coherence Theory of Truth?
(1) Coherence theory: "An empirical belief is realatively true if and
only if it coheres with a system of other beliefs, which together form
a comprehensive account of reality - fact can only mean confirmed to
such a degree that it would be perverse to withhold provisional assent.
Succesfully Competitive Inductive Cogency depends upon the evidential
and conceptual ("context") of reasoning. An inductive argument from
evidence to hypothesis is inductively cogent if and only if the
hypothesis is that hypothesis which, of all the competing hypothesis,
has the greatest probability of being true on the basis of the
evidence. Thus, whether it is reasonable to accept a hypothesis as
true, if the statements of evidence are true, is determined by whether
that hypothesis is the most probable, on the evidence, of all those
with which it competes.
(2) The Coherence Theory of Truth: A coherence theory of truth states
that the truth of any (true) proposition consists in its coherence with
some specified set of propositions.
The Correspondence Theory of Truth: Narrowly speaking, the
correspondence theory of truth is the view that truth is correspondence
to a fact. But the label is usually applied much more broadly to any
view explicitly embracing the idea that truth consists in a relation to
reality, i.e., that truth is a relational property involving a
characteristic relation to some portion of reality.
http://plato.stanford.edu/entries/truth-coherence/
http://plato.stanford.edu/entries/truth-correspondence/
Philosophical Problems and Arguments : An Introduction
by James W. Cornman, Keith Lehrer, George Sotiros Pappas
http://www.amazon.com/exec/obidos/ASIN/0872201244/104-9938841-0500749
The coherence theory differs from the correspondence theory of truth in
two essential respects. The competing theories give conflicting
accounts of the relation between propositions and their truth
conditions.
1. According to one, the relation is coherence
2. According to the other, it is correspondence
The two theories also give conflicting accounts of truth conditions.
According to the coherence theory, the truth conditions of propositions
consist in other propositions. The correspondence theory, in contrast,
states that the truth conditions of propositions are not (in general)
propositions, but rather objective features of the world. (Even the
correspondence theorist holds that propositions about propositions have
propositions as their truth conditions.)
-----------------------------------
> You can use the same idea to elegantly parse NLs by transducing
> the VP into a lambda abstraction and the NP into a term. The
> correct translation is then produced by applying the transduction of
> the VP to the transduction of the NP - i.e. by beta reduction.
>
> So "Mark is bald" becomes ((/. X [bald X]) Mark) (/. is lambda in Qi)
> and this reduces to [bald Mark]. Something like this is going on in
> the Qi program I cited.
>
> Now to answer your question about the computer recognising the
> absurdity of fat slim girls etc. This does require an inference
> engine.
>
> But if you use the approach above, you can actually place the
> semantic rules into the transduction rather than into the domain of
> the inference engine. This has the advantage of being very
> efficient.
>
> How can you do this? OK; lets take "Mark is slim". We transduce to
>
> ((/. X (slim X)) Mark)
>
> Notice that we are actually applying a function slim here to Mark.
> (In Qi [ ] forms lists and ( ) applies functions). So Qi will say
> 'Hey! What is this 'slim' function?'. So what we do is define it.
>
> (define slim
> Subject -> [~ [fat Subject]])
>
> Here 'fat' is a semantic primitive. But it need not be. We could
> define it as another function.
>
> (define slim
> Subject -> [~ (fat Subject)])
>
> (define fat
> Subject -> [> [bmi Subject] 35])
>
> and so on. Hence your NLP system will automatically place the
> transduction into a canonical form using demodulation (rewriting)
> in which only your chosen semantic primitives appear. This
> forestalls the use of many semantic rules which inevitably pose
> computational overheads to the inference engine.
>
> Qi makes this sort of stuff very easy. Its an extremely powerful
> system.
>
> OK, I'm supposed to be doing meditation and yoga. But this
> came to mind.
>
> bw
>
> Mark
Immortalist wrote:
> Can you show how your LISP system would work with two other theories of
> truth besides Aristotle's theory (1) Coherence theory and (2) The
> Coherence Theory of Truth?
Hi,
OK. Fundamentally I use lambda calculus and an Aristolean
theory of truth for natural language semantics - for the actual
process of reducing English sentences to first order logic. Its
powerful and very clean.
You're right in suggesting that correspondence theory is not unique
amongst philosophical approaches to truth. Coherence theory was
adopted by some very eminent thinkers of the Vienna Circle. The
passage in Quine's "Two Dogmas of Empiricism" about the web of
belief is very much coherence-oriented.
I suppose I would begin by drawing a distinction between
(a) what it *means* to say something is true and
(b) how we tell if something is true.
Not everybody accepts this distinction - for example constructivists
deny this distinction exists in maths. But its a useful distinction.
I think coherency theory of truth probably has the most contribution to
(b) - to the process by which we sift conflicting evidence to come up
with what we regard as a satisfactory set of principles. What
Aristotle has to say really contributes to (a).
* Both theories actually have an important part to play in the
computer manipulation of written material.*
Aristotle's ideas can be used to promote the 'understanding' of text.
But coherency theory will be needed to give computers the capacity
to sift vast amounts of intelligence and produce some coherent
believable conclusion. Its a multi-million dollar challenge. The
answer will require a model of coherency in terms of a weighted
network. I won't say more here.
So the answer to your question is that my system (which is Qi, rather
than Lisp) does not use coherency theory because the problem it was
addressing does not require it.
But the seperate problem I've alluded to does.
Mark
Mark Tarver wrote:
> Immortalist wrote:
>
> > Can you show how your LISP system would work with two other theories of
> > truth besides Aristotle's theory (1) Coherence theory and (2) The
> > Coherence Theory of Truth?
>
> Hi,
>
> OK. Fundamentally I use lambda calculus and an Aristolean
> theory of truth for natural language semantics - for the actual
> process of reducing English sentences to first order logic. Its
> powerful and very clean.
>
Please comment upon this portrayal of your foundation;
A is A: Aristotle's Law of Identity
Everything that exists has a specific nature. Each entity exists as
something in particular and it has characteristics that are a part of
what it is. "This leaf is red, solid, dry, rough, and flammable." "This
book is white, and has 312 pages." "This coin is round, dense, smooth,
and has a picture on it." In all three of these cases we are referring
to an entity with a specific identity; the particular type of identity,
or the trait discussed, is not important. Their identities include all
of their features, not just those mentioned.
Identity is the concept that refers to this aspect of existence; the
aspect of existing as something in particular, with specific
characteristics. An entity without an identity cannot exist because it
would be nothing. To exist is to exist as something, and that means to
exist with a particular identity.
To have an identity means a single identity; an object cannot have two
identities. A tree cannot be a telephone, and a dog cannot be a cat.
Each entity exists as something specific, its identity is particular,
and it cannot exist as something else. An entity can have more than one
characteristic, but any characteristic it has is a part of its
identity. A car can be both blue and red, but not at the same time or
not in the same respect. Whatever portion is blue cannot be red at the
same time, in the same way. Half the car can be red, and the other half
blue. But the whole car can't be both red and blue. These two traits,
blue and red, each have single, particular identities.
The concept of identity is important because it makes explicit that
reality has a definite nature. Since reality has an identity, it is
knowable. Since it exists in a particular way, it has no
contradictions.
http://www.importanceofphilosophy.com/Metaphysics_Identity.html
Many people get their philosophy from little paperbacks that talk about
"Aristotle's Law of Identity." The exercise is to write a paper about
it. What is the Law of Identity? How did it come up, i.e. what was
Aristotle talking about when he introduced it? What role does it play
in his philosophy, and in subsequent philosophical systems?
You are supposed to write this paper off the top of your head, based on
what you have heard, or what you have learned in class, or what you
have learned from your own reading. In other words, write it without
going to the library.
"The mark of an educated man is the clarity of the line drawn in his
mind between what he knows and what he doesn't know."
Is there such a line in your mind? Look over what you have written
about the law of identity, and ask -- which side of the line is it on?
Are you sure?
http://www.geniebusters.org/915/04d_ex01A.html
[the above is groping baby, you know like metaphysics or starting from
scratch playing the dumb role, thats how me and JJ operate. but you
want to start further up the way (heathen life without FAQs)]
-----------------------------------
identity/non-identity
identity/non-identity. I have used the word "central" to describe most
of the korzybskian terms I have presented so far in this glossary.
That's how it goes in a system, a neuro_linguistic_cohort, where every
defining term is directly related to all of its verbal associates. No
cluster of terms can be said to be more 'central' to general-semantics
than non-identity and its rejected misevaluation, "identity."
I deem it useful that we consider non-identity from two points of view:
the historical ('Aristotelian') and the specifically korzybskian.
The 'Law of Identity' of Aristotle had been challenged on limited
verbal-philosophical grounds by Western scholars well before Korzybski.
The challenges to and/or rejections of the Aristotelian "Laws of
Thought" have a long and honorable history, beginning with Aristotle's
own period (384-322 B. C.), reaching an early peak during the mediaeval
era (pace, Thomas Aquinas), but rising to a sturdy chorus from the
mid-nineteenth century and reaching a most personal crescendo in the
writings of Korzybski.
It seems worth pointing out here that Korzybski's position was not
anti-Aristotelian. He expressed great respect for the achievements of
Aristotle (one of the dedicatees of Science and Sanity). Korzybski's
concern was to show the limitations of the Aristotelian orientation,
especially as developed by Aristotle's followers over the last 2500
years. Indeed, Aristotle did not himself formulate the 'Law of
Identity'; it was said by his disciples and interpreters to be implied
or presupposed with reference to his explicitly stated laws and by his
methodological treatises in general (Organon ). (1) By
"non-Aristotelian" Korzybski formulated a point of view which
encompasses the valuable aspects of Aristotle while going beyond ('non'
in the modern, philosophical-scientific sense) the great formulator
from Stagira. After all, Aristotle saw 'logic' as only a preparation
for scientific knowledge, not as knowledge itself. (2) He is regarded
as the first in both 'West' and 'East' to insist on rigorous scientific
procedure, i.e., to be what we would call extensional and what the
general scientific community would call experimental: i.e.,
self-challenging via non-verbal (silent level) tests and observations.
Korzybski was fully aware of all this and took pains to point out that
his non-Aristotelianism was targeted to a rigid commitment to aspects
of Aristotle which Aristotle himself might have rejected - especially
if he lived in 1933! However, Korzybski forthrightly rejected
Aristotle's essentialism which became so 'spiritualized' by Thomas
Aquinas (the 'substance' and 'accidents' opposition) and others during
the heyday of Scholasticism.
"Identity" in the domain of formal logical discourse, which usually
remains strictly verbal/intensional, simply affirms that a statement is
' itself ': "A is A," in modern usage, a tautology. The copula "is,"
which links the terms of the above proposition ("A is A"), Korzybski
called the "is of identity." (3) He maintained that, even at this
level, statements of identity ("absolute sameness in 'all' respects")
are false for many structural (process) reasons. He did not, however,
deny that we can agree on a kind of " 'is' of stability" (my
formulation: RPP) to provide consistency within discourse. After all,
he often said, when misquoted or misinterpreted, "I say what I say; I
do not say what I do not say!" But when used to refer to experiences in
general, including not only our statements but the non-verbal processes
which subtend and give rise to them, identity statements are not only
invariably structurally false to fact but potentially dangerous.
Korzybski was not a practitioner of modern logical-mathematical
formalism. He did not attempt to present 'breakthrough' formulations in
the rather hermetic and hieratic fields of symbolic logic, mathematical
logic, propositional calculi, etc., though he did recognize their value
as disciplines which might find eventual applications. (Witness the
burgeoning field of 'software engineering'.) Yet he did construct a
meta-linguistic schema for examining the structural relations among
languages, nervous systems, non-verbal structures-in-general, and human
doing. He called it "General Semantics," designed for adequately
formulating those structures and combatting neuro-linguistic
auto-intoxication.
This is where the "identity" that most concerned Korzybski comes to the
fore. When humans who are engaged in abstracting identify (confuse)
orders of abstracting, they are "identifying" in the uniquely
korzybskian sense. Korzybski emphasized that orders (levels) of
abstracting, while constituting mutually-influencing phases of a
totality, (4) ought not to be mistaken for 'each other.' He affirmed
this identification as the primary mechanism of misevaluating.
"The word is not the thing." Indeed. But neither are non-verbal
('silent') perceptions, 'feelings', etc., to be confused with the
quantum-level processes to which they are personal summary responses
(ultimately, semantic reactions). We ought not to confuse the state of
our bellies with the state of the world, even though we-bellies are
part of (but only 'part' of) that world.
Human nervous systems/brains (organisms-as-wholes) con- stitute mapping
systems. We abstract. Our abstractions are maps that we have
constructed. The formulation of non-identity, so central (again) to
general-semantics, reminds us that, though we can (must) build useful
maps to make our way in the world, "The map is not the territory."
http://www.generalsemantics.org/Articles/Glos7idn.htm
----------------------------------
> You're right in suggesting that correspondence theory is not unique
> amongst philosophical approaches to truth. Coherence theory was
> adopted by some very eminent thinkers of the Vienna Circle. The
> passage in Quine's "Two Dogmas of Empiricism" about the web of
> belief is very much coherence-oriented.
>
> I suppose I would begin by drawing a distinction between
>
> (a) what it *means* to say something is true and
> (b) how we tell if something is true.
>
> Not everybody accepts this distinction - for example constructivists
> deny this distinction exists in maths. But its a useful distinction.
>
> I think coherency theory of truth probably has the most contribution to
> (b) - to the process by which we sift conflicting evidence to come up
> with what we regard as a satisfactory set of principles. What
> Aristotle has to say really contributes to (a).
>
> * Both theories actually have an important part to play in the
> computer manipulation of written material.*
>
> Aristotle's ideas can be used to promote the 'understanding' of text.
> But coherency theory will be needed to give computers the capacity
> to sift vast amounts of intelligence and produce some coherent
> believable conclusion. Its a multi-million dollar challenge. The
> answer will require a model of coherency in terms of a weighted
> network. I won't say more here.
>
> So the answer to your question is that my system (which is Qi, rather
> than Lisp) does not use coherency theory because the problem it was
> addressing does not require it.
>
> But the seperate problem I've alluded to does.
>
> Mark
Immortalist wrote:
> Can you show how your LISP system would work with two other theories of
> truth besides Aristotle's theory (1) Coherence theory and (2) The
> Coherence Theory of Truth?
Hi,
OK. Fundamentally I use lambda calculus and an Aristolean
theory of truth for natural language semantics - for the actual
process of reducing English sentences to first order logic. Its
powerful and very clean.
You're right in suggesting that correspondence theory is not unique
amongst philosophical approaches to truth. Coherence theory was
adopted by some very eminent thinkers of the Vienna Circle. The
passage in Quine's "Two Dogmas of Empiricism" about the web of
belief is very much coherence-oriented.
I suppose I would begin by drawing a distinction between
(a) what it *means* to say something is true and
(b) how we tell if something is true.
Not everybody accepts this distinction - for example constructivists
deny this distinction exists in maths. But its a useful distinction.
I think coherency theory of truth probably has the most contribution to
(b) - to the process by which we sift conflicting evidence to come up
with what we regard as a satisfactory set of principles. What
Aristotle has to say really contributes to (a).
* Both theories actually have an important part to play in the
computer manipulation of written material.*
Aristotle's ideas can be used to promote the 'understanding' of text.
But coherency theory will be needed to give computers the capacity
to sift vast amounts of intelligence and produce some coherent
believable conclusion. Its a multi-million dollar challenge. The
answer will require a model of coherency in terms of a weighted
network. I won't say more here.
So the answer to your question is that my system (which is Qi, rather
than Lisp) does not use coherency theory because the problem it was
addressing does not require it.
But the seperate problem I've alluded to does.
Mark
From: Jan Burse
Subject: Re: NLP translation in Qi-YACC - an elegant way
Date:
Message-ID: <455E2679.4010105@fastmail.fm>
Hi
Yeah aristoteles alone, would only give monadic logic.
Very bad for comparatives, pr�positions etc..
Bye
Mark Tarver wrote:
> Hi Jans,
>
> Alternatively you can do it this way - which is very elegant.
>
> The theory of transduction into FOL being used in this Qi program
> is based on Aristotle's theory of truth which loosely paraphrased
> says "to say of what is that it is or what is not that it is not, is
> true."
>
> You can look for the full quote in http://en.wikipedia.org/wiki/Truth.
>
> To put the matter in this idiom, an Aristotelian theory of truth for
> natural languages (NLs) says that a sentence is true if the verb
> phrase (VP) correctly applies to the subject of the noun phrase
> (NP). "Mark is bald" is true just when "bald" is correctly applied
> to the denotation of "Mark". Tarski's Semantic Theory of Truth
> is really Aristotle brought up to date by being released from the
> constraints of Aristotelean logic and applied to FOL.
>
> You can use the same idea to elegantly parse NLs by transducing
> the VP into a lambda abstraction and the NP into a term. The
> correct translation is then produced by applying the transduction of
> the VP to the transduction of the NP - i.e. by beta reduction.
>
> So "Mark is bald" becomes ((/. X [bald X]) Mark) (/. is lambda in Qi)
> and this reduces to [bald Mark]. Something like this is going on in
> the Qi program I cited.
>
> Now to answer your question about the computer recognising the
> absurdity of fat slim girls etc. This does require an inference
> engine.
>
> But if you use the approach above, you can actually place the
> semantic rules into the transduction rather than into the domain of
> the inference engine. This has the advantage of being very
> efficient.
>
> How can you do this? OK; lets take "Mark is slim". We transduce to
>
> ((/. X (slim X)) Mark)
>
> Notice that we are actually applying a function slim here to Mark.
> (In Qi [ ] forms lists and ( ) applies functions). So Qi will say
> 'Hey! What is this 'slim' function?'. So what we do is define it.
>
> (define slim
> Subject -> [~ [fat Subject]])
>
> Here 'fat' is a semantic primitive. But it need not be. We could
> define it as another function.
>
> (define slim
> Subject -> [~ (fat Subject)])
>
> (define fat
> Subject -> [> [bmi Subject] 35])
>
> and so on. Hence your NLP system will automatically place the
> transduction into a canonical form using demodulation (rewriting)
> in which only your chosen semantic primitives appear. This
> forestalls the use of many semantic rules which inevitably pose
> computational overheads to the inference engine.
>
> Qi makes this sort of stuff very easy. Its an extremely powerful
> system.
>
> OK, I'm supposed to be doing meditation and yoga. But this
> came to mind.
>
> bw
>
> Mark
>
········@gmail.com wrote:
>
> Wrong! You're know Lisp and writing a program to do your homework for
> you should be a snap.
>
> Being a Lisp hacker, you know the first step is to build the language
> up to suit your new problem. What are the basic axioms of logic you'll
> need? Conjunction, disjunction, not/negation, material equivalence, and
> material implication...
>
raises-hand-in-a-I'm-not-yet-a-lisp-hacker-way .... doesn't that
suggest you should do it in Prolog.