Denotational Syntax: Valuation Functions
I'm having trouble understanding some of the lecture slides from a class I am taking (Principles of Programming Languages) and I've been stuck on it for a few days. The slide states (note AS stands for Abstract Syntax and SA stands for Semantic Algebra, I've already learned how to define these):
Finally, we define the valuation function, V : AS → SA.
It is common to ‘partition’ the valuation function into a number of functions whose domains correspond to the abstract syntax nonterminals,
P : Program → Nat → Nat⊥
C : Command → Store⊥ → Store⊥
E : Expression → Store → Nat
B : Boolean-Expression → Store → Bool
N : Numeral → Nat
The meaning of a program (in this language) is a function that maps Natural numbers to Natural numbers.
P : ℕ → ℕ⊥
For example, an input number, argc, is mapped to a number ‘output’ as the final value of the variable x, i.e., P (argc) → x.
Note, that P may not be defined for a given argument. Hence, the codomain of ℕ (i.e. ℕ and the bottom element, ⊥ ).
For example, in the program we’ll examine later,
P (0) → ⊥
I'm having trouble putting this in plain English. For instance, I really don't know what the uptack (⊥) is supposed to mean. What I'm getting from 'P : Program → Nat → Nat⊥' is that it will a program will produce a Natural number which will produce a Natural Number or Bottom element? I don't know what that means.
Submitted July 31, 2015 at 07:41PM by Ass_Dragon
via reddit http://ift.tt/1DgrbNM