K-user mailing list

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

Thanks! I'll reply to both of these helpful messages at once.

Grigore:

I had looked at LOGIK—it convinced me that my language was likely possible to represent in K, although my needs are more complex (negation-as-failure, default reasoning and precedence levels, aggregation, etc) so I may have to explicitly represent search in my semantics (which actually seems to be a common feature of logic programming languages).

Are LOGIK clauses each stored in their own cell simply in order to use implicit sets-of-cells instead of an explicit set in a cell like "<clauses>... SetItem(Clause) ...</clauses>"? Are there performance tradeoffs there, or is it solely an elegance thing?

Traian:

Thanks for the tip on how KOOL produces cell structures out of syntax, that is quite helpful and I will probably use it in the process of implementing search over facts and intensional predicates.

The idea of storing schemae more or less as-is and using a more complicated retrieval mechanism is certainly attractive, because it seems like it will be of similar complexity to searching over prefixes anyway. I may pursue that and report back.

Here's a link to the definition and some test files, although things are working now and I have no specific problem besides "It doesn't feel very K-like".

http://users.soe.ucsc.edu/~jcosborn/game-k.zip

The language is "game.k" because this is to be a language for defining board and card games, but that's neither here nor there. Expected output is also given. The approach I ended up taking was the "cloning" approach where a special "clone(A,B)" syntax bubbles up from the first choice-marker, swallowing up the following HOLE-y syntax (e.g. clone(A,B) ~> HOLE . T => clone(A.T, B.T)), and splitting "clone(A,B) ~> define(HOLE)" into "define(A) ~> define(B)". The procedural nature of it bugs me though, so I think that once I have queries in place I will try removing this stuff and replacing it with a query mechanism that can query over un-instantiated schemae.

I have a couple of other scattered questions that may have specific answers:

1.) Can line comments be described in K syntax? I can imagine how to do block comments fairly straightforwardly (syntax BlockComment ::= "/*" K "*/" ; rule /* Cmt */ => .), though I would have to include BlockComment in a lot of productions.

2.) If I have a sort that can conditionally be a final result based on a predicate (e.g. isGroundTerm()), can I say something like "syntax KResult ::= isGroundTerm( K )" and have it do the right thing?

3.) The "forall" and "exists" predicates in k-symbolic.k. I guess that the "Bool" I give can be a predicate (added to Bool via "syntax Bool ::= ...") with variables named in the given set. Could I use these to quantify over a variable whose domain is given as a set? Alternately, is there a way to ask K to give me all the terms which would match a pattern (maybe within a given cell or set?)? I need the capability of aggregating results in my language, so if I could reuse existing machinery that would be great.

4.) I wanted to use Lists in various places in the syntax, but it introduced a lot of ambiguities so I gave up. I'm not sure I understand the proper use of List, but basically: Is it possible to use List unambiguously without "trapping" it inside of containing syntax like "var Ids ;"? I kept ending up with a lot of ambiguous cases with empty lists.

Thanks very much,

Joe

On Feb 8, 2013, at 05:17 , "Rosu, Grigore" <grosu AT illinois.edu> wrote:

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