Unclear logic notation for PFX program rules

Question

I'm very new to this so please bear with me.

I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the result.

The image is supposed to be the rules describing the logic of a PFX program, but being very new to logical symbols, I can barely read it.

From what I understand, the top parts are suppositions and the bottom parts are conclusions. The first one, to me, reads, if i is different from n, then if either of the vk's implies i, the program declares an error. But I can tell my understanding is deeply flawed. I searched and have found close to no similar rules.

Also, the use of the letter "i" seems unclear to me mostly.

If someone can explain with words what the rules actually mean, it would help me a lot.

Thank you.

Answer 1

The "fraction"-style notation is an inference rule in natural deduction style. See What is this fraction-like "discrete mathematics"–style notation used for formal rules?.

$v_1,\dots,v_n\vdash \cdots$ means "in the environment $v_1,\dots,v_n$, such-and-such is true". (It's not an "or", and it doesn't mean "implies".) See What does ⊢ mean in operational semantics?.

I recommend finding a good textbook on programming language semantics, and reading it. It will give you some background that will help you understand that notation. It's probably too much to explain all of that in a single answer here.