DavidWhitten: Created page with " MELD features = Appendix C: BNF Grammar for MELD = This BNF can be used to check for syntactic well-formedness of a MELD formula, and -- coupled..."

2019-09-30T18:27:36Z

Created page with "<noinclude> MELD features </noinclude> = Appendix C: BNF Grammar for MELD = This BNF can be used to check for syntactic well-formedness of a MELD formula, and -- coupled..."

New page

<noinclude> [[MELD features]] </noinclude>
= Appendix C: BNF Grammar for MELD =

This BNF can be used to check for syntactic well-formedness of a MELD formula, and -- coupled with the 650 formulas above in Appendix A, -- to check a MELD formula for semantic well-formedness as well.

Assume the following Terminals (token-level non-terminals)
<pre>
<Character>
<String>
<Number>
<Symbol>
<Variable>

Assume the following MELD data object:

<Constant>

The empty expansion is:

<epsilon>

;;;;;;;;;;;;;;;;;;;;;;;;
;; Syntactic Constraints
;;;;;;;;;;;;;;;;;;;;;;;;

<Formula> ::= #$True
| #$False
| <Variable>
| <Literal>
| <NotForm>
| <AndForm>
| <OrForm>
| <XorForm>
| <ImpForm>
| <EquivForm>
| <UnivForm>
| <ExistForm>
| <ExistExactForm>
| <ExistUBoundForm>
| <ExistLBoundForm>

<Formula-Seq> ::= <Formula> <Formula-Seq>
| . <Variable>
| <epsilon>

<NotForm> ::= ( #$not <Formula> )

<AndForm> ::= ( #$and <Formula-Seq> )

<OrForm> ::= ( #$or <Formula-Seq> )

<XorForm> ::= ( #$xor <Formula> <Formula> )

<ImpForm> ::= ( #$implies <Formula> <Formula> )

<EquivForm> ::= ( #$equivalent <Formula> <Formula> )

<UnivForm> ::= ( #$forAll <Variable> <Formula> )

<ExistForm> ::= ( #$thereExists <Variable> <Formula> )

<ExistExactForm> ::= ( #$thereExistExactly <1stOrderTerm> <Variable> <Formula> )

<ExistUBoundForm> ::= ( #$thereExistAtMost <1stOrderTerm> <Variable> <Formula> )

<ExistLBoundForm> ::= ( #$thereExistAtLeast <1stOrderTerm> <Variable> <Formula> )

<Literal> ::= <AtomicFormula>
| ( #$not <AtomicFormula> )

<AtomicFormula> ::= ( <Predicate> <Argument-Seq> )

<Argument-Seq> ::= <2ndOrderTerm> <Argument-Seq>
| . <Variable>
| <epsilon>

<Predicate> ::= <Rep1stOrderTerm>

<FunctionExp> ::= ( <Function> <Argument-Seq> )

<Function> ::= <Rep1stOrderTerm>

<2ndOrderTerm> ::= <1stOrderTerm>
| <Formula>

<1stOrderTerm> ::= <Rep1stOrderTerm>
| <PrimitiveTerm>

<Rep1stOrderTerm> ::= <Constant>
| <FunctionExp>
| <Variable>

<PrimitiveTerm> ::= <Character>
| <String>
| <Number>
| <Symbol>
| <Variable>

;;;;;;;;;;;;;;;;;;;;;;;
;; Semantic Constraints
;;;;;;;;;;;;;;;;;;;;;;;

For <ExistExactForm> :

1st arg must denote a positive integer

For <ExistUBoundForm> :

1st arg must denote a positive integer

For <ExistLBoundForm> :

1st arg must denote a positive integer

For <Function> :

when <Function> is ground
(#$isa <Function> #$NonPredicateFunction) must be true

For <Predicate> :
when <Predicate> is ground
(#$isa <Predicate> #$Predicate) must be true

Relation Arity Constraints:

For <FunctionExp> :
when <Function> is ground
either
(#$isa <Function> #$VariableArityRelation)
or
(#$arity <Function> <N>)
and
<N> is a non-negative integer
and
if <Argument-Seq> is terminated by . <Variable>
the number of <2ndOrderTerm>s in <Argument-Seq>
must be less than or equal to <N>
else the number of <2ndOrderTerm>s in <Argument-Seq>
must be equal to <N>

For <AtomicFormula> :

when <Predicate> is ground
either
(#$isa <Predicate> #$VariableArityRelation)

or
(#$arity <Predicate> <N>)
and
<N> is a non-negative integer
and
if <Argument-Seq> is terminated by . <Variable>
the number of <2ndOrderTerm>s in <Argument-Seq>
must be less than or equal to <N>
else the number of <2ndOrderTerm>s in <Argument-Seq>
must be equal to <N>

Relation Argument Constraints:

For <FunctionExp> :

each term in <Argument-Seq> must satisfy all applicable arg constraints
(e.g., #$arg1Isa, #$interArgIsa2-1, ...)

or <AtomicFormula> :

each term in <Argument-Seq> must satisfy all applicable arg constraints
(e.g., #$arg1Isa, #$interArgIsa2-1, ...)
</pre>

MELD features/Appendix C/0 - Revision history

DavidWhitten: Created page with " MELD features = Appendix C: BNF Grammar for MELD = This BNF can be used to check for syntactic well-formedness of a MELD formula, and -- coupled..."