doc-src/Logics/syntax.tex
 author haftmann Wed Dec 27 19:10:06 2006 +0100 (2006-12-27) changeset 21915 4e63c55f4cb4 parent 14209 180cd69a5dbb child 42637 381fdcab0f36 permissions -rw-r--r--
different handling of type variable names
     1 %% $Id$

     2 %% THIS FILE IS COMMON TO ALL LOGIC MANUALS

     3

     4 \chapter{Syntax definitions}

     5 The syntax of each logic is presented using a context-free grammar.

     6 These grammars obey the following conventions:

     7 \begin{itemize}

     8 \item identifiers denote nonterminal symbols

     9 \item \texttt{typewriter} font denotes terminal symbols

    10 \item parentheses $(\ldots)$ express grouping

    11 \item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$

    12 can be repeated~0 or more times

    13 \item alternatives are separated by a vertical bar,~$|$

    14 \item the symbol for alphanumeric identifiers is~{\it id\/}

    15 \item the symbol for scheme variables is~{\it var}

    16 \end{itemize}

    17 To reduce the number of nonterminals and grammar rules required, Isabelle's

    18 syntax module employs {\bf priorities},\index{priorities} or precedences.

    19 Each grammar rule is given by a mixfix declaration, which has a priority,

    20 and each argument place has a priority.  This general approach handles

    21 infix operators that associate either to the left or to the right, as well

    22 as prefix and binding operators.

    23

    24 In a syntactically valid expression, an operator's arguments never involve

    25 an operator of lower priority unless brackets are used.  Consider

    26 first-order logic, where $\exists$ has lower priority than $\disj$,

    27 which has lower priority than $\conj$.  There, $P\conj Q \disj R$

    28 abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$.  Also,

    29 $\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than

    30 $(\exists x.P)\disj Q$.  Note especially that $P\disj(\exists x.Q)$

    31 becomes syntactically invalid if the brackets are removed.

    32

    33 A {\bf binder} is a symbol associated with a constant of type

    34 $(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as a binder

    35 for the constant~$All$, which has type $(\alpha\To o)\To o$.  This defines the

    36 syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We can also write $\forall   37 x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is

    38 possible for any constant provided that $\tau$ and $\tau'$ are the same type.

    39 The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To   40 bool)\To\alpha$ and normally binds only one variable.

    41 ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a

    42 binder because it has type $[i, i\To o]\To o$.  The syntax for binders allows

    43 type constraints on bound variables, as in

    44 $\forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z)$

    45

    46 To avoid excess detail, the logic descriptions adopt a semi-formal style.

    47 Infix operators and binding operators are listed in separate tables, which

    48 include their priorities.  Grammar descriptions do not include numeric

    49 priorities; instead, the rules appear in order of decreasing priority.

    50 This should suffice for most purposes; for full details, please consult the

    51 actual syntax definitions in the {\tt.thy} files.

    52

    53 Each nonterminal symbol is associated with some Isabelle type.  For

    54 example, the formulae of first-order logic have type~$o$.  Every

    55 Isabelle expression of type~$o$ is therefore a formula.  These include

    56 atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more

    57 generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have

    58 suitable types.  Therefore, expression of type~$o$' is listed as a

    59 separate possibility in the grammar for formulae.

    60

    61
`