Definition 1 uses something like Backus–Naur Form, though BNFs usually use ::= instead of := . This means that K is either an ordered pair or the result of the operation defined in point 3. Along with K, is another nonterminal symbol. I would render this grammar as follows, with defined separately.

Concerning Definition 4, apparently the interpretation of K is a binary relation on functions. Also, is defined as a relation on functions. The five points of the definition correspond to five variants of K and in the grammar above. The circle is the composition of relations.