"Denotational Semantics" and The Unset State

On gitter.im's red/red/welcome, Nenad Rakocevic said::

"Redbol languages are based on denotational semantics, where the meaning of every expression needs to have a representation in the language itself. Every expression needs to return a value. Without unset! there would be a hole in the language, several fundamental semantic rules would be collapsing, e.g. reduce [1 print ""] => [1] (reducing 2 expressions would return 1 expression)."

I suppose he hasn't read Godel, Escher, Bach.

The fact of the matter is that there is no such thing as a "complete" system. All we do is push complexity around in order to shape the territory to become suitable for our purposes.

Somehow, the idea that reduce [1 print ""] could be an error is by its definition worse than having a block that holds a "unset value".

It's strange how uneducated minds work.

This is correct explanation and Gödel, Escher and Bach have nothing to do with it, they all died long before Rebol was written by Carl Sassenrath. It is of course strange how uneducated minds work, when they can't get correct explanation when they see one.

I don't know what you have to gain by embracing this fallacy.

Variables are "set" or "unset". Not values (at least not the kind of "value" you can put in blocks). All elements in blocks should represent a "set" state.

x: 10
if set? $x [print "The variable is set."]

set $x 20
if set? $x [print "Yup, the variable is still set."]

unset $x
x: ()  ; alternative unset method

if unset? $x [
    print "Now it's unset."
]
if void? ^x [
    print "Here's another way to do it (^x is sorta like 'GET-WORD')"
]

Generic code has to process blocks of values, and it's just not helping anyone when you can put "unset values" in blocks. Imagine enumerating this block, each item stored in a variable as you go. The variable you are using to enumerate the block runs into a problem... it has to hold the current item, yet it also might be unset. Don't you see why this is not right?

2 Likes

This GitHub Issue is one of the many places where you can see Red suffering: `transcode/next` at end-of-input design issue · Issue #5183 · red/red · GitHub

Whereas Ren-C is doing quite well: Incomplete TRANSCODEs: Actually an Optimization Problem

3 Likes

The proof of Ren-C is in that it works, while Red does not.

It's kind of like I have a patent on zero (NULL), negative numbers (QUASIFORM!), and imaginary numbers (antiforms)... and they're trying to do math without them. #goodluckwiththat !

This is the correct explanation:

Red hasn't gotten past multiplication.

I see this argument now and again and it always irritates me. The notion of ‘completeness’ in Gödel’s theorems is, essentially, a statement about what can be proved in formal systems. Nothing more than that. Ren-C can’t be used to write down mathematical proofs, therefore Gödel’s theorems are irrelevant for it. (They’re more relevant for proof languages like Coq or Lean, with their much more elaborate type systems.)

Of course, Ren-C is designed better than Red nonetheless. But this is unrelated to anything Gödel or Hofstadter said.

I think generalized escaping and meta representation, use-mention distinction and self reference, is within the themes of the book...whether it uses the specific theorems or not.

Certainly reading the book would give someone a leg up mentally on addressing the kinds of problems you face when you're pushing things up and down meta levels.

The better analogy is the math one... complex numbers, zero, etc.

Hmm, I guess I can see where you’re coming from. It’s not precisely the same idea but the similarity is there.

(‘Completeness’ really has nothing to do with it, though. I get very annoyed when I see people misusing that term.)

I've mentioned elsewhere that this part is right...

Nenad: "Redbol languages are based on denotational semantics, where the meaning of every expression needs to have a representation in the language itself. Every expression needs to return a value."

...every expression indeed needs to return "a value" (or be divergent, and throw or panic).

It just DOES NOT follow that the language is served by allowing any form of these "values" to be put absolutely anywhere, e.g. as elements of a List.

Nenad: "Without unset! there would be a hole in the language, several fundamental semantic rules would be collapsing, e.g. reduce [1 print ""] => [1] (reducing 2 expressions would return 1 expression)."

This is the part where their religion falls apart.

To ever climb out of that hole, they need to embrace the superior principle:

"There must be a transformation available by which any value can be represented in a List, and a reverse transformation by which that value can be recovered."

Ren-C's "Lifting Ladder" of ANTIFORM => QUASIFORM => QUOTED may not be the only way to accomplish that. But it pulls it off with style and efficiency, in just one byte of the Cell.

The code speaks for itself.