		Search-engine friendly clone of the ACL2 documentation.

Semantics

Languagep

Notion of language.

The language defined by a list of rules consists of the sequences of natural numbers that form parsable strings for given rule names. An ABNF grammar does not include any explicit axiom (or start symbol); thus, the top-level symbols of interest (one or more) are specified as an additional parameter of this predicate.

Note that the condition that the existentially quantified rulename be defined by rules would be superfluous, because if rulename is not defined then no parse trees with only terminal leaves can originate from it.

Definitions and Theorems

Theorem: languagep-suff

(defthm languagep-suff
  (implies (and (nat-listp nats)
                (in rulename rulenames)
                (string-parsablep nats rulename rules))
           (languagep nats rulenames rules)))

Theorem: booleanp-of-languagep

(defthm booleanp-of-languagep
  (b* ((yes/no (languagep nats rulenames rules)))
    (booleanp yes/no))
  :rule-classes :rewrite)