On Sat, Dec 24, 2011 at 8:20 PM, Alexander Solla <alex.so...@gmail.com>wrote:
> > > On Wed, Dec 21, 2011 at 8:39 PM, MigMit <miguelim...@yandex.ru> wrote: > >> >> On 22 Dec 2011, at 06:25, Alexander Solla wrote: >> >> > Denotational semantics is unrealistic. >> >> And so are imaginary numbers. But they are damn useful for electrical >> circuits calculations, so who cares? >> > > Not a fair comparison. Quaternions are not particularly useful for > electrical circuits, because it is unrealistic to apply a four-dimensional > construct to two-dimensional phase spaces. In the same way, denotational > semantics adds features which do not apply to a theory of finite > computation. > > >> >> > The /defining/ feature of a bottom is that it doesn't have an >> interpretation. >> > >> What do you mean by "interpretation"? >> > > You know, the basic notion of a function which maps syntax to concrete > values. > > http://en.wikipedia.org/wiki/Model_theory > > > >> >> > They should all be treated alike, and be treated differently from every >> other Haskell value. >> >> But they ARE very similar to other values. They can be members of >> otherwise meaningful structures, and you can do calculations with these >> structures. "fst (1, _|_)" is a good and meaningful calculation. > > > Mere syntax. What is fst doing? It computes "forall (x,y) |- x". Using > the language of model theory, we can say that Haskell computes an > interpretation "forall (x,y) |= x". It is _|_ that lacks an intepretation, > not fst. We can see that by trying > "fst (_|_,1), which reduces to _|_ by the proof rule for fst. _|_ lacks > an interpretation, so the run-time either loops forever or throws an error > (notice that error throwing is only done with compiler magic -- if you > define your own undefined = undefined, using it will loop. GHC is > specially trained to look for Prelude.undefined to throw the "undefined" > error.) > > >> > Every other Haskell value /does/ have an interpretation. >> >> So, (_|_) is bad, but (1, _|_) is good? > > > I did not introduce "good" and "bad" into this discussion. I have merely > said (in more words) that I want my hypothetical perfect language to prefer > OPERATIONAL (model) SEMANTICS for a typed PARACONSISTENT LOGIC over the > DENOTATIONAL SEMANTICS which the official documentation sometimes dips into. > > Using examples from denotational semantics is not going to change my mind > about the applicability of one or the other. It is clear that denotational > semantics is a Platonic model of constructive computation. > > You make it sound as though platonism is somehow bad. Before we get into that lets look at a capsule of our history: Kronecker and Cantor disagree on whether sets exist. K: God created the natural numbers; all the rest is the work of man. C: All manner of infinite sets exist (presumably in the mind of God?) A generation later and continuing, Hilbert and Brouwer disagree on what constitutes a proof. A little later Goedel sets out to demolish Hilbert's formalist agenda. The (interpretations of) Hilbert's philosophical position is particularly curious: For Brouwer, Hilbert is wrong because he is a platonist -- believes in completed infinities For Goedel, Hilbert is wrong because he is not a platonist -- he is looking for mechanizable proofs. Talk of two stools!! Turing tries to demolish Goedel. His real intention is AI not the Turing machine. He does not succeed -- simple questions turn out to be undecidable/non-computable. However a 'side-effect' (ahem) of his attempts via the TM is ... the computer. That Goedel was a (mostly closet) platonist: http://guidetoreality.blogspot.com/2006/12/gdels-platonism.html Am I arguing that platonism is good? Dunno... I am only pointing out that the tension between platonism and its opponents (formalist, empiricist, constructivist etc) is evidently a strong driver for progress BTW a more detailed look at the historical arguments would show that the disagreements were more violent than anything on this list :-) Hopefully on this list we will be cordial and wish each other a merry Christmas!
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
