car-game readme

acl2, a common lisp and graphviz for generating dot graphics.

apt install acl2 ecl graphviz

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.

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.

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).

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.