Talk:Haskell/Denotational semantics

From Wikibooks, the open-content textbooks collection

Look of ⊥ in a mathematical context, $\perp$ is preferred, whereas in a code context, ⊥ should be the way to go.
Draw real pictures showing the various poset structures. Especially the ones with the recursive data type definitions!
It's very cool that semantics can partly be explored in Haskell itself. Are there paragraphs where this opportunity was forgotten?

Improve examples and exercises. Most have been invented very quickly and are not very good. Those that are, are most likely ones that I remembered from different textbooks. Exercises where one must repeat or slightly modify the explanation from the text are helpful for a first understanding but should be held in low quantities. True insight can be only be achieved by tasks where one has to twist one's mind. Train your brain, don't train a pattern.
Add more exercises and examples? A spot where readers frequently get stuck is clearly a good place for additional examples and exercises. Hopefully, these will emerge at this Talk-page.

Apfelmus 19:39, 22 December 2006 (UTC)

1 Denotational semantics
2 forall a . a
3 Mistake in the definition of ?
4 Love it!
5 Non-strict constructors
6 Approximations of the Factorial Function
7 Denotional semantics & Equational reasoning
8 Continuity
9 Not all Functions in Strict Languages are Strict
10 Partiality of (in "Strict functions")
11 Definition of
12 Functions with several Arguments
13 take 3 nats
14 Recursive data types and infinite lists diagram
15 Naïve Sets are unsuited for Recursive Data Types
16 Is g in section 3.1 a monotone functional?
17 Functions Integer -> Integer is a (d)cpo
18 Why is Nothing less defined than Just True?
19 Haskell Recursion Example

[edit] Denotational semantics

Imperative languages can certainly be given denotational semantics. It's just that a direct semantics doesn't work anymore. You need to model the store, and usually continuations as well.

Furthermore imperative languages can be given other non-operational semantics such as Floyd-Hoare-Dijkstra style axiomatic semantics. You (Apfelmus) may be interested to search the EWD archive for what Dijkstra had to say about operational reasoning, most of it in regard to imperative programming. It was I who removed the erroneous and misleading paragraph mentioning imperative languages. I apologise for not adding an edit summary this was due to my stupidity not rudeness.

Of course, you are right. Indeed, just by using a MonadState, one already gives denotational semantics to imperative stuff. I somehow wanted to pin down that reasoning is much easier in purely functional languages because the semantics are very direct. So I just denied denotational semantics for imperative stuff altogether and hoped nobody would complain :) Compared to pure functional programs, it doesn't matter much whether I have operational ("machine, change your state!") or denotational ("plan of how machine state changes") semantics, the reasoning doesn't get much easier. Denotational semantics tries to recapture as much pure stuff as possible from the operational semantics, similar in power to the finding of a suitable loop invariant. Ah, and thanks for the EWD link. Apfelmus 22:29, 27 December 2006 (UTC)

[edit] forall a . a

The type 'forall a . a' doesn't have to give an error. It can also loop forever. (Which is an error, but not observable.)

Fixed, "any function of the polymorphic type forall a . a must denote ⊥". Why didn't I chose that compelling formulation in first place? Apfelmus 21:04, 27 December 2006 (UTC)

[edit] Mistake in the definition of $\sqsubset$ ?

Isn't there a mistake in the definition, which states that " $a \sqsubset b$ denotes that a is more defined than b" ? It seems inconsistent with "every concrete number is more defined than $\perp$ : $\perp\ \sqsubset 1\ ,\ \perp\ \sqsubset 2\ , \dots$ ". Shouldn't it be "less defined" ?

I was going to point this out too. How about " $a \sqsubset b$ denotes that b is more defined than a"? 71.202.203.117 00:34, 27 December 2006 (UTC)

Oops, it's a mistake of course. Fixed. At the same time, I reverted "completely equal programs" to "equal", because of the subtetly that programs can be syntactically equal as well. Of course, they can be syntactically different and still denote the same "mathematical object". Apfelmus 20:47, 27 December 2006 (UTC)

[edit] Love it!

Has really helped my understanding. Thankyou.

I did some images, they're perhaps a bit big, anyone who cares can resize them. DavidHouse 17:32, 26 December 2006 (UTC)

[edit] Non-strict constructors

"because we can write a function that tells them apart"

f (Just _) = 4
f _        = 7

"As f ignores the contents of the Just constructor, f (Just _|_) is 4 but f _|_ is 7." This argument is truly ingenious but unfortunately wrong :) With the above definition, we have f ⊥ = ⊥. The stated properties cannot hold because they violate monotonicity. The fact that Just ⊥ is different from ⊥ cannot be "proved", it's a design decision. How can this be formulated nicely? The author above clearly wanted to appeal to a "proof" by example like in the case of const 1. Apfelmus 13:38, 28 December 2006 (UTC)

[edit] Approximations of the Factorial Function

The sentence "That is, it transforms less defined functions to more defined ones." seems to mean that $x\sqsubseteq g(x)$ for all x which isn't true.

You're right. I just put in a clarification that hopefully makes more sense. Stereotype441 15:28, 8 February 2007 (UTC)

[edit] Denotional semantics & Equational reasoning

I just found an interesting article Fast and loose reasoning is morally correct. Basically it says that even though having Bottom results in inconsistent logic, with a few simple constraints equational proofs still work. I wonder whether some of it can be useful here. I'll be away the rest of the weekend but then will try to read the paper more carefully. I also wonder if the subject of w:paraconsistent logic has any applicability here. </clueless newbie> 64.160.39.153 05:28, 4 March 2007 (UTC)

Hello, sorry for this late response. I planned a chapter Haskell/Equation reasoning that covers reasoning formally about Haskell programs. As you point out, it would be great to have a subsection based on the article you mentioned that shows how equational reasoning keeps working with ⊥ although it usually assumes that all programs terminate. Thanks for your suggestion :) I don't know enough about paraconsistent logic, but equational reasoning that ignores ⊥ is like calculating with infinitesimal numbers: done right, it works, done wrong, it doesn't :). Related to that, I'd like also to outsource the infinite lists from this chapter to a place where all forms of program proofs (equational, denotational semantics, coinduction) live together, maybe even as a separate chapter. -- apfeλmus 12:10, 24 April 2007 (UTC)

[edit] Continuity

The text says that for any type a, any monotone function f :: a -> Integer must be continuous. Why? I can only prove $\sup\{f(x_0), f(x_1), \ldots \} \sqsubseteq f(\sup\{x_0, x_1, \ldots \})$ . Why there is not a type a and a sequence of values $x_0 \sqsubseteq x_1 \sqsubseteq \ldots$ of type a such that, say, $f(x_i) = \perp$ for any $i$ and $f(\sup \{x_0, x_1, \ldots\}) = 0$ ?

In the light of your comment, the argument in the text indeed doesn't show anything.

The fundamental question I wanted to answer is that although the choice allowing or disallowing continuity is an arbitrary choice, every programming language can only formulate continous function. What magic makes this possible? I think that one can of course prove for every given language (given by its programming constructs like case, if .. then .. else, recursion and so on) that only continous functions can be written down. However, I feel that this is not the right way to prove it because this property is universal for all programming languages, hence there ought to be a proof working for all languages at the same time.

If the type a has only chains with finitely many elements, continuity is granted for free. But for example, Integer->Integer has infinite chains, one being

$x_i = n\mapsto\mbox{ if } n \le i \mbox{ then } 0 \mbox{ else } \perp$ .

Of course, $x_i\sqsubset x_{i+1}$ . Now, imagine a non-continuous function f :: (Integer->Integer) -> Integer with the requirements

$f(x_i)=\perp$
$f(\sup \{x_0, x_1, \ldots\})=0$

Can this funtion be written down in Haskell? No, for it would have to test it's function argument at all possible value and check whether the outcome is 0. Clearly, this would take an infinite amount of time. What I had in mind when writing the text is that the transition of

f

from ⊥ to 0 must happen at some finite point in the chain, the decision whether it's ⊥ or 0 may not be postponed to infinity. This is due to the finite nature of computation. With this in mind, the current text argues that the image of any function has in essence only finite chains so that the decision about the result value can indeed be done after a finite number of steps.

Of course, this whole argument isn't formally correct, but I think it hints on what's going on. I currently don't know a correct argument.

Clearly, the text needs a rewrite, though I'm unsure on how to do that. -- apfeλmus 11:31, 24 April 2007 (UTC)

I have an informal counterexample (maybe), but I haven't the knowledge to formalize it. It is inspired by Fran (indeed, I found this book when trying to understand Fran semantics). Let us define

data Time = Exact Float | Interval Float Float

A value Exact t means "time is t" and a value Interval t1 t2 with $t_1 \le t_2$ means "time is in between t1 and t2". Thus, according to this meaning, we define Interval t1 t2 $\sqsubset$ Exact t for any $t \in [t_1,t_2]$ and Interval t1 t2 $\sqsubset$ Interval s1 s2 iff $[s_1,s_2] \subset [t_1,t_2]$ . Now consider the sequence xn = Interval 0 (1/n), which converges to Exact 0, and consider the function f = g . len where

len Interval t1 t2 = t2 - t1

len Exact t = 0

and g is any function such that g 0 = 0 and g x = ⊥ for any $x \ne 0$ . This is only an informal example, I don't know if it is valid.

I don't think it's a counterexample because the meaning of $\sqsubset$ is fixed as "less defined than". I mean, neither Interval t1 t2 $\sqsubset$ Exact t nor Interval t1 t2 $\sqsupset$ Exact t hold. In other words, $\sqsubset$ is quite different. Your example basically tries to introduce the real numbers into denotational semantics by redefining $\sqsubset$ . Of course, not all functions on real numbers are continuous anymore. (In fact, they all are continuous again in intuitionistic logic but that leads too far here)

Also note that Float is a bad choice, because there is a smallest nonzero floating point number, i.e. the sequence xn doesn't converge to Exact 0. But you can use an exact representation of rational numbers instead to make at least this convergence work.

-- apfeλmus 15:50, 26 April 2007 (UTC)

[edit] Not all Functions in Strict Languages are Strict

I think this section is wrong. The reason that the lifting trick works is not because functions are not strict in function types, but because lambda terms like (\x:Int.1) or (\x:Int._|_) are in normal form and so cannot take a step of evalution. Other terms of type Int->Int, like (\x:Int->Int.x)(\x:Int.x) will be reduced.

In fact (ignoring type classes), evaluation in a Haskell-like language ought to be completely independent of type information, which can be erased and forgotten once type checking is completed. In a strict language, if const1 (undefined :: Int) = _|_, then const1 (undefined :: Int->Int) = _|_.

The following Standard ML code supports this:

exception Undefined

fun const1 (x:int->int) = 1

const1 (raise Undefined)

In the above code, const1 has type (int->int)->int and raise Undefined, which has equivalent behaviour to Haskell's undefined, has type int->int.

The line const1 (raise Undefined) gives an exception (bottom), not 1.

A strict language shown in chapter 14 of TAPL has an 'error' term, very similar to Haskell's 'undefined'. It also has this behaviour.

Rebooted 15:32, 6 September 2007 (UTC)

Good point. The problem is that ML has "two" undefined functions, namely

raise Undefined :: Int -> Int

and

λx.raise Undefined :: Int -> Int

or better

fix (λf x.f x) :: Int -> Int

In other words, we can distinguish between a function that is an exception and a function that raises an exception on every value. Put differently, the function type is lifted by an additional ⊥ ~= raise Undefined and every function is indeed strict with respect to this ⊥. Unfortunately, this ⊥ is useless for fixpoint iteration which depends on ⊥ = λx.⊥ (as defined in the beginning of the chapter).

So, yes, the section is not correct but the denotational semantics of call-by-value are even trickier than the section is wrong :-) I'm unsure what to do. I wanted the section to somehow show the () -> a trick which can simulate call-by-name in a call-by-value language. Hm, maybe it doesn't belong to denotational semantics at all?

-- apfeλmus 16:59, 6 September 2007 (UTC)

I'd recommend removing the section and replacing it with one entitled "Emulating non-strict behavior in strict languages" which just demonstrates the trick.

Rebooted 15:31, 9 September 2007 (UTC)

On second thought, I'm not sure whether this solves the problem because the issue is even larger now: the discussion of "strict language" is wrong, too. I mean, the whole chapter implicitly assumes that λx.⊥=⊥ which doesn't work for call-by-value. Also, the trick works still thanks to some kind of non-strictness, namely the fact that f (λx.⊥) =/= ⊥ in contrast to f ⊥ = ⊥.

It's probably best to look up the exact denotational semantics of call-by-value in a paper/book to figure out how (or whether) to present strict semantics.

--apfeλmus 08:33, 10 September 2007 (UTC)

Self-note: fixpoints in call-by-value are fine, it's just that the iterated functional is not strict in the value (and thus not internal to the language). In other words, a function fix that starts the iteration with ⊥ would be rather useless in a call-by-value language.

--apfeλmus 20:05, 6 October 2007 (UTC)

[edit] Partiality of $\sqsubseteq$ (in "Strict functions")

FIXME: $\sqsubseteq$ defines a totally ordered set (toset) on [[Integer]], so we have either $2 \sqsubseteq 5$ or $5 \sqsubseteq 2$ or both ; if both were true, then 2 = 5, which would be effectively a contradiction, but we can still have either $2 \sqsubseteq 5$ or $5 \sqsubseteq 2$ where one of these two predicates is true and the other is false. Such thing is easy to define by defining a semantic to $x \sqsubseteq y$ where x and y are both non-undefined integers, using a "friend" toset on [[Integer]]-{undefined} (such as $\le$ ). So 2 and 5 can be compared with $\sqsubseteq$ .

Isn't there a confusion here between the toset $\sqsubseteq$ and the poset $\sqsubset$ ?

-- 90.50.99.233

Eh? The main point about $\sqsubseteq$ (i.e. $\sqsubset$ ) is that it's not a total ordering, exemplified in Haskell/Denotational semantics#Partial Functions and the Semantic Approximation Order. The choice that neither $2 \sqsubset 5$ nor $2 \sqsupset 5$ hold is intentional, the semantic approximation order only says whether one value (like ⊥) is an approximation to another one (like 1). The usual ordering $\leq$ of integers is irrelevant here.

--apfeλmus 20:02, 6 October 2007 (UTC)

[edit] Definition of $\sqsubseteq$

The definition of $\sqsubseteq$ seems pretty counter-intuitive for me: Are not $2\sqsubseteq 5$ at equally defined?

2 = 5

still means "equal". In other words, $\sqsubseteq$ is "the same value, less defined" but not "some values ordered by some degree of definedness". apfeλmus 08:54, 18 June 2008 (UTC)

[edit] Functions with several Arguments

Should not the code associated with "We see that it is strict in y depending on whether ..." be

cond True  x ⊥ = x;
cond False x ⊥ = ⊥

instead the current one? --AndresSR (talk) 21:46, 28 January 2008 (UTC)

That's right, thanks :-) Fixed now. -- apfeλmus 08:23, 29 January 2008 (UTC)

[edit] `take 3 nats`

take 2 (map (+1) nats) = take 3 nats

Is this really true? Doesn't the left expression evaluate to [2, 3] while the right expression evaluates to [1, 2, 3]?

--Md2perpe (talk) 00:03, 17 February 2008 (UTC)

Oops, that's wrong of course. I'm going to fix that. -- apfeλmus 22:01, 20 February 2008 (UTC)

[edit] Recursive data types and infinite lists diagram

In the illustration of the data type

   data List = [] | () : List

The value ():[] is shown below ():_|_. Is this a mistake? Thanks.

Oops, it indeed is. -- apfeλmus 21:11, 8 May 2008 (UTC)

[edit] Naïve Sets are unsuited for Recursive Data Types

Nevermind, didn't read carefully enough 76.105.193.33 (talk) 13:45, 22 September 2008 (UTC)

[edit] Is g in section 3.1 a monotone functional?

Take f such that f(2)=1 and f = _|_ everywhere else. Now g(f)(2) = 2*f(1) = 2 * _|_ = _|_ , which is less defined than f(2) ?

Oh. Right, thank you for pointing this out. Looks like there's a fundamental flaw in the argument presented. I'll fix that.

-- apfeλmus 08:06, 12 October 2008 (UTC)

Ah wait, no that's no problem. Monotone doesn't mean that the result is more defined than the orginal ( $x \sqsubseteq g(x)$ ), it means that a larger orgininal will be turned into a larger result ( $x \sqsubseteq y \Rightarrow g(x) \sqsubseteq g(y)$ ). So, the fixed point iteration only works if we start with $x_0=\perp$ .

-- apfeλmus 12:24, 12 October 2008 (UTC)

[edit] Functions `Integer -> Integer` is a (d)cpo

I don't understand why that monotone sequences may be of infinite length implies functions Integer -> Integer is a (d)cpo.
$\forall n \in \mbox{ Integer } . \sup_{\sqsubseteq} \{\dots f_{j-1}(n) \sqsubseteq f_j(n) \sqsubseteq f_{j+1}(n) \sqsubseteq \dots\} = i_n$
$f (n) = i n$
$\forall j \mbox{ is index of chain } . \forall m \in \mbox{ Integer } . f_j(m) \sqsubseteq i_m \Rightarrow \forall j \mbox{ is index of chain } . f_j \sqsubseteq f$
$\therefore f \mbox{ is upper bound of } \{\dots f_{j-1}(n) \sqsubseteq f_j(n) \sqsubseteq f_{j+1}(n) \sqsubseteq \dots\}$
Define $k \sqsubset g \mbox{ if } \forall x. k(x) \sqsubseteq g(x) \mbox{ and } \exists y. k(y) \sqsubset g(y)$
$\forall h . h \sqsubset f \Rightarrow \exists n . h(n) \sqsubset f(n) = i_n$
$\Rightarrow h(n) \mbox{ is not upper bound of chain } f_j(n) \Rightarrow h \mbox{ is not upper bound of chain } f_j$
$\therefore \sup_{\sqsubseteq} \{\dots f_{j-1} \sqsubseteq f_j \sqsubseteq f_{j+1} \sqsubseteq \dots\} = f$
$\therefore$ every chain of functions Integer -> Integer has a least upper bound.
Therefore, functions Integer -> Integer is a (d)cpo. --LungZeno (talk) 03:55, 7 November 2008 (UTC)

What the text wants to say is the following: if monotone sequences are always finite, like in the case of Integer, then it's clear that the ordering is complete. Of course, this doesn't work for Integer->Integer, but there is a (slightly) different argument that does show that the partial functions are a cpo, too.

apfeλmus 09:51, 7 November 2008 (UTC)

~~Does "finite" mean that number of element in a monotone sequence is finite?~~

~~Or mean that number of monotone sequences in Integer is finite?~~

--LungZeno (talk) 11:10, 7 November 2008 (UTC)

I saw the explaination.

You mean that number of elements in every monotone sequence in Integer is finite.

--LungZeno (talk) 11:42, 7 November 2008 (UTC)

My proof is wrong. Because

$\forall h . h \sqsubset f \Rightarrow \exists n . h(n) \sqsubset f(n) = i_n$

$\Rightarrow h(n) \mbox{ is not upper bound of chain } f_j(n) \Rightarrow h \mbox{ is not upper bound of chain } f_j$

$\therefore \sup_{\sqsubseteq} \{\dots f_{j-1} \sqsubseteq f_j \sqsubseteq f_{j+1} \sqsubseteq \dots\} = f$

Only prove that every chain of functions Integer -> Integer has a minimum upper bound.

Changing my proof to

$\forall n \in \mbox{ Integer } . \mbox{ cardinal of } \{f_j(n) | f_j(n) \sqsubseteq f_{j+1}(n)\} \mbox{ is finite }$

$\Rightarrow \mbox{ supremum } i_n \in \{f_j(n) | f_j(n) \sqsubseteq f_{j+1}(n)\}$

$\therefore \forall j , h , n. f_j \sqsubseteq h \Rightarrow f_j(n) \sqsubseteq h(n) \Rightarrow i_n \sqsubseteq h(n) \Rightarrow f(n) \sqsubseteq h(n) \Rightarrow f \sqsubseteq h$

$\therefore$ every chain of functions Integer -> Integer has a least upper bound.

--LungZeno (talk) 12:24, 7 November 2008 (UTC)

[edit] Why is Nothing less defined than Just True?

And why is it at the same level as Just _|_ ? --Colin-adams (talk) 21:03, 22 November 2008 (UTC)

It's not. Nothing and Just True are incomparable, and Just ⊥ is less defined than Just True.

In the diagrams, "every link between two nodes specifies that the one above is more defined than the one below" (Section 2.2). Should there be a reminder in the section about data types?

-- apfeλmus 10:09, 23 November 2008 (UTC)

[edit] Haskell Recursion Example

I think it might be useful to point out that the "let x = f x in x" construction for the "fix" function actually uses the same least fixpoint semantics under the hoods. Thus "x = f x" semantically means that "x = fix(g)", where g = \x -> f x, leading to x = lfp(f); Thus you are using the same semantics for recursive functions to denote recursive elements.

I think some extra explanation such as above is really useful as I can see many people becoming puzzled by reading this "let x = f x in x" construction because there could be many fixpoint of f and it is not clear that the haskell semantics for functions are the same for these values. jjanssen (talk) 18:51, 2 April 2009 (UTC)

Sounds good. A new subsection on how the discussion applies to Haskell (touching on the examples fib n = fib (n-1) + fib (n-2), fix and let x = f x in) in the recursion chapter is probably the best way to incorporate that.

-- apfeλmus 20:51, 2 April 2009 (UTC)

Talk:Haskell/Denotational semantics

From Wikibooks, the open-content textbooks collection

Contents

[edit] Denotational semantics

[edit] forall a . a

[edit] Mistake in the definition of $\sqsubset$ ?

[edit] Love it!

[edit] Non-strict constructors

[edit] Approximations of the Factorial Function

[edit] Denotional semantics & Equational reasoning

[edit] Continuity

[edit] Not all Functions in Strict Languages are Strict

[edit] Partiality of $\sqsubseteq$ (in "Strict functions")

[edit] Definition of $\sqsubseteq$

[edit] Functions with several Arguments

[edit] `take 3 nats`

[edit] Recursive data types and infinite lists diagram

[edit] Naïve Sets are unsuited for Recursive Data Types

[edit] Is g in section 3.1 a monotone functional?

[edit] Functions `Integer -> Integer` is a (d)cpo

[edit] Why is Nothing less defined than Just True?

[edit] Haskell Recursion Example

Views

Personal tools

Navigation

Search

community

Print/export

Toolbox

Talk:Haskell/Denotational semantics

From Wikibooks, the open-content textbooks collection

Contents

[edit] Denotational semantics

[edit] forall a . a

[edit] Mistake in the definition of ?

[edit] Love it!

[edit] Non-strict constructors

[edit] Approximations of the Factorial Function

[edit] Denotional semantics & Equational reasoning

[edit] Continuity

[edit] Not all Functions in Strict Languages are Strict

[edit] Partiality of (in "Strict functions")

[edit] Definition of

[edit] Functions with several Arguments

[edit] take 3 nats

[edit] Recursive data types and infinite lists diagram

[edit] Naïve Sets are unsuited for Recursive Data Types

[edit] Is g in section 3.1 a monotone functional?

[edit] Functions Integer -> Integer is a (d)cpo

[edit] Why is Nothing less defined than Just True?

[edit] Haskell Recursion Example

Views

Personal tools

Navigation

Search

community

Print/export

Toolbox

[edit] Mistake in the definition of $\sqsubset$ ?

[edit] Partiality of $\sqsubseteq$ (in "Strict functions")

[edit] Definition of $\sqsubseteq$

[edit] `take 3 nats`

[edit] Functions `Integer -> Integer` is a (d)cpo