MELD features/Appendix C/0

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 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)

 <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, ...)