One of my projects this week has been writing a
road-painting game which will eventually surface in some
form, largely at the prompting of my brother a few weeks ago
but I am just getting to it now.
Perhaps only to my own and ratxue's delights, it continues
my exploration of maverick acl2. To resemble my brother's
idea, I'm writing it for compilation targets that ecl
matches.
QUICK CLARIFICATION OF ACRONYMS
acl2 is an *automatic* theorem prover; a computational
logic for an applicative subset of common lisp
ecl embeddable common lisp is a common lisp compiler that is
just a C library, libecl. Since C is ubiquitous, this is a
way of easily getting common lisp programs *anywhere* such
as if one desired it, the proprietary apple store, the
proprietary steam store, the proprietary google store for
example if this was the only way to get the program onto a
non-free device. If you wanted to embed ecl in golang, one
could compile the ecl to a C lib and use the C lib in
golang, which is supported. The big C dependency is the
Boehm garbage collector. ECL conses quite a lot, leaning on
garbage collection.
END OF CLARIFICATION
An idea that came to me was the reusability of theorems to
infer truths you couldn't personally reach, the magical
value-adding of acl2's automatic nature implying natural
feature reuse.
Imagine that a game is a collection of capabilities and a
puzzle where the puzzle contents and capabilities imply a
way of reaching the next level. defthm the idea that the
player has the capability to reveal unknown locations, and
has some unknown locations that if revealed allow the
character to reach the next level. So I could do some higher
level reasoning about a space of games using the same lemmas
- imagine the memory card-flipping game, or cutting grass in
a walking simulator in order to find a dropped key. This
would be cooler if I had implemented these already, but this
was an exciting conceptual discovery for me.
Call the capabilities acl2-compatible lambda forms and the
game state an acl2 single threaded object acted upon by
those lambda forms. Then I could have a theorem about a
permuted set of features I hadn't personally thought of
putting together that the character has the capabilities to
act on the level (single threaded object) to advance in the
game.
Single threaded objects in acl2 are a generalisation of its
early von neumann state in theorems, used in some examples
with a non-canonical #'seq acl2 macro which is essentially a
forward pipe operator
#|addendum
If for some reason you know R, imagine magrittr
(I'm not going to explain R's implementation but arbitrary
strings can be new infix operators) bad analogy:
> add-1 "%>%" add-2 "%>%" add-3 "%<%" 4
10
the number four was a stobj here ;p
|#
This pushes me to jettison non-acl2 common lisp, such as
progn forms (though seq is basically that) and my dear clos.
The exploration continues.
