1
$\begingroup$

I was reading about denotational semantics

Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. For example, programs (or program phrases) might be represented by partial functions.

I was wondering, how does one map programs to partial functions? What is the mapping? What is the intuition and conceptual idea? I don't understand what the relationship (formally or conceptually) is between partial functions and program (or Turing Machines).

$\endgroup$

2 Answers 2

3
$\begingroup$

Partial functions from initial program states to final program states are a suitable model for deterministic sequential programs that do not interact with the environment while executing. Such programs just try to compute a result depending on what they find in their starting state. If program $P$'s attempted computation fails when starting from some initial state $\sigma$, then that means that the function describing $P$'s semantics doesn't yield a final state for $\sigma$.

Using functions (of the common type mentioned above) makes sense when the constructs of the programming language under consideration are deterministic. That is the case e.g. for a language made up of assignment statements, sequential composition, conditionals, and while loops.

Partial as opposed to total functions are chosen for two reasons. 1. to allow loops to diverge and 2. to model problems such as division by 0.

$\endgroup$
2
  • $\begingroup$ related question, why are states also reasonable to think of as partial function on identifiers to say, values (e.g. integers) $\sigma: Id \rightharpoondown Int$? Is the idea that when a variable is not defined i.e. $x \not \in Domain(\sigma)$, does that mean $\sigma(x) = \bot$? $\endgroup$ Nov 7, 2019 at 22:33
  • $\begingroup$ also related to point 2, when we allow programs to diverge, how is the denotation know to map that to the bottom element beforehand? Thats undecidable. Except for something silly like $ [ while(true)\{ \} ]\sigma = \bot $ $\endgroup$ Nov 7, 2019 at 22:36
0
$\begingroup$

The point is to express what a piece "means"/semantics. To define what it means we map syntax **at a given state ** (that takes in a state $\sigma$) to a mathematical object. This mathematical object is maps. Basically code takes in states to states (where a [of the program] state just says what the variables are for example). So for example:

$$ [\![ i ]\!] \sigma = f_i(\sigma) = i$$

where $[\![ i ]\!] = f_i$ the partial map that when given a state returns the integer $i$. That is what the code fragment $i$ means. Basically $[\![ \cdot ]\!]$ maps the syntax to a CPO (complete partial order), essentially partial functions.

The reason we do this is because we are defining what the code does by saying how it maps states to states. Partial is because some code maps to undefined $\bot$. So some subset of the domain (domain are states) is undefined or simply we say

$$[\![ Syntax ]\!] \sigma = f_{Syntax} ( \sigma ) = \bot $$

Programs map states to states or undefined. Thats why programs can be mapped to partial functions.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.