ForTheL’s FTL 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 FTL lexing
This chapter describes a specification of a lexer for FTL documents. 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 FTL 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.)
| ⟨ftl tokens⟩ | = | { ⟨alphanumeric token⟩ | ⟨symbolic token⟩ | ⟨white token⟩ } |
2.1 Tokens
| ⟨white token⟩ | = | ⟪Horizontal Space⟫ |
| | | ⟪Vertical Space⟫ | |
| | | ⟨comment⟩ |
| ⟨comment⟩ | = | “#” { ⟪Visible Character⟫ | ⟪Horizontal Space⟫ } ⟪Vertical Space⟫ |
| ⟨alphanumeric token⟩ | = | ⟪Alphanum⟫ { ⟪Alphanum⟫ } |
| ⟨symbolic token⟩ | = | ⟪Symbol⟫ \ {“#”} |
2.2 Special tokens
The rules in this paragraph are only needed to specify certain special tokens in the next section.
| ⟨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⟫ \ {“#”, “]”} |
2.3 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 carriage return:
| ⟪Vertical Space⟫ | = | “\U+000A;” |
| | | “\U+000B;” | |
| | | “\U+000C;” | |
| | | “\U+000D;” |
| ⟪Visible Character⟫ | = | “!” | … | “~” |
Horizontal tab, space, line feed, vertical tab, form feed or carriage return:
| ⟪Invisible Character⟫ | = | “\U+0009;” |
| | | “\U+0020;” | |
| | | “\U+000A;” | |
| | | “\U+000B;” | |
| | | “\U+000C;” | |
| | | “\U+000D;” |
3 FTL parsing
This chapter describes a specification of a parser for lexed FTL 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 document.
| ⟨ftl text⟩ | = | { ⟨forthel section⟩ } |
| ⟨forthel section⟩ | = | ⟨instruction⟩ |
| | | ⟨declaration⟩ | |
| | | ⟨top-level section⟩ |
3.1 Special strings
| ⟨label⟩ | = | ⟨label token⟩ { ⟨label token⟩ } |
| ⟨name⟩ | = | “(” ⟨label⟩ “)” |
The following rule is adopted from [2].
| ⟨variables⟩ | = | ⟨variable⟩ { “,” ⟨variable⟩ } |
| ⟨variable⟩ | = | ⟨variable token⟩ { “\’” } |
| ⟨var⟩ | = | ⟨var token⟩ |
| ⟨qed⟩ | = | ( ‘qed’ | ‘end’ | ‘obvious’ | ‘trivial’ ) [ ⟨reference⟩ ] “.” |
3.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’ |
3.3 Instructions
| ⟨instruction⟩ | = | “[” ⟨instr⟩ “]” |
| ⟨instr⟩ | = | ⟨command instruction⟩ |
| | | ⟨limit instruction⟩ | |
| | | ⟨flag instruction⟩ | |
| | | ⟨argument instruction⟩ | |
| | | ⟨synonym instruction⟩ | |
| | | ⟨drop instruction⟩ |
3.3.1 Command instructions
| ⟨command instr⟩ | = | “exit” |
| | | “quit” | |
| | | “thesis” | |
| | | “context” | |
| | | “filter” | |
| | | “rules” |
3.3.2 Limit instructions
| ⟨limit instruction⟩ | = | ⟨limit instr⟩ ⟨limit⟩ |
| ⟨limit instr⟩ | = | “timelimit” |
| | | “memorylimit” | |
| | | “depthlimit” | |
| | | “checktime” | |
| | | “checkdepth” |
| ⟨limit⟩ | = | ⟨numeric token⟩ |
3.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” |
3.3.4 Argument instructions
| ⟨argument instruction⟩ | = | ⟨argument instr⟩ ⟨argument⟩ |
| ⟨argument instr⟩ | = | “read” |
| | | “readtex” | |
| | | “library” | |
| | | “provers” | |
| | | “prover” |
| ⟨argument⟩ | = | ⟨argument token⟩ { ⟨argument token⟩ } |
3.3.5 Synonym instructions
| ⟨synonym instruction⟩ | = | “synonym” ⟨regular alphabetic token⟩ { “/” [ “-” ] ⟨regular alphabetic token⟩ } |
3.3.6 Drop instructions
| ⟨drop instruction⟩ | = | “/” ( ⟨command instr⟩ | ⟨limit instr⟩ | ⟨flag instr⟩ ) |
3.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⟩ “.” |
3.5 Patterns
3.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⟩ |
3.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.
3.6 Top-level sections
| ⟨top-level section⟩ | = | ⟨axiom⟩ |
| | | ⟨definition⟩ | |
| | | ⟨signature extension⟩ | |
| | | ⟨theorem⟩ [ ⟨proof⟩ ] |
3.6.1 Axioms
The following rule is adopted from [2].
| ⟨axiom⟩ | = | ⟨axiom header⟩ { ⟨assumption⟩ } ⟨axiom affirmation⟩ |
The following rule is adopted from [2].
| ⟨axiom header⟩ | = | ‘axiom’ [ ⟨label⟩ ] “.” |
| ⟨axiom affirmation⟩ | = | [ ⟨then⟩ ] ⟨statement⟩ “.” |
3.6.2 Definitions
The rules in this paragraph are adopted from [2].
| ⟨definition⟩ | = | ⟨definition header⟩ { ⟨assumption⟩ } ⟨definition affirmation⟩ |
| ⟨definition header⟩ | = | ‘definition’ [ ⟨label⟩ ] “.” |
| ⟨definition affirmation⟩ | = | ⟨definition statement⟩ “.” |
3.6.3 Signature extensions
The rules in this paragraph are adopted from [2].
| ⟨signature extension⟩ | = | ⟨signature header⟩ { ⟨assumption⟩ } ⟨signature affirmation⟩ |
| ⟨signature header⟩ | = | ‘signature’ [ ⟨label⟩ ] “.” |
| ⟨signature affirmation⟩ | = | ⟨signature statement⟩ “.” |
3.6.4 Theorems
The following rule is adopted from [2].
| ⟨theorem⟩ | = | ⟨theorem header⟩ { ⟨assumption⟩ } ⟨theorem affirmation⟩ |
The following rule is adopted from [2].
| ⟨theorem header⟩ | = | ( ‘theorem’ | ‘proposition’ | ‘lemma’ | ‘corollary’ ) [ ⟨label⟩ ] “.” |
| ⟨theorem affirmation⟩ | = | [ ⟨then⟩ ] ⟨statement⟩ [ ⟨reference⟩ ] “.” |
3.7 Assumptions
| ⟨assumption⟩ | = | [ ⟨name⟩ ] ⟨assumption prefix⟩ ⟨statement⟩ “.” |
The following rule is adopted from [2].
3.8 Definition and notion statements
3.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⟩ | “<” “=” “>” ) ⟨statement⟩ |
3.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’ | “=” “>” ) ⟨statement⟩ |
| | | ⟨predicate head⟩ ‘is’ [ ⟨article⟩ ] ( ‘atom’ | ‘relation’ ) |
Note that in contrast to the rules before, ⟨predicate signature⟩ requires an 'is' instead of an ⟨is⟩.
3.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⟩ |
3.9 Proofs
| ⟨proof⟩ | = | ⟨proof head⟩ { ⟨proof step⟩ } ⟨qed⟩ |
| | | ‘indeed’ ⟨confirmation⟩ |
| ⟨proof head⟩ | = | ‘proof’ [ ‘by’ ⟨method⟩ ] “.” |
| ⟨confirmation⟩ | = | ⟨affirmation⟩ [ ⟨proof⟩ ] |
| | | ⟨choose⟩ [ ⟨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⟩ [ ⟨proof⟩ ] |
| | | ⟨choose⟩ [ ⟨proof⟩ ] | |
| | | ⟨low-level definition⟩ [ ⟨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⟩ ] } “.” |
3.10 Low-level definitions
| ⟨low-level definition⟩ | = | [ ⟨name⟩ ] ⟨class definition⟩ |
| | | [ ⟨name⟩ ] ⟨function definition⟩ |
3.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⟩ ( “|” | “:” ) ⟨statement⟩ “}” |
| ⟨class-of term⟩ | = | ( ‘class’ | ‘classes’ | ‘collection’ | ‘collections’ ) [ ⟨variable⟩ ] ‘of’ [ ‘all’ ] ⟨notion⟩ |
| ⟨separation⟩ | = | ⟨term⟩ |
| | | ⟨term⟩ ‘in’ ( ⟨term⟩ | ⟨class term⟩ | ⟨class-of term⟩ ) |
3.10.2 Function definitions
| ⟨function definition⟩ | = | ‘define’ ⟨variable⟩ “(” ⟨variable⟩ [ “,” ⟨variable⟩ ] “)” “=” ⟨function body⟩ ‘for’ ( ⟨variable⟩ | “(” ⟨variable⟩ “,” ⟨variable⟩ “)” ) ‘in’ ⟨term⟩ “.” |
| | | ‘define’ ⟨variable⟩ “=” ⟨lambda term⟩ “.” |
| ⟨function body⟩ | = | ⟨case function⟩ |
| | | ⟨plain function term⟩ |
| ⟨case function⟩ | = | ‘case’ ⟨statement⟩ “-” “>” ⟨plain function term⟩ [ “,” ⟨case function⟩ ] |
| ⟨plain function term⟩ | = | ⟨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⟩ |
| | | ‘define’ ⟨variable⟩ “=” ( ⟨class term⟩ | ⟨class-of term⟩ | ⟨lambda term⟩ ) |
| ⟨lambda term⟩ | = | “\\” ( ⟨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⟩ ) “)” |
3.11 Statements
| ⟨statement⟩ | = | ⟨headed statement⟩ |
| | | ⟨chained 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⟩ |
3.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⟩ |
3.11.2 Symbolic formulas
| ⟨symbolic formula⟩ | = | ⟨biimplication⟩ |
| ⟨biimplication⟩ | = | ⟨implication⟩ [ “<” “=” “>” ⟨implication⟩ ] |
| ⟨implication⟩ | = | ⟨disjunction⟩ [ “=” “>” ⟨implication⟩ ] |
| ⟨disjunction⟩ | = | ⟨conjunction⟩ [ “\\” “/” ⟨disjunction⟩ ] |
| ⟨conjunction⟩ | = | ⟨non-binary formula⟩ [ “/” “\\” ⟨conjunction⟩ ] |
| ⟨non-binary formula⟩ | = | ⟨universal formula⟩ |
| | | ⟨existential formula⟩ | |
| | | ⟨negation⟩ | |
| | | ⟨separated formula⟩ | |
| | | ⟨atomic formula⟩ |
| ⟨universal formula⟩ | = | ‘forall’ ⟨symbolic notion⟩ ⟨non-binary formula⟩ |
| ⟨existential statement⟩ | = | ‘exists’ ⟨symbolic notion⟩ ⟨non-binary formula⟩ |
| ⟨negation⟩ | = | ‘not’ ⟨non-binary formula⟩ |
| ⟨separated formula⟩ | = | “:” ⟨symbolic formula⟩ |
| ⟨atomic formula⟩ | = | ⟨symbolic relation⟩ |
| | | “(” ⟨statement⟩ “)” |
| ⟨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⟩ } |
3.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⟩ ] |
3.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⟩ ] |
3.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⟩ ] |
3.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⟩ |
3.12.4 Predicates
The rules 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⟩ } |
3.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⟩ |
3.12.6 Verbs
| ⟨primitive verb⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
| ⟨primitive m-verb⟩ | = | ⟨alphabetic pattern⟩ { ⟨term⟩ ⟨alphabetic pattern⟩ } [ ⟨term⟩ ] |
3.13 Terms
The rules 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⟩ |
3.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⟩ “)” |
3.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⟩ |
4 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
5 Copyright
Marcel Schütz, CC BY-SA 4.0.