K-user mailing list

["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

Attachment: sums.k
Description: sums.k

Attachment: maj.k
Description: maj.k