ForTheL’s TEX dialect
Marcel Schütz
December 2022
Contents
1 Conventions
This syntax reference is written in NBNF, an extension of BNF, where the following conventions are adopted.
| Pattern | Meaning |
|---|---|
pattern₁ | pattern₂ | … | patternₙ |
Choice |
[ pattern ] |
Option |
( pattern ) |
Grouping |
{ pattern } |
Zero or more repetitions |
pattern₁ pattern₂ … patternₙ |
Concatenation |
"string" |
Case-sensitive string |
'string' |
Case-insensitive string |
⟨identifier⟩ |
Non-terminal |
⟪identifier⟫ |
Alphabet (see below) |
⟪identifier⟫ \ (expr₁, …, exprₙ) |
A character (i.e. single-character string) that matches the alphabet ⟪identifier⟫, but none of the expressions expr₁, …, exprₙ which can either be case-sensitive or case-insensitive characters. |
⟪identifier⟫* \ (expr₁, …, exprₙ) |
All words over the alphabet ⟪identifier⟫ that do not match any of the expressions expr₁, …, exprₙ which can either be case-sensitive or case-insensitive strings. |
⟪identifier⟫+ \ (expr₁, …, exprₙ) |
All non-empty words over the alphabet ⟪identifier⟫ that do not match any of the expressions expr₁, …, exprₙ which can either be case-sensitive or case-insensitive strings. |
An alphabet is a non-terminal, where the right-hand side of its definition must consist of an expression of the form expr₁ | expr₂ | … | exprₙ, where exprₙ, …, exprₙ can be single case-sensitive characters or so-called character lists, i.e. expressions of the form "char₁" | ... | "char₂" (here the ... are part of the syntax), where char₁ and char₂ are arbitrary characters. Such a character list accepts all characters in the Unicode table from the code point of char₁ to the code point of char₂.
To avoid parentheses, we assume that choice has a lower precedence than concatenation.
Within a string the following characters have to be escaped by prepending a backslash to them: \, ", '. Any special characters can be represented by the pattern \U+XXXX;, where XXXX is its hexadecimal Unicode code point.
Moreover, identifiers of non-terminals and alphabets are only allowed to contain the letters “a” - “z”, “A” - “Z”, the digits “0” - “9”, spaces and the characters “-” and “_“.
2 TEX extraction
This chapter describes a specification of an “extractor” which extracts the content of forthel environments from a TEX document, i.e. everything enclosed within the tags \begin{forthel} and \begin{forthel}. This means a parser for the grammar described in this chapter is intended to accept any arbitrary string of characters from Unicode’s Basic Latin code block and returns the content of all forthel environments it contains.
| ⟨tex document⟩ | = | [ ⟨ignored text⟩ ] { “\\begin{forthel}” ⟨tex text⟩ “\\end{forthel}” [ ⟨ignored text⟩ ] } |
Text before any occurence of the string \begin{forthel} is intended to be ignored by a ForTheL compiler. Hence it can be arbitrary text not containing \begin{forthel} as a substring.
| ⟨ignored text⟩ | = | ““ |
| | | ⟪Latin⟫ \ {“\\”} ⟨ignored text⟩ | |
| | | “\\” ⟪Latin⟫ \ {“\\”} ⟨ignored text⟩ | |
| | | “\\\\” ⟪Latin⟫ \ {“b”} ⟨ignored text⟩ | |
| | | “\\\\b” ⟪Latin⟫ \ {“e”} ⟨ignored text⟩ | |
| | | “\\\\be” ⟪Latin⟫ \ {“g”} ⟨ignored text⟩ | |
| | | “\\\\beg” ⟪Latin⟫ \ {“i”} ⟨ignored text⟩ | |
| | | “\\\\begi” ⟪Latin⟫ \ {“n”} ⟨ignored text⟩ | |
| | | “\\\\begin” ⟪Latin⟫ \ {“{”} ⟨ignored text⟩ | |
| | | “\\\\begin{” ⟪Latin⟫ \ {“f”} ⟨ignored text⟩ | |
| | | “\\\\begin{f” ⟪Latin⟫ \ {“o”} ⟨ignored text⟩ | |
| | | “\\\\begin{fo” ⟪Latin⟫ \ {“r”} ⟨ignored text⟩ | |
| | | “\\\\begin{for” ⟪Latin⟫ \ {“t”} ⟨ignored text⟩ | |
| | | “\\\\begin{fort” ⟪Latin⟫ \ {“h”} ⟨ignored text⟩ | |
| | | “\\\\begin{forth” ⟪Latin⟫ \ {“e”} ⟨ignored text⟩ | |
| | | “\\\\begin{forthe” ⟪Latin⟫ \ {“l”} ⟨ignored text⟩ | |
| | | “\\\\begin{forthel” ⟪Latin⟫ \ {“}”} ⟨ignored text⟩ |
A ForTheL text is an arbitrary text which does not contain the string \end{forthel}:
| ⟨forthel text⟩ | = | ““ |
| | | ⟪Latin⟫ \ {“\\”} ⟨forthel text⟩ | |
| | | “\\” ⟪Latin⟫ \ {“\\”} ⟨forthel text⟩ | |
| | | “\\\\” ⟪Latin⟫ \ {“e”} ⟨forthel text⟩ | |
| | | “\\\\e” ⟪Latin⟫ \ {“n”} ⟨forthel text⟩ | |
| | | “\\\\en” ⟪Latin⟫ \ {“d”} ⟨forthel text⟩ | |
| | | “\\\\end” ⟪Latin⟫ \ {“{”} ⟨forthel text⟩ | |
| | | “\\\\end{” ⟪Latin⟫ \ {“f”} ⟨forthel text⟩ | |
| | | “\\\\end{f” ⟪Latin⟫ \ {“o”} ⟨forthel text⟩ | |
| | | “\\\\end{fo” ⟪Latin⟫ \ {“r”} ⟨forthel text⟩ | |
| | | “\\\\end{for” ⟪Latin⟫ \ {“t”} ⟨forthel text⟩ | |
| | | “\\\\end{fort” ⟪Latin⟫ \ {“h”} ⟨forthel text⟩ | |
| | | “\\\\end{forth” ⟪Latin⟫ \ {“e”} ⟨forthel text⟩ | |
| | | “\\\\end{forthe” ⟪Latin⟫ \ {“l”} ⟨forthel text⟩ | |
| | | “\\\\end{forthel” ⟪Latin⟫ \ {“}”} ⟨forthel text⟩ |
| ⟪Latin⟫ | = | “\U+0009;” | … | “\U+000D;” |
| | | “\U+0020;” | … | “~” |
3 TEX lexing
This chapter describes a specification of a lexer for the content of forthel environments within a TEX document. This means a parser for the grammar described in this chapter is intended to accept any arbitrary string of characters from Unicode’s Basic Latin code block and split it into TEX lexemes. (Note that we use the word token as a synonym for lexeme in the following to match the usage of the word token in the referenced literature.)
| ⟨tex tokens⟩ | = | { ⟨alphanumeric token⟩ | ⟨symbolic token⟩ | ⟨backslashed token⟩ | ⟨white token⟩ } |
3.1 Tokens
| ⟨white token⟩ | = | ⟪Horizontal space⟫ |
| | | ⟪Vertical space⟫ | |
| | | “$” | |
| | | “\\\\” | |
| | | “\\[” | |
| | | “\\]” | |
| | | “\\left” | |
| | | “\\middle” | |
| | | “\\right” | |
| | | ⟨comment⟩ |
| ⟨comment⟩ | = | “%” { ⟪Visible Character⟫ | ⟪Horizontal Space⟫ } ⟪Vertical Space⟫ |
| ⟨alphanumeric token⟩ | = | ⟪Alphanum⟫ { ⟪Alphanum⟫ } |
| ⟨symbolic token⟩ | = | ⟪Symbol⟫ \ {“%”, “\\”} |
| ⟨backslashed token⟩ | = | “\\” ( ⟪Alphanum⟫+ \ {“left”, “middle”, “right”} | ⟪Symbol⟫ \ {“\\”, “[”, “]”} ) |
The following rules are only needed to specify certain special tokens in the next paragraphs.
3.2 Special symbols
| ⟨greek letter⟩ | = | ⟨lower greek letter⟩ |
| | | ⟨upper greek letter⟩ | |
| | | ⟨varied greek letter⟩ |
| ⟨lower greek letter⟩ | = | “\\alpha” |
| | | “\\beta” | |
| | | “\\gamma” | |
| | | “\\delta” | |
| | | “\\epsilon” | |
| | | “\\zeta” | |
| | | “\\eta” | |
| | | “\\theta” | |
| | | “\\iota” | |
| | | “\\kappa” | |
| | | “\\lambda” | |
| | | “\\mu” | |
| | | “\\nu” | |
| | | “\\xi” | |
| | | “\\pi” | |
| | | “\\rho” | |
| | | “\\sigma” | |
| | | “\\tau” | |
| | | “\\upsilon” | |
| | | “\\phi” | |
| | | “\\omicron” | |
| | | “\\chi” | |
| | | “\\psi” | |
| | | “\\omega” |
| ⟨upper greek letter⟩ | = | “\\Gamma” |
| | | “\\Delta” | |
| | | “\\Theta” | |
| | | “\\Lambda” | |
| | | “\\Xi” | |
| | | “\\Pi” | |
| | | “\\Sigma” | |
| | | “\\Upsilon” | |
| | | “\\Phi” | |
| | | “\\Psi” | |
| | | “\\Omega” |
| ⟨varied greek letter⟩ | = | “\\varbeta” |
| | | “\\varepsilon” | |
| | | “\\vartheta” | |
| | | “\\varkappa” | |
| | | “\\varpi” | |
| | | “\\varvarpi” | |
| | | “\\varrho” | |
| | | “\\varvarrho” | |
| | | “\\varsigma” | |
| | | “\\varphi” |
| ⟨argument symbol⟩ | = | ⟨alphanumeric character⟩ |
| | | ⟪Symbol⟫ \ {“%”, “]”} |
3.3 Special tokens
| ⟨regular token⟩ | = | ⟨regular alphanumeric token⟩ |
| | | ⟨regular symbolic token⟩ |
| ⟨regular alphabetic token⟩ | = | ⟪Letter⟫+ \ {‘the’, ‘a’, ‘an’, ‘is’, ‘are’, ‘be’} |
| ⟨regular alphanumeric token⟩ | = | ⟪Alphanum⟫+ \ {‘the’, ‘a’, ‘an’, ‘is’, ‘are’, ‘be’} |
| ⟨regular symbolic token⟩ | = | ⟪Symbol⟫ \ {“%”, “.”} |
| ⟨label token⟩ | = | ⟨alphanumeric token⟩ |
| | | “_“ |
| ⟨variable token⟩ | = | ⟪Letter⟫ { ⟪Alphanum⟫ } |
| ⟨var token⟩ | = | ⟨alphabetic token⟩ |
| ⟨argument token⟩ | = | ⟨alphanumeric token⟩ |
| | | ⟪Symbol⟫ \ {“%”, “]”} |
| ⟨environment name token⟩ | = | ⟨alphanumeric token⟩ |
| | | ⟪Symbol⟫ \ {“%”, “]”} |
3.4 Alphabets
| ⟪Alphanum⟫ | = | “0” | … | “9” |
| | | “A” | … | “Z” | |
| | | “a” | … | “z” |
| ⟪Letter⟫ | = | “A” | … | “Z” |
| | | “a” | … | “z” |
| ⟪Digit⟫ | = | “0” | … | “9” |
| ⟪Symbol⟫ | = | “!” | … | “/” |
| | | “:” | … | “@” | |
| | | “[” | … | “`” | |
| | | “{” | … | “~” |
Horizontal tab or space:
| ⟪Horizontal Space⟫ | = | “\U+0009;” |
| | | “\U+0020;” |
Line feed, vertical tab, form feed or chrriage return:
| ⟪Vertical Space⟫ | = | “\U+000A;” |
| | | “\U+000B;” | |
| | | “\U+000C;” | |
| | | “\U+000D;” |
| ⟪Visible Character⟫ | = | “!” | … | “~” |
4 TEX parsing
This chapter describes a specification of a parser for lexed TEX documents. This means a parser for the grammar described in this chapter is intended to accept a list of lexemes generated by a parser for the grammar described in the previous chapter and returns for instance an abstract syntax tree for such an FTL-TeX document.
| ⟨tex text⟩ | = | { ⟨forthel section⟩ } |
| ⟨forthel section⟩ | = | ⟨instruction⟩ |
| | | ⟨declaration⟩ | |
| | | ⟨top-level section⟩ |
4.1 Special strings
4.1.1 Labels
| ⟨label⟩ | = | ⟨label token⟩ { ⟨label token⟩ } |
| ⟨name⟩ | = | “(” ⟨label⟩ “)” |
The following rule is adopted from [2].
| ⟨variables⟩ | = | ⟨variable⟩ { “,” ⟨variable⟩ } |
| ⟨variable⟩ | = | ( ⟨variable token⟩ | ⟨greek letter⟩ ) { “\’” } |
| ⟨var⟩ | = | ⟨var token⟩ |
| | | ⟨greek letter⟩ |
| ⟨qed⟩ | = | ( ‘qed’ | ‘end’ | ‘obvious’ | ‘trivial’ ) [ ⟨reference⟩ ] “.” |
4.2 Keywords
| ⟨assume⟩ | = | ‘assume’ |
| | | ‘presume’ | |
| | | ‘suppose’ |
| ⟨iff⟩ | = | ‘iff’ |
| | | ‘if’ ‘and’ ‘only’ ‘if’ | |
| | | ‘when’ ‘and’ ‘only’ ‘when’ |
| ⟨is⟩ | = | ‘is’ |
| | | ‘are’ | |
| | | ‘be’ |
| ⟨does⟩ | = | ‘does’ |
| | | ‘do’ |
| ⟨has⟩ | = | ‘has’ |
| | | ‘have’ |
| ⟨with⟩ | = | ‘with’ |
| | | ‘of’ | |
| | | ‘having’ |
| ⟨let us⟩ | = | ‘let’ ‘us’ |
| | | ‘we’ ‘can’ |
| ⟨stand for⟩ | = | ‘stand’ ‘for’ |
| | | ‘denote’ |
| ⟨then⟩ | = | ‘then’ |
| | | ‘hence’ | |
| | | ‘thus’ | |
| | | ‘therefore’ | |
| | | ‘consequently’ |
| ⟨article⟩ | = | ⟨indefinite article⟩ |
| | | ⟨definite article⟩ |
| ⟨indefinite article⟩ | = | ‘a’ |
| | | ‘an’ |
| ⟨definite article⟩ | = | ‘the’ |
4.3 Instructions
| ⟨instruction⟩ | = | “[” ⟨instr⟩ “]” |
| ⟨instr⟩ | = | ⟨command instruction⟩ |
| | | ⟨limit instruction⟩ | |
| | | ⟨flag instruction⟩ | |
| | | ⟨argument instruction⟩ | |
| | | ⟨synonym instruction⟩ | |
| | | ⟨drop instruction⟩ |
4.3.1 Command instructions
| ⟨command instr⟩ | = | “exit” |
| | | “quit” | |
| | | “thesis” | |
| | | “context” | |
| | | “filter” | |
| | | “rules” |
4.3.2 Limit instructions
| ⟨limit instruction⟩ | = | ⟨limit instr⟩ ⟨limit⟩ |
| ⟨limit instr⟩ | = | “timelimit” |
| | | “memorylimit” | |
| | | “depthlimit” | |
| | | “checktime” | |
| | | “checkdepth” |
| ⟨limit⟩ | = | ⟨numeric token⟩ |
4.3.3 Flag instructions
| ⟨flag instruction⟩ | = | ⟨flag instr⟩ ⟨bool⟩ |
| ⟨flag instr⟩ | = | “prove” |
| | | “check” | |
| | | “checkconsistency” | |
| | | “symsign” | |
| | | “info” | |
| | | “thesis” | |
| | | “filter” | |
| | | “skipfail” | |
| | | “flat” | |
| | | “printgoal” | |
| | | “printsection” | |
| | | “printcheck” | |
| | | “printunfold” | |
| | | “printreason” | |
| | | “printprover” | |
| | | “printfulltask” | |
| | | “dump” | |
| | | “printsimp” | |
| | | “printthesis” | |
| | | “unfold” | |
| | | “unfoldsf” | |
| | | “unfoldlow” | |
| | | “unfoldlowsf” | |
| | | “translation” | |
| | | “tex” |
| ⟨bool⟩ | = | “yes” |
| | | “no” | |
| | | “on” | |
| | | “off” |
4.3.4 Argument instructions
| ⟨argument instruction⟩ | = | ⟨argument instr⟩ ( “\\path” “{” ⟨argument⟩ “}” | ⟨argument⟩ ) |
| ⟨argument instr⟩ | = | “read” |
| | | “readtex” | |
| | | “library” | |
| | | “provers” | |
| | | “prover” |
| ⟨argument⟩ | = | ⟨argument token⟩ { ⟨argument token⟩ } |
4.3.5 Synonym instructions
| ⟨synonym instruction⟩ | = | “synonym” ⟨regular alphabetic token⟩ { “/” [ “-” ] ⟨regular alphabetic token⟩ } |
4.3.6 Drop instructions
| ⟨drop instruction⟩ | = | “/” ( ⟨command instr⟩ | ⟨limit instr⟩ | ⟨flag instr⟩ ) |
4.4 Declarations
| ⟨declaration⟩ | = | ⟨variable declaration⟩ |
| | | ⟨notion declaration⟩ | |
| | | ⟨function declaration⟩ | |
| | | ⟨predicate declaration⟩ |
| ⟨variable declaration⟩ | = | ‘let’ ⟨variables⟩ ⟨stand for⟩ [ ⟨article⟩ ] ⟨class noun⟩ “.” |
| ⟨notion declaration⟩ | = | ‘let’ ⟨notion pattern⟩ ⟨stand for⟩ [ ⟨article⟩ ] ⟨class noun⟩ “.” |
| ⟨function declaration⟩ | = | ‘let’ ⟨function pattern⟩ ⟨stand for⟩ ⟨plain term⟩ “.” |
| ⟨predicate declaration⟩ | = | ‘let’ ⟨predicate pattern⟩ ⟨stand for⟩ ⟨statement⟩ “.” |
4.5 Patterns
4.5.1 Notion, function and predicate patterns
| ⟨notion pattern⟩ | = | ⟨indefinite article⟩ ⟨alphanumeric pattern⟩ |
The usage of ⟨indefinite article⟩ is necessary to tell a variable from a notion pattern and hence a type declaration from a notion declaration.
| ⟨function pattern⟩ | = | ⟨definite article⟩ ⟨alphanumeric pattern⟩ |
| | | ⟨pattern⟩ |
| ⟨predicate pattern⟩ | = | ⟨var⟩ ⟨is⟩ ⟨alphanumeric pattern⟩ |
| | | ⟨var⟩ ⟨alphanumeric pattern⟩ | |
| | | ⟨pattern⟩ |
4.5.2 General patterns
| ⟨alphabetic pattern⟩ | = | ⟨regular alphabetic token⟩ { ⟨regular alphabetic token⟩ } |
| ⟨alphanumeric pattern⟩ | = | ⟨regular alphanumeric token⟩ { ⟨regular alphanumeric token⟩ } |
| ⟨symbolic pattern⟩ | = | ⟨regular symbolic token⟩ { ⟨regular symbolic token⟩ } |
| ⟨pattern⟩ | = | ⟨regular token⟩ { ⟨regular token⟩ } |
Note that we ignore variables in the definition of (symbolic) patterns since on a syntactic level they cannot be distinguished from other tokens.
4.6 Top-level sections
| ⟨top-level section⟩ | = | ⟨axiom⟩ |
| | | ⟨definition⟩ | |
| | | ⟨signature extension⟩ | |
| | | ⟨theorem⟩ [ ⟨top-level proof⟩ ] |
| ⟨environment label⟩ | = | “[” [ ⟨label⟩ ] “]” |
| | | [ “[” ⟨environment name token⟩ { ⟨environment name token⟩ } “]” ] ( “\\label” | “\\printlabel” ) “{” ⟨label⟩ “}” |
4.6.1 Axioms
| ⟨axiom⟩ | = | “\\begin” “{” “axiom” “}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨axiom affirmation⟩ “\\end” “{” “axiom” “}” |
| | | “\\begin” “{” “axiom” “” ”}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨axiom affirmation⟩ ”\\end” ”{” ”axiom” ”” “}” |
| ⟨axiom affirmation⟩ | = | [ ⟨then⟩ ] ⟨statement⟩ “.” |
4.6.2 Definitions
| ⟨definition⟩ | = | “\\begin” “{” “definition” “}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨definition affirmation⟩ “\\end” “{” “definition” “}” |
| | | “\\begin” “{” “definition” “” ”}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨definition affirmation⟩ ”\\end” ”{” ”definition” ”” “}” |
The following rule is adopted from [2].
| ⟨definition affirmation⟩ | = | ⟨definition statement⟩ “.” |
4.6.3 Signature extensions
| ⟨signature extension⟩ | = | “\\begin” “{” “signature” “}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨signature affirmation⟩ “\\end” “{” “signature” “}” |
| | | “\\begin” “{” “signature” “” ”}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨signature affirmation⟩ ”\\end” ”{” ”signature” ”” “}” |
The following rule is adopted from [2].
| ⟨signature affirmation⟩ | = | ⟨signature statement⟩ “.” |
4.6.4 Theorems
| ⟨theorem⟩ | = | “\\begin” “{” “theorem” “}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ “\\end” “{” “theorem” “}” |
| | | “\\begin” “{” “theorem” “” ”}” [ ⟨environment label⟩ ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ ”\\end” ”{” ”theorem” ”” “}” | |
| | | “\\begin” “{” “proposition” “}” [ “[” [ ⟨label⟩ ] “]” ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ “\\end” “{” “proposition” “}” | |
| | | “\\begin” “{” “proposition” “” ”}” [ ”[” [ ⟨label⟩ ] ”]” ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ ”\\end” ”{” ”proposition” ”” “}” | |
| | | “\\begin” “{” “lemma” “}” [ “[” [ ⟨label⟩ ] “]” ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ “\\end” “{” “lemma” “}” | |
| | | “\\begin” “{” “lemma” “” ”}” [ ”[” [ ⟨label⟩ ] ”]” ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ ”\\end” ”{” ”lemma” ”” “}” | |
| | | “\\begin” “{” “corollary” “}” [ “[” [ ⟨label⟩ ] “]” ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ “\\end” “{” “corollary” “}” | |
| | | “\\begin” “{” “corollary” “” ”}” [ ”[” [ ⟨label⟩ ] ”]” ] { ⟨assumption⟩ } ⟨theorem affirmation⟩ ”\\end” ”{” ”corollary” ”” “}” |
| ⟨theorem affirmation⟩ | = | [ ⟨then⟩ ] ⟨statement⟩ [ ⟨reference⟩ ] “.” |
4.7 Assumptions
| ⟨assumption⟩ | = | [ ⟨name⟩ ] ⟨assumption prefix⟩ ⟨statement⟩ “.” |
The following rule is adopted from [2].
4.8 Definition and notion statements
4.8.1 Definition statements
The following rule is adopted from [2].
| ⟨definition statement⟩ | = | ⟨notion definition⟩ |
| | | ⟨function definition⟩ | |
| | | ⟨predicate definition⟩ |
| ⟨notion definition⟩ | = | ⟨notion head⟩ ( “=” | ⟨is⟩ [ ‘equal’ ‘to’ ] ) [ ⟨article⟩ ] ⟨class noun⟩ |
| ⟨function definition⟩ | = | ⟨function head⟩ ( “=” | ⟨is⟩ [ ‘equal’ ‘to’ ] ) [ ⟨article⟩ ] ( ⟨class noun⟩ | ⟨plain term⟩ ) |
| ⟨predicate definition⟩ | = | ⟨predicate head⟩ ( ⟨iff⟩ | “<” “=” “>” | “\\iff” ) ⟨statement⟩ |
4.8.2 Signature statements
The following rule is adopted from [2].
| ⟨signature statement⟩ | = | ⟨notion signature⟩ |
| | | ⟨function signature⟩ | |
| | | ⟨predicate signature⟩ |
| ⟨notion signature⟩ | = | ⟨notion head⟩ ⟨is⟩ [ ⟨article⟩ ] ( ⟨class noun⟩ | ‘notion’ | ‘constant’ ) |
| ⟨function signature⟩ | = | ⟨function head⟩ ⟨is⟩ [ ⟨article⟩ ] ⟨class noun⟩ |
| ⟨predicate signature⟩ | = | ⟨predicate head⟩ ( ‘implies’ | ‘is’ | “=” “>” | “\\implies” ) ⟨statement⟩ |
| | | ⟨predicate head⟩ ‘is’ [ ⟨article⟩ ] ( ‘atom’ | ‘relation’ ) |
Note that in contrast to the rules before, ⟨predicate signature⟩ requires an 'is' instead of an ⟨is⟩.
4.8.3 Notion, function and predicate heads
The rules in this paragraph are adopted from [2].
| ⟨notion head⟩ | = | ⟨article⟩ ⟨primitive class noun⟩ |
| | | ⟨notion pattern⟩ |
| ⟨function head⟩ | = | [ ⟨definite article⟩ ] ⟨primitive definition noun⟩ |
| | | ⟨primitive infix operator⟩ | |
| | | ⟨primitive prefix operator⟩ | |
| | | ⟨primitive postfix operator⟩ | |
| | | ⟨function pattern⟩ |
4.9 Proofs
| ⟨top-level proof⟩ | = | “\\begin” “{” “proof” “}” [ “[” ‘by’ ⟨method⟩ “]” ] { ⟨proof step⟩ } “\\end” “{” “proof” “}” |
| ⟨low-level proof⟩ | = | ⟨proof head⟩ { ⟨proof step⟩ } ⟨qed⟩ |
| | | ‘indeed’ ⟨confirmation⟩ |
| ⟨proof head⟩ | = | ‘proof’ [ ‘by’ ⟨method⟩ ] “.” |
| ⟨confirmation⟩ | = | ⟨affirmation⟩ [ ⟨low-level proof⟩ ] |
| | | ⟨choose⟩ [ ⟨low-level proof⟩ ] | |
| | | ⟨low-level definition⟩ | |
| | | ⟨assumption⟩ | |
| | | ⟨low-level theorem⟩ |
Note that in contrast to ⟨proof step⟩ low-level definitions cannot be followed by a proof.
The following rule is adopted from [2].
| ⟨method⟩ | = | ‘contradiction’ |
| | | ‘case’ ‘analysis’ | |
| | | ‘induction’ [ ‘on’ ⟨plain term⟩ ] |
| ⟨proof step⟩ | = | ⟨affirmation⟩ [ ⟨low-level proof⟩ ] |
| | | ⟨choose⟩ [ ⟨low-level proof⟩ ] | |
| | | ⟨low-level definition⟩ [ ⟨low-level proof⟩ ] | |
| | | ⟨assumption⟩ | |
| | | ⟨case⟩ | |
| | | ⟨low-level theorem⟩ | |
| | | ⟨equality chain⟩ | |
| | | ⟨instruction⟩ |
| ⟨low-level theorem⟩ | = | ⟨low-level theorem head⟩ ( ⟨affirmation⟩ | ⟨equality chain⟩ ) [ ⟨proof head⟩ ] { ⟨proof step⟩ } ⟨qed⟩ |
| ⟨choose⟩ | = | [ ⟨name⟩ ] [ ⟨then⟩ ] [ ⟨let us⟩ ] ( ‘take’ | ‘choose’ | ‘consider’ ) [ ⟨article⟩ ] ⟨notions⟩ [ ⟨reference⟩ ] “.” |
| ⟨case⟩ | = | [ ⟨name⟩ ] ‘case’ ⟨statement⟩ [ ⟨reference⟩ ] “.” { ⟨proof step⟩ } ⟨qed⟩ |
| ⟨affirmation⟩ | = | [ ⟨name⟩ ] [ ⟨then⟩ ] ⟨statement⟩ [ ⟨reference⟩ ] “.” |
| ⟨equality chain⟩ | = | [ ⟨name⟩ ] ⟨symbolic term⟩ “.” “=” ⟨symbolic term⟩ [ ⟨reference⟩ ] { “.” “=” ⟨symbolic term⟩ [ ⟨reference⟩ ] } “.” |
4.10 Low-level definitions
| ⟨low-level definition⟩ | = | [ ⟨name⟩ ] ⟨class definition⟩ |
| | | [ ⟨name⟩ ] ⟨function definition⟩ |
4.10.1 Class definitions
| ⟨class definition⟩ | = | ‘define’ ⟨variable⟩ ‘=’ ( ⟨class term⟩ | ⟨class-of term⟩ ) “.” |
| ⟨class term⟩ | = | ⟨descriptive class term⟩ |
| | | ⟨enumerative class term⟩ |
| ⟨descriptive class term⟩ | = | ( “{” | “\\{” ) ( ⟨separation⟩ | ⟨separation in text-mode⟩ ) ( “|” | “:” | “\\mid” ) ( ⟨statement⟩ | ⟨statement in text-mode⟩ ) ( “}” | “\\}” ) |
| | | “\\class” “{” ( ⟨separation⟩ | ⟨separation in text-mode⟩ ) “|” ( ⟨statement⟩ | ⟨statement in text-mode⟩ | ⟨statement in classtext-mode⟩ ) “}” |
| ⟨class-of term⟩ | = | ( ‘class’ | ‘classes’ | ‘collection’ | ‘collections’ ) [ ⟨variable⟩ ] ‘of’ [ ‘all’ ] ⟨notion⟩ |
| ⟨separation⟩ | = | ⟨term⟩ |
| | | ⟨term⟩ ( ‘in’ | “\\in” ) ( ⟨term⟩ | ⟨class term⟩ | ⟨class-of term⟩ ) |
| ⟨separation in text-mode⟩ | = | “\\text” “{” ⟨separation⟩ “}” |
4.10.2 Function definitions
| ⟨function definition⟩ | = | ‘define’ ⟨variable⟩ “(” ⟨variable⟩ [ “,” ⟨variable⟩ ] “)” “=” ⟨function body⟩ ‘for’ ( ⟨variable⟩ | “(” ⟨variable⟩ “,” ⟨variable⟩ “)” ) ( ‘in’ | “\\in” ) ⟨term⟩ “.” |
| | | ‘define’ ⟨variable⟩ “=” ⟨lambda term⟩ “.” |
| ⟨function parameter⟩ | = | ⟨variable⟩ |
| | | “(” ⟨variable⟩ “,” ⟨variable⟩ “)” |
| ⟨function body⟩ | = | ⟨case function⟩ |
| | | ⟨plain function term⟩ |
| ⟨case function⟩ | = | ‘case’ ⟨statement⟩ ( “-” “>” | “\\rightarrow” ) ⟨plain function term⟩ [ “,” ⟨case function⟩ ] |
| | | “\\begin” “{” “cases” “}” ⟨case term⟩ “&” [ “:” ] ⟨case statement⟩ { ⟨case term⟩ “&” [ “:” ] ⟨case statement⟩ } “\\end” “{” “cases” “}” |
Note that linebreaks via \\ are ignored by Naproche, so you can (and should) use them to separate several cases if you use the second option of ⟨case function⟩
| ⟨case term⟩ | = | ⟨plain function term⟩ |
| ⟨case statement⟩ | = | ⟨statement⟩ |
| | | ⟨statement in text-mode⟩ |
| ⟨plain function term⟩ | = | ⟨choice term⟩ | ⟨function term⟩ |
| | | “\\text” “{” ( ⟨choice term⟩ | ⟨function term⟩ ) “}” |
| ⟨choice term⟩ | = | ⟨low-level-def choice⟩ { “,” ⟨low-level-def choice⟩ } ‘in’ ⟨function term⟩ |
| ⟨function term⟩ | = | ⟨term⟩ |
| | | ⟨lambda term⟩ | |
| | | ⟨class term⟩ | |
| | | ⟨class-of term⟩ |
| ⟨low-level-def choice⟩ | = | ‘choose’ [ ⟨article⟩ ] ⟨notion⟩ |
| | |
“"</span></span> <span class="NBNF_terminal"><span class="NBNF_case_sensitive_string">"” ‘choose’ [ ⟨article⟩ ] ⟨notion⟩ “\’” “\’”
|
|
| | | ‘define’ ⟨variable⟩ “=” ( ⟨class term⟩ | ⟨class-of term⟩ | ⟨lambda term⟩ ) | |
| | |
“"</span></span> <span class="NBNF_terminal"><span class="NBNF_case_sensitive_string">"” ‘define’ ⟨variable⟩ “=” ( ⟨class term⟩ | ⟨class-of term⟩ | ⟨lambda term⟩ ) “\’” “\’”
|
| ⟨lambda term⟩ | = | “\\fun” ( ⟨variable⟩ | “(” ⟨variable⟩ “,” ⟨variable⟩ “)” ) “\\in” ⟨lambda domain⟩ “.” ⟨lambda body⟩ |
| ⟨lambda domain⟩ | = | ⟨term⟩ |
| | | ⟨descriptive class term⟩ | |
| | | ⟨enumerative class term⟩ |
| ⟨lambda body⟩ | = | ⟨function term⟩ | ⟨case function⟩ | ⟨choice term⟩ |
| | | “(” ( ⟨function term⟩ | ⟨case function⟩ | ⟨choice term⟩ ) “)” |
4.11 Statements
| ⟨statement⟩ | = | ⟨headed statement⟩ |
| | | ⟨chained statement⟩ |
| ⟨statement in text-mode⟩ | = | “\\text” “{” ⟨statement⟩ “}” |
| ⟨statement in classtext-mode⟩ | = | “\\classtext” “{” ⟨statement⟩ “}” |
| ⟨headed statement⟩ | = | ⟨quantified statement⟩ |
| | | ⟨if-then statement⟩ | |
| | | ⟨it-is-wrong statement⟩ |
| ⟨chained statement⟩ | = | ( ⟨and chain⟩ | ⟨or chain⟩ | ⟨neither-nor chain⟩ ) [ ⟨chain end⟩ ] |
| ⟨quantified statement⟩ | = | ⟨quantifier chain⟩ ⟨statement⟩ |
| ⟨if-then statement⟩ | = | ‘if’ ⟨statement⟩ ‘then’ ⟨statement⟩ |
| ⟨it-is-wrong statement⟩ | = | ‘it’ ‘is’ ‘wrong’ ‘that’ ⟨statement⟩ |
| ⟨and chain⟩ | = | ⟨atomic statement⟩ { ‘and’ ⟨atomic statement⟩ } |
| ⟨or chain⟩ | = | ⟨atomic statement⟩ { ‘or’ ⟨atomic statement⟩ } |
| ⟨neither-nor chain⟩ | = | ‘neither’ ⟨atomic statement⟩ ‘nor’ ⟨atomic statement⟩ { ‘nor’ ⟨atomic statement⟩ } |
| ⟨quantifier chain⟩ | = | ‘for’ ⟨quantified notion⟩ { “,” ⟨quantified notion⟩ } |
| ⟨chain end⟩ | = | ‘and’ ⟨headed statement⟩ |
| | | ‘or’ ⟨headed statement⟩ | |
| | | ⟨iff⟩ ⟨statement⟩ | |
| | | ( ‘when’ | ‘where’ ) ⟨statement⟩ |
4.11.1 Atomic statements
| ⟨atomic statement⟩ | = | ⟨simple statement⟩ |
| | | ⟨there-is statement⟩ | |
| | | [ ‘we’ ‘have’ ] ( ⟨symbolic statement⟩ | ⟨constant statement⟩ ) |
| ⟨simple statement⟩ | = | ⟨terms⟩ ⟨does-predicate⟩ { ‘and’ ⟨does-predicate⟩ } [ ⟨late quantifiers⟩ ] |
| ⟨there-is statement⟩ | = | ‘there’ ( ‘is’ | ‘exists’ | ‘exist’ ) ( ⟨no notion⟩ | [ ⟨article⟩ ] ⟨notions⟩ ) |
| ⟨symbolic statement⟩ | = | ( ⟨symbolic formula⟩ | ⟨class equality⟩ ) [ ⟨late quantifiers⟩ ] |
| ⟨constant statement⟩ | = | [ ⟨article⟩ ] ( ‘thesis’ | ‘contrary’ | ‘contradiction’ ) |
| ⟨late quantifiers⟩ | = | ‘for’ ⟨quantified notion⟩ { ( “,” | ‘and’ ) ⟨quantified notion⟩ } |
| ⟨class equality⟩ | = | ⟨class term⟩ “=” ⟨class term⟩ |
| | | ⟨class term⟩ “=” ⟨symbolic term⟩ | |
| | | ⟨symbolic term⟩ “=” ⟨class term⟩ |
4.11.2 Symbolic formulas
| ⟨symbolic formula⟩ | = | ⟨biimplication⟩ |
| ⟨biimplication⟩ | = | ⟨implication⟩ [ ( “<” “=” “>” | “\\iff” ) ⟨implication⟩ ] |
| ⟨implication⟩ | = | ⟨disjunction⟩ [ ( “=” “>” | “\\implies” ) ⟨implication⟩ ] |
| ⟨disjunction⟩ | = | ⟨conjunction⟩ [ ( “\\” “/” | “\\vee” ) ⟨disjunction⟩ ] |
| ⟨conjunction⟩ | = | ⟨non-binary formula⟩ [ ( “/” “\\” | “\\wedge” ) ⟨conjunction⟩ ] |
| ⟨non-binary formula⟩ | = | ⟨universal formula⟩ |
| | | ⟨existential formula⟩ | |
| | | ⟨negation⟩ | |
| | | ⟨separated formula⟩ | |
| | | ⟨atomic formula⟩ |
| ⟨universal formula⟩ | = | ( ‘forall’ | “\\forall” ) ⟨symbolic notion⟩ ⟨non-binary formula⟩ |
| ⟨existential statement⟩ | = | ( ‘exists’ | “\\exists” ) ⟨symbolic notion⟩ ⟨non-binary formula⟩ |
| ⟨negation⟩ | = | ‘not’ ⟨non-binary formula⟩ |
| ⟨separated formula⟩ | = | “:” ⟨symbolic formula⟩ |
| ⟨atomic formula⟩ | = | ⟨symbolic relation⟩ |
| | | “(” ( ⟨statement⟩ | ⟨statement in text-mode⟩ ) “)” |
| ⟨symbolic relation⟩ | = | ⟨symbolic chain⟩ |
| | | ⟨primitive circumfix predicate⟩ |
| ⟨symbolic chain⟩ | = | ⟨left head⟩ |
| | | ⟨term chain⟩ ⟨symbolic tail⟩ |
| ⟨left head⟩ | = | ⟨primitive left predicate⟩ ⟨term chain⟩ |
| ⟨symbolic tail⟩ | = | ⟨infix tail⟩ |
| | | ⟨right tail⟩ |
| ⟨infix tail⟩ | = | ⟨primitive infix predicate⟩ ⟨term chain⟩ |
| ⟨right tail⟩ | = | ⟨primitive right predicate⟩ |
| ⟨term chain⟩ | = | ⟨symbolic term⟩ { “,” ⟨symbolic term⟩ } |
4.12 Notions
The following rule is adopted from [2].
| ⟨notion⟩ | = | ⟨class noun⟩ |
| | | ⟨class relation⟩ |
| ⟨no notion⟩ | = | ‘no’ ⟨notion⟩ |
The following rule is adopted from [2].
| ⟨quantified notion⟩ | = | ( ‘every’ | ‘all’ | ‘any’ | ‘each’ ) ⟨notion⟩ |
| | | ‘some’ ⟨notion⟩ | |
| | | ‘no’ ⟨notion⟩ |
| ⟨symbolic notion⟩ | = | ⟨variables⟩ [ ⟨pattern⟩ ] |
4.12.1 Relations
The following rule is adopted from [2].
| ⟨class relation⟩ | = | { ⟨left attribute⟩ } “(” ⟨primitive class relation⟩ “)” [ ⟨right attribute⟩ ] |
| | | { ⟨left attribute⟩ } ⟨primitive class relation⟩ [ ⟨right attribute⟩ ] |
| ⟨primitive class relation⟩ | = | ⟨symbolic pattern⟩ ⟨variables⟩ { ⟨symbolic pattern⟩ ⟨symbolic term⟩ } [ ⟨symbolic tokens⟩ ] |
| | | ⟨variables⟩ ⟨symbolic pattern⟩ { ⟨symbolic term⟩ ⟨symbolic tokens⟩ } [ ⟨symbolic term⟩ ] |
4.12.2 Nouns
The following rule is adopted from [2].
| ⟨class noun⟩ | = | { ⟨left attribute⟩ } ⟨primitive class noun⟩ [ ⟨right attribute⟩ ] |
| ⟨primitive class noun⟩ | = | ⟨alphabetic pattern⟩ [ ⟨variables⟩ [ ⟨alphabetic pattern⟩ ] ] { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
The following rule is adopted from [2].
| ⟨possessed noun⟩ | = | { ⟨left attribute⟩ } ⟨primitive possessed noun⟩ [ ⟨right attribute⟩ ] |
| ⟨primitive possessed noun⟩ | = | ⟨alphabetic pattern⟩ [ ⟨variables⟩ [ ⟨alphabetic pattern⟩ ] ] { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
| ⟨primitive definite noun⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
| ⟨primitive plain noun⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
4.12.3 Attributes
The rules defined in this paragraph are adopted from [2].
| ⟨left attribute⟩ | = | ⟨primitive simple adjective⟩ |
| | | ⟨primitive simple m-adjective⟩ |
| ⟨right attribute⟩ | = | ⟨is-predicate⟩ { ‘and’ ⟨is-predicate⟩ } |
| | | ‘that’ ⟨does-predicate⟩ { ‘and’ ⟨does-predicate⟩ } | |
| | | ‘such’ ‘that’ ⟨statement⟩ |
4.12.4 Predicates
The rules defined in this paragraph are adopted from [2].
| ⟨is-predicate⟩ | = | [ ‘not’ ] ⟨primitive adjective⟩ |
| | | [ ‘not’ ] [ ‘pairwise’ ] ⟨primitive m-adjective⟩ | |
| | | ⟨with⟩ ⟨has-predicate⟩ |
| ⟨is-a-predicate⟩ | = | [ ‘not’ ] ⟨indefinite article⟩ ⟨class noun⟩ |
| | | [ ‘not’ ] ⟨definite term⟩ |
| ⟨does-predicate⟩ | = | [ ⟨does⟩ ] [ ‘not’ ] ⟨primitive verb⟩ |
| | | [ ⟨does⟩ ] [ ‘not’ ] [ ‘pairwise’ ] ⟨primitive m-verb⟩ | |
| | | ⟨has⟩ ⟨has-predicate⟩ | |
| | | ⟨is⟩ ⟨is-predicate⟩ { ‘and’ ⟨is-predicate⟩ } | |
| | | ⟨is⟩ ⟨is-a-predicate⟩ { ‘and’ ⟨is-a-predicate⟩ } |
| ⟨has-predicate⟩ | = | [ ⟨article⟩ ] ⟨possessed noun⟩ { ‘and’ [ ⟨article⟩ ] ⟨possessed noun⟩ } |
4.12.5 Adjectives
| ⟨primitive adjective⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
| ⟨primitive m-adjective⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
| ⟨primitive simple adjective⟩ | = | ⟨alphabetic pattern⟩ |
| ⟨primitive simple m-adjective⟩ | = | ⟨alphabetic pattern⟩ |
4.12.6 Verbs
| ⟨primitive verb⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
| ⟨primitive m-verb⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
4.13 Terms
The rules defined in this paragraph are adopted from [2].
| ⟨term⟩ | = | “(” ⟨quantified notion⟩ “)” |
| | | ⟨quantified notion⟩ | |
| | | ⟨definite term⟩ |
| ⟨definite term⟩ | = | “(” [ ⟨definite article⟩ ] ⟨primitive definite noun⟩ “)” |
| | | [ ⟨definite article⟩ ] ⟨primitive definite noun⟩ | |
| | | ⟨symbolic term⟩ |
| ⟨symbolic term⟩ | = | ⟨primitive infix operator⟩ |
| | | ⟨tighter symbolic term⟩ |
| ⟨tighter symbolic term⟩ | = | ⟨primitive prefix operator⟩ |
| | | ⟨tightest symbolic term⟩ |
| ⟨tightest symbolic term⟩ | = | ⟨primitive postfix operator⟩ |
| | | “(” ⟨symbolic term⟩ “)” | |
| | | ⟨variable⟩ |
4.13.1 Operators
| ⟨primitive infix operator⟩ | = | ⟨tighter symbolic term⟩ ⟨pattern⟩ ⟨symbolic term⟩ |
| ⟨primitive prefix operator⟩ | = | ⟨pattern⟩ ⟨tighter symbolic term⟩ |
| ⟨primitive postfix operator⟩ | = | ⟨symbolic pattern⟩ { ⟨symbolic term⟩ ⟨pattern⟩ } |
| | | ⟨tightest symbolic term⟩ “(” ⟨symbolic term⟩ “)” |
4.13.2 Plain terms
The following rule is adopted from [2].
| ⟨plain term⟩ | = | “(” [ ⟨definite article⟩ ] ⟨primitive plain noun⟩ “)” |
| | | [ ⟨definite article⟩ ] ⟨primitive plain noun⟩ | |
| | | ⟨symbolic term⟩ |
5 References
This reference is based on:
[1] Steffen Frerix, Text-orientated Formalization Methods, Rheinische Friedrich-Wilhelms-Universität Bonn, 2018
[2] Andrei Paskevich, The syntax and semantics of the ForTheL language, Université Paris XII - Val de Marne, Kiev National Taras Shevchenko University, 2007
[3] The source code of Naproche’s ForTheL parser: https://github.com/naproche/naproche
6 Copyright
Marcel Schütz, CC BY-SA 4.0.