Kinds of strategic programming errors

The examples on this page use the following algebraic data type for arithmetic expressions:

abstract class Factor
case class Var(s: String) extends Factor
case class Num(i: Int) extends Factor

abstract class Term
case class Mult(t: Term, f: Factor) extends Term
case class BaseTerm(f: Factor) extends Term

abstract class Expr
case class Plus(e: Expr, t: Term) extends Expr
case class BaseExpr(t: Term) extends Expr

object Examples {
val tree1 = Plus (BaseExpr (BaseTerm (Num (3))), Mult (BaseTerm (Num (4)), Num (6))))
val tree2 = Plus (BaseExpr (BaseTerm (Num (3))), BaseTerm (Num (2)))

def full_td (s:Strategy): Strategy = {s <* (all (full_td (s)))}
def full_bu (s:Strategy): Strategy = {(all (full_bu (s))) <* s}
def stop_td (s:Strategy): Strategy = {s + (all (stop_td (s)))}
def once_bu (s:Strategy): Strategy = {one (once_bu (s)) + s}
def innermost (s:Strategy): Strategy = {repeat (once_bu (s))}
}


All the examples are rendered in Kiama<https://code.google.com/p/kiama/>_. Kiama was chosen because it is a stratego-like language embedded in a general purpose language. The stratego-like language allows our encodings to have a close correspondance with existing literature and the general purpose language ensures we can render all the examples (even if the encoding gets a bit dense).

Application Errors [Mamet11].

Application of a strategy to a term that always fails, for example [Mamet11]:

object ApplicationErrors {

strategy {
case (Plus(BaseExpr(BaseTerm(Num(0))),pat)) => Some (BaseExpr(pat))
case otherwise => None
}

def main(args: Array[String]){
}
}


TODO: I am wholey unconvinced by this example. The point is that the strategy will always fail, but why must I never run a strategy which will always fail? What if my input has no zeros? Even the correct version would then still always fail.

UPDATE: Think of it more like the boolean test - if you can say an if branch is never executed - that's an error. This means you need to come up with a better example. Detecting this is much better suited to static analysis and will probably remain there. Did the static analyis people mamage to track this error statically?

This error appears to be analagous to having a method that is never called in OO programming. We expect this to happen all the time and it is only an error when we expected a method to be called for a certain input and it is not. Thus I think the approach to detecting these errors should be more like mock-objects than like static typing.

Sequential composition errors [Mamet11].

val timesZero =
strategy {
case Mult(BaseTerm(Num(0)),pat) => Some (BaseTerm(Num(0)))
case otherwise => None
}
val timesZeroDash =
strategy {
case Mult(x,Num(0)) => Some (BaseTerm(Num(0)))
case otherwise => None
}

val timesZeros = timesZero + timesZeroDash

val timesOne =
strategy {
case Mult(BaseTerm(Num(1)),pat) => Some (BaseTerm(pat))
case otherwise => None
}
val timesOneDash =
strategy {
case Mult(x,Num(1)) => Some (x)
case otherwise => None
}

val timesOnes = timesOne + timesOneDash

val simpTimes = timesZeros <* timesOnes

val simpTimesDash = timesOnes <* timesZeros

def mainDash(stg: Strategy){
println(rewrite(stg)(Mult(BaseTerm(Num(10)),Num(10))))
println(rewrite(stg)(Mult(BaseTerm(Num(10)),Num(1))))
println(rewrite(stg)(Mult(BaseTerm(Num(10)),Num(0))))
println(rewrite(stg)(Mult(Mult(BaseTerm(Num(10)),Num(0)), Num(1))))
}


simpTimes will fail on everything because the output of timesZeros will always cause timesOnes to fail. simpTimesDash will fail on a great many things but can concievably pass (as the last example shows).

simpTimes is a clear programming error. A strategy that always fails on all input (aside from fail) is clearly an error we would like to catch. Can it be caught at compile time?

In this case, the correct strategy is timesOnes + timesZeros

UPDATE: potential rule: don't use sequence with strategies that fail. UPDATE: static proof that a certain strategy can never succeed UPDATE: include three-way <+ in here as well (subpart is a sequence) UPDATE: you want to know if the strategy might fail UPDATE: in the analaguous example (nested booleans) data flow analysis finds the error.

Conditional Composition Errors [Mamet11].

Called "Unreachable consitutents" in [Laemmel09].

val timesToPlus =
strategy {
case Plus(e, Mult(t, Num(x))) => Some(Plus(Plus(e,t), Mult(t, Num(x-1))))
case otherwise => None
}

val timesToPlusDash =
strategy {
case Plus(e, Mult(t, Num(2))) => Some(Plus(Plus(e,t), t))
case otherwise => None
}

val timesToPluses = timesToPlus <+ timesToPlusDash
val timesToPlusesDash = timesToPlusDash <+ timesToPlus

val removeTimes = repeat(timesToPluses)
val removeTimesDash = repeat(timesToPlusesDash)

def main(args: Array[String]){
println(rewrite(removeTimesDash)(Plus(BaseExpr(BaseTerm(Num(3))),Mult(BaseTerm(Num(4)),Num(6)))))
//println(rewrite(removeTimes)(Plus(BaseExpr(BaseTerm(Num(3))),Mult(BaseTerm(Num(4)),Num(6)))))
}


This is a clear programming error. It is analagous to unreachable code in an imperative language and should be rejected at compile time if possible, run time otherwise. An even clearer comparison is to pattern matching in functional programming languages. The reason the problem is more pressing in strategic programming is that different patterns can be composed in more ways than they can in functional programming. There is no way is Haskell, for example, to take a function which pattern matches on all numbers:

foo :: Int -> Int
foo x -> x + 1


and introduce a new case to it. Some strategic programming systems which are "more functional" in some way share this characteristic. For example, the problematic example cannot be encoded in SYB where the type class system imposes a constraint which prevents it. dgen also explicitly prevents it by not allowing the extension of one "strategy" with another which works on the same type. These systems are forcing a different style of programming which, in this case, is no less flexible because the rewrites are known in the same module. It does however present some compositions which are possible in Stratego.

Its the fact that pattern matching drop-down can be split accross functions which creates the possibility for this error.

Non-termination [Laemmel09].

object NonTermination{
def increment (d: Strategy):Strategy = {
strategy {
case Plus(e, t) => Some (Plus (Plus (e, t), BaseTerm (Num (1))))
case otherwise  => d (otherwise)
}
}

def main(args: Array[String]){
println (rewrite (full_td (increment (id))) (tree2))
println (rewrite (innermost (increment (fail))) (tree2))
}
}


As Lammel says,

"The intuitive reason for non-termination is that full_td applies the argument strategy prior to descent, which may be problematic in case the argument strategy increases the depth of the given term, which is exactly what increment does. If full_td is not appropriate for the problem at hand, let us try another scheme, be it innermost. Again, we witness non-termination: ... The combinator innermost repeats the traversal strategy ... until it fails, but it never does because the subtree position with the natural always fits."" -- [Laemmel09]

UPDATE: this is a good example of the fail/id/traversal combinations. full_td really needs the failover to be id and innermost needs rules to only fire if they move the tree closer to the end point. UPDATE: Guido? Can you find examples of full_td which does not use try?

Incorrect Quantification [Laemmel09].

This error occurs when the traversal goes into a part of the tree we don't want it to. In this case "quantification" means quanatifying the terms of interest. One way this is done is with pattern matching on the actual rewrite rule, but the traversal is also involved in this task and seen in the following example:

// Ralf's example is a Peano number where each number down the chain get sthe same
// treatment when you only want to do it at the top level.

Examples:

UPDATE: Although the solution shows how easy the problem was and how perfect stratego is for solving the problem the guys agree I was not completely stupid getting there the long way. Go the last step and get rid of justtop!!!

Incorrect success/failure handling [Laemmel09].

todo - how is this different from Incorrect polymophic default_. ?

Poor performance

Mentioned in the conclusion of [Laemmel09].

UPDATE: I think this is the same as incorrect quantification.

References

 [Mamet11] (1, 2, 3, 4) http://dl.acm.org/citation.cfm?id=1988786
 [Laemmel09] (1, 2, 3, 4, 5, 6, 7, 8, 9) http://dx.doi.org/10.1016/j.entcs.2009.09.045

UPDATE: find the scp version of this.

Updated