K-user mailing list

[Joseph Osborn <joe.osborn AT me.com>]

Hello!

I'm new to K (my only experience is reading and watching tutorials, writing a 
small Forth, and helping debug a Scheme) and I've spent the last day or so 
thinking about how to represent a particular feature of my language. It's a 
relational language, though the syntax strays a bit from simple Horn clauses. 
My extensional knowledge is written as a kind of dot-separated path of ground 
terms (with the expectation that later, I can query on prefixes or use globs):

> an example program. each line will add one fact to the knowledge-base.
> fact
> fact.postfix
> fact.path.to.postfix
> fact.2

I've borrowed a notation from Answer Set Prolog to make writing groups of 
similar facts easier:
> Either of these will produce term.1.term, term.2.term, ... term.5.term.
> term.1..5.term
> term.1;2;3..5.term

> This one produces fact.0.0, fact.0.1, fact.0.2, fact.1.0, ...
> fact.0..2.0..2

So, a statement is a fact schema which is used to define a set of facts.

But the problem I've run into is how to represent this in K. I've tried 
several approaches, but they all fall flat when it comes to the choice 
operator (;). If the syntax rules are strict and the choice floats up to the 
top of K, splitting it there does me no good; I have to duplicate the entire 
schema that they're a part of. But if I try to work on the whole statement at 
once, it becomes very difficult to write modular rules in case I add new 
shorthands or features (and I'm not convinced that such rules will work for 
deeply nested syntax trees).

The only way I've been able to come close is by proceduralizing my semantics: 
I turn a fact schema into a "processFact(Schema, List{GroundTerm})" (I've 
tried it with a Fact as the second parameter but I have trouble building up 
the term correctly) and match cases for (Schema . GroundTerm), (Schema . (I1 
.. I2)), etc -- and when encountering (Schema . (A ; B)) I produce 
"processFact(Schema . A, SoFar) ~> processFact(Schema . B, SoFar)". 

But this is terribly unsatisfying (I feel like I'm working around K) and 
what's worse I keep running into weird issues with termination when I try to 
turn the List{GroundTerm} back into a T1 . T2 . T3 form (via another special 
bit of syntax). Anyway, it's just unpleasant all around and I wonder if 
there's a proper K way to do it.

Three other approaches I've considered have been:
  1.) trying to pass a "clone(A,B)" term backwards into the K cell (e.g. 
clone(A,B) ~> (T1 . HOLE) => clone(T1 . A, T1 . B)) and stopping at a 
"defineFact()" term, but that only works for predefined hole-positions;
  2.) building up the candidate facts in a cell (pretty much the same as what 
I'm doing, but harder to find my place at each step--plus I don't know how to 
say "for every fact F in this cell, turn it into F . Term" or something)
  3.) making "." strict and permitting "choice(N)" as a ground term; when one 
is created, a current_fact cell is given a map item mapping from a fresh N 
|-> (A,B); this is used at assertion time to instantiate the schema. This 
fell down on clauses like a.b;c.d;e that have two choices at different 
positions, since the machinery for finally asserting the fact couldn't 
distinguish between "a ground fact" and "a fact with choices remaining".

So, what's the "K way" to do something like the above, imagining that the 
configuration is:

configuration <k> $PGM:Program </k> <facts> .Set </facts>

and that a Program is a sequence of fact schemae?

(I'm tempted to just give in and write a preprocessor—please save me from 
bailing out on one of my language's most basic features!)

Thanks,

Joe Osborn
University of California, Santa Cruz
Expressive Intelligence Studio
http://eis.soe.ucsc.edu