K-user mailing list

[Traian Florin Șerbănuță <tserban2 AT illinois.edu>]

Hi Brandon,

I've been thinking a bit about this, and this is something which might help you progress, perhaps.

What I would try would be using contexts with side conditions restricting the heating to only take place when no rule applies (you can probably do this with a predicate). 

Then, tag all rules with supercool to ensure that computation is cooled completely after each execution step.

Grigore might not like this idea as he views supercooling as the "opposite" of superheat, while in your case would be more the opposite of the side conditions to the rules.   Admittedly this will be pretty inefficient as you probably only want to cool it one step.  But it is something to try, I think.

best wishes,

- traian

2012/2/15 Moore, Brandon Michael <bmmoore AT illinois.edu>

I'm trying to define a language with a function
that is not strict in any argument, but can
reduce when various subsets of the arguments are ready.

It seems superheat doesn't look for reductions inside
arguments that are not marked strict, but if an argument
is marked strict then K will not try to apply rules at the
top level until that argument becomes a value.

A simple example is a language with a majority function,
evaluated and unevaluated booleans, and a stuck non-value
_expression_. A full definition is attached in maj.k
Here's a grammar

syntax Exp ::= Val | "tE" | "fE" | "stuck" | "majority" Exp Exp Exp
syntax Val ::= "T" | "F"

The unevaluated boolean tE/fE reduce in one step to the evaluated
booleans T/F, and majority should reduce as soon as any two arguments
have reduced to the same  booleans.

Is there any way to adjust the strictness, attributes, or contexts so all of
majority tE tE stuck
majority tE stuck tE
majority stuck tE tE
compute only to T? Without --search, only the last does.

Something closer to my full language is attached as sums.k
It adds binders, and now the results of --search do not
necessarily even include the correct result.

I've tried combination of marking either string or string(1),
whether or not to mark "alt" strict, whether to include Alt
in KResult, and whether or not to include the context
patterns, with no success. Two incompatible examples
are getting

either stuck
 (alt a . (lambda x . left x) a)
 (alt b . (lambda x . left x) b)

to reduce to

left (either stuck (alt a . a) (alt b . b))

and getting

either (lambda v . left v) (lambda x . x)
      (alt f . f (f z))
      (alt f . stuck)

to reduce to

z

Is it possible to do this? Does the superheat system or
its interaction with context/rules need to be changed to
make this possible?

Brandon