Suppositions as I read 'Pict Language Definition, Version 4.1'
I wish the file were searchable.

Sec 2.1: I take it from later text that subscripts are allowed on metavariables. It seems peculiar that syntactic categories are assigned these small fixed strings. Syntactic categories need to appear on the left side of a production. I need to know, for example, what’s in an abstraction. 6.3.3 is only a clue.
Ahaa! This section seems to take effect first in Section 5 where the derived constructs are explained in terms of the core constructs.
“typing context” seems undefined in this document. Later in

2.2: I suppose that ‘Keywords’ are (some of) the terminal productions.

3.3: I wonder if the user gets to see the stuff that is ‘filled in’ such as type annotations.

3.3.2: I collect below the sorts of identifiers (a syntactic category) that I suspect need to appear in declarations (Dec) before use.
Id, Pat (elements thereof), ???

3.3.6: ( Proc1 | ... | Proc 1 ) does not fit special metasyntax ‘...’ pattern.

3.3.10: A rendering error leads to confusion. Apple’s ‘Preview’ makes a .pfd which Adobe’s ‘Reader’ shows in the same bad form:

4.1: "compilation units that has been designated ..." reword!
"preorder traversal" jargon: needs pointer. I presume that "name" in this context is file name and the ‘String’ in the Import.

Anitgripe: 4.1 is more information than I have found for Java. I still do not understand the rules like these for Java. I suspect but don't assume that these preclude dependent compilation.

4.2 There be Dragons! (Well “ccode” is easy to search for.) I presume that fvi must yield a string.

4.2.6 Wow! Hints of magic still beyond the ken.

4.2.8 Facinating

Sec 6: (before 6.1) I presume that the result of the substitution is still a string, or is it some other construct (such as value) used in defining the semantics?

5.1: Opaque
"since it a large increase" I presume that inline defs do post lexing expansion.

5.3: Opaque

6.1: The first use of the simple right arrow. Arrow is briefly described in tutorial on page 21 and more fully in section 2.5.3. The prime is obscure too.

6.3.1: I suppose that it is customary as is but I think that there is an implicit universal quantifier on Γ, albeit informal. One quantifier will do the trick, or one per syllogism.

“Well formed” is used in a contrary way to what I learned 50 years ago. That’s OK but perhaps an explanation. I assume “Γ ⊢ e” means here that all free variables in e are included in Γ.

6.3.2 Here I realize that I need to know the nature of a “binding”. Is it a mere list of variables? Is “x” a binding? How about “•”? Perhaps • is the empty binding.
I deduce from last syllogism that “x1, x2” is a binding since it follows ▷ (right-pointing triangle) and also to the left of a ⊢. Is a binding the same as a typing context?

Index of productions
Abs 3.3.3
Const 3.3.7
Constr 3.3.5
Dec 3.3.2
FieldPat 3.3.4
FieldVal 3.3.7
FieldType 3.3.8
Flag 3.3.2
Import 3.3.1
Kind 2.2.10
KindingPolarityID 3.3.10
Label 3.3.11
Pat 3.3.4
Path 3.3.7
Polarity 3.3.9
Proc 3.3.6
RType 3.3.8
TopLevel 3.3.1
Type 3.3.8
Val 3.3.7
Categories without productions:
String, Id, Int (terminal?), Char, KindredId String & Int are described informally above. I suspect the following is true
Alphanumeric identifiers must be separated by white space. An Alphanumeric identifier followed by a symbolic identifier must have intervening white space. Integers must be separated by white space. Perhaps an integer can be directly followed by an alphanumeric identifier with no whitespace, but I doubt it.

General note

The style of definition is much more accessible than the Algol 68 report whose two level grammar included much of what you do with your scoping rules. The report went to exquisite length to explain all their obscure notation mechanisms in plain but difficult English. Your early definition depends on a good deal of type theory introduced elsewhere. This is not a criticism; yours is easier to read even with my tenuous hold on type theory notation.

The Tutorial

I interrupt this study of the definition to study the tutorial.

The text of section 4.2.2 seems to assume that the reader has some expectations of order of events. I have assumed, so far, only that things happen in some possible order. I remain confused about the meaning of run. I have assumed that there may be queues of values for a channel. These grow when a bang operator fires, and shrink when a question operator fires. I assume also a queue of ‘threads’ blocked on question operators. I have hoped that not all channels need both of these mechanisms. I guess the sample equivalence at the end of the section makes thing clear.

backwater