DavidWhitten at 18:30, 30 September 2019

2019-09-30T18:30:21Z

DavidWhitten: Replaced content with "Do you mean: MELD features/Appendix C ?"

2019-09-30T18:27:02Z

Replaced content with "Do you mean: MELD features/Appendix C ?"

Show changes

DavidWhitten: /* Appendix C: BNF Grammar for MELD */

2019-09-30T17:18:49Z

‎Appendix C: BNF Grammar for MELD

DavidWhitten at 17:15, 30 September 2019

2019-09-30T17:15:35Z

DavidWhitten: Created page with "== 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..."

2019-09-30T17:14:49Z

Created page with "== 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..."

New page

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

← Older revision		Revision as of 18:30, 30 September 2019
Line 1:		Line 1:
	Do you mean: [[MELD features/Appendix C]] ?		Do you mean: [[MELD features/Appendix C]] ?
		+	Or the top level page: [[MELD features]] ?

← Older revision		Revision as of 17:15, 30 September 2019
Line 1:		Line 1:
		+	<noinclude> [[MELD features]] </noinclude>
	== Appendix C: BNF Grammar for MELD ==		== Appendix C: BNF Grammar for MELD ==

@@ Line 1: / Line 1: @@
 <noinclude> [[MELD features]] </noinclude>
-== Appendix C: BNF Grammar for MELD ==
+= 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.

Template:MELD features/Appendix C - Revision history

DavidWhitten at 18:30, 30 September 2019

DavidWhitten: Replaced content with "Do you mean: MELD features/Appendix C ?"

DavidWhitten: /* Appendix C: BNF Grammar for MELD */

DavidWhitten at 17:15, 30 September 2019

DavidWhitten: Created page with "== 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..."