Grail Tutorial - Definitions and Vocabulary

Given that there is quite a lot of vocabulary which is introduced throughout the different sections of this tutorial, this section lists the different terms and their alternatives.

A

AB
AB grammars are a grammar formalism named after its two founders Ajdukiewicz (1935) and Bar-Hillel (1964). AB grammars are a restriction of the grammars Grail allows you to write and are discussed in a separate section of this tutorial.
abstract proof structure
Technical name for the graphs used by Grail for both for its lexical entries and for the graphs shown during the analysis of a phrase. The term was introduced in (Moot & Puite 2002). Compared to a proof structure the formulas assigned to the internal nodes of the graphs are missing.
active component
A component is called active whenever there is no arrow from an auxiliary constructor which arrives at one of its nodes.
active formula
A link, depending on whether it corresponds to a unary or a binary connective, connects either two or three formulas. ...
auxiliary constructor (also called par link or destructor)
Auxiliary constructors are graph connections like the main constructors, but instead of creating tree structure, like the main constructors do, they destroy structure.
axiom link
Connection of a positive and negative formula in a proof structure. Frequently called a substitution in this tutorial.

C

component (also called tensor tree)
Given a proof structure or an abstract proof structure, we obtain the set of its components by erasing all its par links (but not the nodes they are connected to). Each connected subgraph of the resulting graph, possibly just a single node, is a component.
contraction 1
Contraction is a structural rule of classical and intuitionistic logic stating that the number of occurrences of a formula A does not matter. This is true when A is something like a lemma, which, once proved can be used any number of times without necessitating a reproof but not when A is a resource such as a euro or (in the linguistic context) a noun phrase.
contraction 2
A contraction is the operation of removing a main and an auxiliary constructor from an abstract proof structure in order to try and obtain a tree and show the proof structure is a proof net. Contractions are explained in the section about NL for the binary modes. Other sections of the tutorial discussing contractions are the section about modes, which discusses multimodal contractions and the section about unary contractions. See an image of all binary contractions and all unary contractions.
correctness criterion
A correctness criterion is a way to identify those proof structures which correspond to proofs (in other words, which are proof nets) from those who do not.

G

graph
Generic term for a set of nodes or vertices connected by a set of edges or links. Throughout this tutorial, I will frequently use the term graph to mean abstract proof structure, the specific type of node- and edge-labeled graph used by Grail.

L

L (also called Lambek calculus)
L is short for Lambek's syntactic calculus (Lambek 1958), also called the Lambek calculus. Lambek added the right rules for the implications to AB and proved basic results like cut elimination and decidability for the calculus.
lexical leaf
A lexical leaf of a graph (or abstract proof structure) ...
lexical graph
Graph (or abstract proof structure) assigned by a grammar to a word in the lexicon.
linear logic
Linear logic is a logic discovered by Girard (1987). It rejects global use of the rules of contraction and weakening and is therefore more suited than classical logic for dealing with resources. Lambek calculi can be seen as even more restricted in their resource management than linear logic in that global use of the commutativity (and associativity in the case of NL) are rejected as well.
link
A link is a special type of subgraph: we display a link with a central circle connecting three (or two in the case of the unary connectives) nodes. See an image of all links in multimodal categorial grammars.

M

main constructor
A main constructor (also called tensor link when is it opposed to a par link or just constructor when opposed to a destructor).
mode
A mode (sometimes called a mode of composition) is a way of distinguishing between different ways of composing linguistic resources. It can be used to distinguish between left-headed and right-headed composition, for example, or to allow lexically controlled acces to structural rules.
mode of composition, see mode

N

NL
Abbreviation for the the Non-associative Lambek calculus, introduced in (Lambek 1961). Grail grammars for NL are discussed in a separate section of this tutorial

P

par
The term par comes from linear logic where it is the multiplicative disjunction. Therefore, par links in proof structures correspond to a type of logical or. For example, the par links for NL are the product link for formulas AB when it occurs in a negative position (as a hypothesis) and the links for the implications when they occur in positive (conclusion) positions. Using the definition of implication in terms of disjunction and negation and the de Morgan rule for the distribution of negation over conjunction, we see that both these cases correspond to a logical or as follows.
A → B = ¬ A ∨ B
¬(A ∧ B) = ¬ A ∨ ¬ B
proof net
The term proof net was first used as a way present proofs for (multiplicative) linear logic in the form of graphs, introduced by Girard (1987). It has the advantage of identifying proofs which differ only for bureaucratic reasons.

Proof nets are usually defined as a subset of a larger class of structures, called proof structures which satisfy an additional correctness criterion.

proof structure
A proof structure is a representation of a logical statement, not necessarily derivable, in the form of a graph.

R

resource
Resource is a generic term used for entities which are single-use. In the context of categorial grammars an np is a resource since, when we combine it with a verb of type np\s

T

tensor
Tensor is the name for the multiplicative conjunction of linear logic. The links for the implications, when they occur in a negative (hypothesis) context and the link for the product in a positive (conclusion) context are tensor links. Note that these are the main links. For the implications, we can see they correspond to conjunctions by the translation of implication into disjunction combined with the de Morgan rule for the distribution of negation over disjunction.
¬(A → B) = ¬(¬ A ∨ B) = A ∧ ¬ B

Richard.Moot@labri.fr
Last modified: Wed Feb 25 22:14:05 CET 2009