Denotational Syntax: Valuation Functions

Solved

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 a program will produce map a Natural number which will produce a Natural Number or Bottom element? I don't know what that means.

Edit: a grammars

Posted Jul 31, 2015, 11:41 PM UTC · edited

93
Loading comments…