I have my collection of Sandewall’s open-access paradigm knowledge here. Here, we are going to look at Sandewall’s pedagogical SAT solver example. SAT means CONSTRAINT SATISFACTION (search). Sandewall is not just teaching ∃SAT-SOLVERS, though he does that, but rather their implementation, and the Leonardo system as a medium for such with ANSI CL as the host language. This is from a lab from a course Sandewall taught in 2010.
Here we will just march through git-cloning, starting, and running Sandewall’s base example from his SAT-SOLVER lab.
Note I am using emacs eev-mode.
• (find-git-links "https://codeberg.org/tfw/pawn-75")
whence I guess you have cloned that into something like ~/usrc/pawn-75.
Aside, Sandewall’s lifelong hypothesis was that machine learning should be understood and expected to be something that happened over the course of a software’s life measured in months or years. So please consider making a new software (Leonardo system software individual) as being like adopting a kitten or puppy not-just-for-christmas (actually in Sandewall’s writing, his metaphor is a grandchild).
Assuming the git location ⬆
mkdir ~/leocommunity/
cp -r ~/usrc/pawn-75/Pawn-75 ~/leocommunity/saturn
saturn in lisp without emacsThis would be your normal (re-)entry point to this software-individual.
cd ~/leocommunity/saturn/utilus/Process/main
clisp -E iso-8859-1 -modern
(load #P"../../../remus/Startup/cl/acleo.leos")
(cle)
• (setq inferior-lisp-program "clisp -E iso-8859-1 -modern")
• (slime)
• (setq eepitch-buffer-name "*slime-repl clisp*")
(require "asdf") ; might need to (load "asdf.lisp") instead
(require "uiop")
(uiop:chdir "~/leocommunity/saturn/utilus/Process/main/")
(load #P"../../../remus/Startup/cl/acleo.leos")
(cle)
I.e. Decision-trees library knowledgebase.
ses.225) loadk dtc-lib-kb
Load-ef: dtc-lib-kb at ../../../demus/Dtc-lib/dtc-lib-kb.leo
Load-ef: dtc-onto at ../../../demus/Dtc-lib/dtc-onto.leo
Load-ef: dt-nonprob at ../../../demus/Dtc-lib/dt-nonprob.leo
Load-ef: dt-prob at ../../../demus/Dtc-lib/dt-prob.leo
Load-ef: caunet-defs at ../../../demus/Dtc-lib/caunet-defs.leo
ses.226) loadk dt-logcond
Load-ef: dt-logcond at ../../../demus/Dtc-lib/dt-logcond.leo
ses.229) curtree log-tree-1
ses.230) pula
[block
[:= a b
:label L-02 ]
[loop v 1 100
[loop a 1 v
[routine-2
:label L-05 ]
:label L-04 ]
:label L-03 ]
[:= c v
:label L-06 ]
:label L-01 :pred2 t :pred3 {foo fie} ]
ses.231) lode
Several solutions found:
red for .x = L-06
yellow for .x = L-03
red for .x = L-02
The mnemonics are pula put-labels and lode logical-decision-tree. This file in the knowledgebase contains the useage though I will expound a bit here.
The default test observed-structure (also a tree, but that is a confusing name collision with the later decision-tree which we will call a tree about this observed-structure) is
-----------------------------------------------
-- log-test-11
[: type observed-structure]
[: has-structure
[block
[:= a b]
[loop v 1 100 [loop a 1 v [routine-2]]]
[:= c v]
:pred2 t :pred3 {foo fie}
]]
---------------------------------
this is the data being operated on, I guess describing a computer program with some nested looping constructs.
The default decision tree - the sort-of query being solved for is
----------------------------------------------
-- log-tree-1
[: type decision-tree]
[: has-tree [? [is-loop .t]
green
[?? .x [has-subexpr .t .x]
[? [is-loop .x] yellow red]
violet ]
]]
this solves for
.x inside a node (basically a sequence).t in the failure branch of the [is-loop .t] predicate, which is to say .t is not itself a loop..x is a subexpression of the .t.x is a loop, the solution is yellow, if not, the solution is red.We can see from the result output,
ses.231) lode
Several solutions found:
red for .x = L-06
yellow for .x = L-03
red for .x = L-02
ses.230) pula
[block
[:= a b
:label L-02 ]
[loop v 1 100
[loop a 1 v
[routine-2
:label L-05 ]
:label L-04 ]
:label L-03 ]
[:= c v
:label L-06 ]
:label L-01 :pred2 t :pred3 {foo fie} ]
Note I changed to the demo.txt test using curtree, the default one from the lab solved for multiple variables with results also being in terms of those variables.
Sandewall suggests you could either edit the trees and tests in place and re-loadk dt-logcond
if you do not know how to write crefil my-tree-file, loadk my-tree-file, put my-tree type decision-tree, addmember (get my-tree-file contents) my-tree, writefil my-tree-file, make your own tree in in your prefered text editor, and loadk my-tree-file your own tree.
Here we went through exactly a piece of Sandewall’s lisp ai course labs 2 and 5. Actually, in my own software-individuals I rewrote it a bit, but here I stuck closely to the lab as it was taught in 2010 at IDA / the university of Linkoping.
The SAT solver - logical decision tree processor - seems to be eminently useable in my experience so far. Sandewall describes his implementation as being algorithmically efficient - but for pedagogical purposes. It is a key example of the sorts of additional knowledge of how-to-do-things Sandewall regarded the adding-of-which as the personal growth of a particular software individual in his vision of what machine learning should be.
Sandewall, similar to John Allen, I believe had a strong principle of using lisp without embellishments as the host language for their logical systems, while having the strict separation that the system they wrote is not the same thing as the host lisp, and they do not really co-occur in program running.
This is quite different to the modernly conventional style of frankensteining a mess of opaque additional functions into the host language (python, for an example) and acting like the additional frankenlimbs are part of the language itself. Lisp does account for this by de facto canonicalising certain packages in the community, and also by having the my-package-user namespace convention.
Sorry about my absenteeism recently. Catch everyone at the https://anonradio.net live show in a two hours (Tuesday evening in the Americas; 0UTC Wednesday in the universe).
Did you create your first software-individual? Tell me / other commentary on the Mastodon please as always.
screwlisp proposes kittens