#+TITLE: car-game readme
#+AUTHOR: screwtape

* car-game
Car-game currently contains mutually compatible ACL2 and common lisp code for making rectilinear hypergrid alists.

** ASDF3
It is an ASDF3 project directory tree that should live in ~/common-lisp/ or ~/.local/share/common-lisp/source/ and has some utility as a reference on ASDF projects.

** ACL2
In the ACL2 module directory (notably not an asdf module) there is a Makefile which certifies (compiles and signs) macros.lisp and car-game.lisp under the package nickname "ACL2-USER" with a simple defthm as a #!/bin/sh script which also is a trivial stobj (single threaded object/von neumann state) example.

Since ACL2 is an applicative subset of common lisp, functions are written to use tail recursion with clearly implied measures. Compilation such as operated by asdf as required in general replaces tail recursion with efficient iteration, however alists are not otherwise a very optimised data structure.

** Side effects
There is a defun for creating graphviz dot graphics from hypergrids (styled stobjs) in side-effects.lisp. side-effects.lisp also houses lisp definitions of ACL2 built in utilities. Currently not very strict but intended to be the the definition :docs from ACL2.

** Usage
*** Dependencies
acl2, a common lisp and graphviz for generating dot graphics.
#+begin_src shell
  apt install acl2 ecl graphviz
#+end_src

*** common-lisp with graphviz dot
#+begin_src lisp
  (require 'asdf)
  (require 'car-game)
  (in-package :car)
  (defvar *stobj-alist* (reset nil))
  (setq *stobj-alist* (make-connected-grid *stobj-alist* 3 2))
  (look *stobj-alist*)
#+end_src

**** output png
[[file:acl2/tmp.png]]

*** acl2
#+begin_src shell
  cd ~/common-lisp/car-game/acl2/
  make all
#+end_src

** Future

*** Hypergrid alist applications
Non-dense association list serialised rectangular meshgrids are always kind of useful. In particular the alist could output CLML sexp or be used directly as a basis for toy machine learning. The current functions slowly remove previous degenerate alist keys in general to avoid some memory leak scenarios.

ACL2 needs proof support especially about interrogating what is in a stobj-alist and how to measure it, this has not been done at all yet (though there is an example proof that a one by three meshgrid will have a list of length three as the cdr assoc of 'NODES). It needs more guards and support to replace any particular integer with a free variable. This is promising for creating first order logic proofs of common lisp software applications which are amenable to representation with meshgrids and is already useful for describing finitely constrained applications.

*** Future features
While it currently closely resembles what I wrote for Wumpus hunting when we were looking at Land of Lisp, my initial motivation here was to make an AI path-painting game after talking to my brother about that sort of thing. To keep things challenging, the direction I am taking that is to define games as meeting a set of criteria for acheivability with the player given a set of capabilities (lambdas) to act on a notion of von neumann state and hence prove the existence of a set of unplanned games rather than just the one.

Already mentioned, for CPU based high performance machine learning interoperability side-effects for BLAS-based CLML are planned. I am sure we both know that graphics cards are not very good for machine learning which involves syncronising different positions in memory, and do nothing even remotely like thousand-times speedups with their single-threaded task dispatching so this sentence really did not need to be here. BLAS refers to the academic precedent and hence eternal high performance algebra library implemented in fortran. CLML is the largest Japanese telco's data division's machine learning common lisp package. There is a glimmer of doing the oh-so-academic deep learning piled with proofs we can prove to obfuscate the presence of proofs we can't prove yet.

*** More side effects
It was on my mind so I am planning to add trivial-garbage to the side-effect side of things, and have SDL2, libgmsh and jns' Eternal Game Engine side effect outputs.

ACL2 has a notion of arrays which could result in more optimised common lisp compilation, and I believe there are books of theories supporting that and hopefully weak hash-tables as well.

Since I've seen Albatross around, I might also take an exploratory journey into network MUDs (with theorems proved about their nature).

*** Since this is just a phlog phost now
I also want to crash first order logic theorems against ad hoc or regression testing, though I need a more comprehensive model of or instead of my simple alist stobjs at the moment. There are many obvious interesting targets for automatic theorem provers associated to high performance realisations of its theories.

* Signature
Truly,
screwtape.

gopher://gopher.club/1/users/screwtape