Extending Newton with conditionals

[angelospl]

Newton’s current implementation does not give the opportunity for the user , neither to choose between different process models (invariants) ,when describing a physical system, nor to create constraints with different branches, based on a condition. We believe that conditional branches for constraints are very common when modeling physical systems and therefore should be available for the user. Even though we observed the lack of conditionals as a problem in the estimator backend, we believe that their addition would make the language more expressive , easy-to-use and appealing for all its users. Therefore, we propose the extension of Newton to support a form of conditional branching for constraints as well as the merging of different invariants in one. Below we present the proposed grammar and some thoughts on open issues of this extension. For more information one can refer to the newton-condtional-extension repository.

The proposed grammar for this extension :

constraint ::= ["case" condition | "otherwise" ] "->" '{' constraint-list '}' 
           |   ["case" condition | "otherwise" ] "->"  invariant-invocation

Example usage of the proposed syntax :

process_name : invariant (args, ...) = 
{
        case condition1 -> process1(args1, ...),
        case condition2 -> process2(args2, ...),
        case condition3 -> 
        {
                constraint-list
        }
        otherwise -> process3(args3, ...),
        rest of constraints
}

Open Issues:

A. Condition Syntax. One issue that will arise is how we can define the condition term, since the language’s constraints are already a form of condition. We think that using the "case" keyword could help the compiler differentiate the condition from the constraint.

B. Floating point equality operator. Another issue would be with the equality operator "==". Since we are working with real world applications the absolute equality for floating-point values is not something that is achieved easily. However, Newton’s user should be able to write the "==" operator without thinking the implications for the implementation.The equality is a valid mathematics construct and we assume that our users should use the mathematics notation. Therefore, Newton should have a way of creating C conditions statements that account for the double equality problem and not transfer this problem to the end user.

C. Invariants. Finally, another possible problem that could arise is how the compiler could differentiate between the invariant "dec- laration" and "invocation" and whether there should be a syntactic distinction between those two.

[KomaGR]

A. Condition Syntax. One issue that will arise is how we can define the condition term, since the language’s constraints are already a form of condition. We think that using the "case" keyword could help the compiler differentiate the condition from the constraint.

I think this is an important observation. After reading @angelospl's write-up, it occurred to me that it could make sense to view this proposed extension as syntactic sugar that transforms to invariants. For example consider the following case from the the first comment of the issue:

process_name : invariant (args, ...) = 
{
        case condition1 -> process1(args1, ...),
        case condition2 -> process2(args2, ...),
        [...]
}

This invariant with the case expression can be thought as equivalent to the following set of invariants and transformed to it during the compilation phase.

cond1_invariant : invariant (args) =
{
        condition1,
        process1(args1, ...)
}

cond2_invariant : invariant (args) =
{
        condition2,
        process2(args2, ...)
}

process_name : invariant (args, ...) = 
{
        cond1_invariant(args),
        cond2_invariant(args),
        [...]
}

B. [...] However, Newton’s user should be able to write the "==" operator without thinking the implications for the implementation. [...]

I agree.

C. Invariants. Finally, another possible problem that could arise is how the compiler could differentiate between the invariant "declaration" and "invocation" and whether there should be a syntactic distinction between those two.

Could you explain this a bit more? An invariant declaration requires the invariant keyword, the = character, and a constraint list. The invocation does not have these so I'd think that you can differentiate them based on these.

[phillipstanleymarbell]

Regarding referring to invariants from within other invariants, also see #329 and #39.

[phillipstanleymarbell]

Regarding the conditional syntax, I recommend the following alternative:

piecewiseConstraint ::= "piecewise" "{" caseList "}" .
caseList        ::= "case" constraint "->" "{" constraintList "}" .

and modify the constraint production to include piecewiseConstraint, i.e.,

constraint      ::= quantityExpression comparisonOp quantityExpression
                | identifier parameterTuple
                | piecewiseConstraint .

The constraint production in the grammar already contains identifier parameterTuple which is the grammar to accept a reference to an existing invariant as a constraint.

[angelospl]

I have started by implementing the constraint ::= identifier parameterTuple production. However, since the parameterTuple syntax also contains the type declarations of the parameters, I have tweaked the grammar. More specifically, the new grammar is :

constraint        ::= quantityExpression comparisonOp quantityExpression
                    | identifier callParameterTuple

callParameterTuple        ::= "(" identifier { "," identifier } ")"

Next , I will add semantic check for the types and names of the identifiers as well as for the name of the invariant.

[KomaGR]

Using the parameterTuple production doesn't necessarily mean providing types. The parameterTuple rule simply requires an identifier or an expression, so it could be like named parameters. That's how I thought about it when writing the signalUncertaintyStatement.

At the end of the day, I do agree that maybe we should keep the typing syntax separate.

[angelospl]

Currently, the syntax and the semantic checking for the "invariant call" production seems to work. I also started implementing the case syntax. I am presenting below the updated syntax used in the newton.ffi file.

constraint ::= quantityExpression comparisonOp quantityExpression
             | identifier callParameterTuple
             | piecewiseConstraint .

callParameterTuple ::= "(" identifier { "," identifier } ")" .

piecewiseConstraint ::= "piecewise" "{" caseStatementList "}" .

caseStatementList ::= caseStatement {"," caseStatement} .

caseStatement ::= ("case" constraint | "otherwise") "->"  "{" constraintList "}" .

The changes for the parameterCallTuple were explained before. I also added the caseStatementList production so we can have multiple case statements in a piecewise constraint and finally I added the "otherwise" keyword so we can cover all different cases without having to manually write them.

Regarding Orestis' idea about named parameters it is not currently implemented. However, we could add it at a later point, since it is a nice addition.