K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Don't know if this helps, but you may also take a look at LOGIK (logik.k), where a program is a set of Horn clauses which are stored in a cell, each in its own subcell.

 

Grigore

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Traian Florin Șerbănuță [traian.serbanuta AT info.uaic.ro]
Sent: Friday, February 08, 2013 7:13 AM
To: Joseph Osborn
Cc: k-user AT cs.uiuc.edu
Subject: Re: [K-user] K Idioms for Instantiating Schemae

Hello Joe,

I'm not sure I fully understand what you want, but we often preprocess programs in K and turn them into data structures which are more amenable for retrieval during execution.  As an example you can check what we do for kool (examples/kool/untyped/kool-untyped.k) or logik (examples/logik/logik.k).

Admittedly, we don't do any rule expansion in either of them.

A possible option would be to leave them as they are, and have a more complicate retrieval mechanism in the semantics.

Unfortunately, I don't think we have any standard way of achieving this.  But if you have problems, please send me/us the definition and a description of a specific problem you are trying to address, and we'll do our best to help.

best wishes,

- traian

2013/2/7 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
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user