I have the following def's

Sns : Stm → (State ֒→ State)

Sns[S] = s' (if <S,s> -> s') else undefined

I'm wondering if Sns is a partial or total function. I think it's total since it always returns a partial function, given any statement.

But the book I'm reading (semantic with application by wiley, pg 41) says:

Note that Sns is a well-defined partial function because of Theorem 2.9. The need for partiality is demonstrated by the statement while true do skip that always loops.

I'm very confused.

  • 1
    $\begingroup$ If your system is normalizing, then the semantics is total over the well-formed expressions. If your system is not normalizing, then the semantics is partial, because it can assign a "meaning" only to expressions that terminate. $\endgroup$ – frabala May 25 '19 at 11:43
  • $\begingroup$ It is possible that the book is considering Sns as a two-argument function, taking statement S and state s as arguments. In such interpretation, it is partial (for your imperative language with infinite loops). $\endgroup$ – chi May 25 '19 at 12:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.