NULLs: theoretical problems?

#**181**

On Aug 31, 2:13 am, Jan Hidders <hidd... (AT) gmail (DOT) com> wrote:

Quote:

On 30 aug, 14:08, JOG <j... (AT) cs (DOT) nott.ac.uk> wrote:

I use a similar notion to def in my own work, but am lacking any
references for it. You say that it is an established (or at least
recorded) approach - do you have links to texts, or academic
references? Or does it have a more formal nomenclature that I could
search for > my normally leet googling skills are not serving me well.

I'm sorry to say that at the moment I cannot tell you where I got it.
The thing that comes closest is Beeson's logic of partial terms, which
has an explicit definedness operator for terms. But it lacks the idea
of a syntactic restriction that allows you to keep the normal
reasoning rules of FOL.

"The Foundations of Constructive Mathematics" is not an easy book to
get hold of...

Quote:

Btw. while looking for that I did find in comp.theory a list of
references on logics dealing with undefinedness. It's probably not
useful to you because more than you asked for, but I'm giving it
anyway:

http://groups.google.com/group/comp....4efa5e74a5f68e

thanks for these. Much appreciated.

Quote:

Of course, if you really want a formal reference I might consider
writing a small technical report about it. ;-)

I think you should make this a priority! Oh, and don't forget to
mention me in the acknowledgements as a motivating factor in its
generation

Quote:

Kind regards,

-- Jan Hidders

"...not even with these (contraries 'Socrates is well' and 'Socrates
is sick') is it necessary always for one to be true and the other
false. For if Socrates exists one will be true and the other false,
but if he does not both will be false... "
(Aristotle, Categories, x, 13b12)

Its good to know we've only been thinking about these concepts for
2300 years...

#**182**

JOG wrote:

Quote:

On Aug 31, 2:13 am, Jan Hidders <hidd... (AT) gmail (DOT) com> wrote:

On 30 aug, 14:08, JOG <j... (AT) cs (DOT) nott.ac.uk> wrote:

I use a similar notion to def in my own work, but am lacking any
references for it. You say that it is an established (or at least
recorded) approach - do you have links to texts, or academic
references? Or does it have a more formal nomenclature that I could
search for > my normally leet googling skills are not serving me well.

I'm sorry to say that at the moment I cannot tell you where I got it.
The thing that comes closest is Beeson's logic of partial terms, which
has an explicit definedness operator for terms. But it lacks the idea
of a syntactic restriction that allows you to keep the normal
reasoning rules of FOL.

"The Foundations of Constructive Mathematics" is not an easy book to
get hold of...

Btw. while looking for that I did find in comp.theory a list of
references on logics dealing with undefinedness. It's probably not
useful to you because more than you asked for, but I'm giving it
anyway:

http://groups.google.com/group/comp....4efa5e74a5f68e

thanks for these. Much appreciated.

Of course, if you really want a formal reference I might consider
writing a small technical report about it. ;-)

I think you should make this a priority! Oh, and don't forget to
mention me in the acknowledgements as a motivating factor in its
generation

Kind regards,

-- Jan Hidders

"...not even with these (contraries 'Socrates is well' and 'Socrates
is sick') is it necessary always for one to be true and the other
false. For if Socrates exists one will be true and the other false,
but if he does not both will be false... "
(Aristotle, Categories, x, 13b12)

Its good to know we've only been thinking about these concepts for
2300 years...

.... or longer.

#**183**

On 31 aug, 17:21, JOG <j... (AT) cs (DOT) nott.ac.uk> wrote:

Quote:

On Aug 31, 2:13 am, Jan Hidders <hidd... (AT) gmail (DOT) com> wrote:

On 30 aug, 14:08, JOG <j... (AT) cs (DOT) nott.ac.uk> wrote:

I use a similar notion to def in my own work, but am lacking any
references for it. You say that it is an established (or at least
recorded) approach - do you have links to texts, or academic
references? Or does it have a more formal nomenclature that I could
search for > my normally leet googling skills are not serving me well.

I'm sorry to say that at the moment I cannot tell you where I got it.
The thing that comes closest is Beeson's logic of partial terms, which
has an explicit definedness operator for terms. But it lacks the idea
of a syntactic restriction that allows you to keep the normal
reasoning rules of FOL.

"The Foundations of Constructive Mathematics" is not an easy book to
get hold of...

There's a nice short and clear description in:

http://www.iam.unibe.ch/publikatione...001/iam-01-005

Quote:

Of course, if you really want a formal reference I might consider
writing a small technical report about it. ;-)

I think you should make this a priority! Oh, and don't forget to
mention me in the acknowledgements as a motivating factor in its
generation

Will do. ;-)

-- Jan Hidders

#**184**

Jan Hidders <hidders (AT) gmail (DOT) com> wrote in news:1188523367.163903.141220
@m37g2000prh.googlegroups.com:

Quote:

On 30 aug, 06:12, "V.J. Kumar" <vjkm... (AT) gmail (DOT) com> wrote:

What you are proposing here is a Z crowd way to handle undefinedness,
one of many really. It's an old, very well know approach called "all
predicates denote" that some like and some others dislike.

As far as I can see it isn't. I first thought you were right, (hence
my previous reply, although I'm still not claiming this is something
original) but since Jim asked me about it I read it back, and as far
as I can tell they don't have a corresponding notion of syntactical
restriction which is pretty much at the core of the approach I'm
talking about. So could you give a concrete reference and maybe a
short explanationa of why you think it is the same?

Your current disagreement plus, especially, your talking about non-
commutativity prodded me to strain my memory and recall a real fossil,
some book by Gries, or Dijkstra or both. He/they wrote it when I was
probably in the kindergarten. Anyway, he used those non-commutative
'cand', 'cor' and so forth to "guard" against undefined values:

'defined(x) cand MyPredicate(x)'

gives exactly what you wrote about including this nice non-commutativity
plus some other gems like need to have two packs of connectives, the
normal ones plus the conditional beasts. So, yes, I was wrong, your
ideas are perhaps closest/the same to/as the cand/cor/etc stuff.

In comparison to "conditionals", partial logic is a thing of beauty
since it is almost classical predicate calculus with weird equality or
definednes predicate. No need to kill commutativity or anything like
that.

IMNSHO, partial logic is still worse than a three-valued way for
undefinedness for the reasons I mentioned earlier.

Quote:

-- Jan Hidders

#**185**

Jan Hidders wrote:

Quote:

On 31 aug, 17:21, JOG <j... (AT) cs (DOT) nott.ac.uk> wrote:

On Aug 31, 2:13 am, Jan Hidders <hidd... (AT) gmail (DOT) com> wrote:

On 30 aug, 14:08, JOG <j... (AT) cs (DOT) nott.ac.uk> wrote:

I use a similar notion to def in my own work, but am lacking any
references for it. You say that it is an established (or at least
recorded) approach - do you have links to texts, or academic
references? Or does it have a more formal nomenclature that I could
search for > my normally leet googling skills are not serving me well.

I'm sorry to say that at the moment I cannot tell you where I got it.
The thing that comes closest is Beeson's logic of partial terms, which
has an explicit definedness operator for terms. But it lacks the idea
of a syntactic restriction that allows you to keep the normal
reasoning rules of FOL.

"The Foundations of Constructive Mathematics" is not an easy book to
get hold of...

There's a nice short and clear description in:

http://www.iam.unibe.ch/publikatione...001/iam-01-005

Of course, if you really want a formal reference I might consider
writing a small technical report about it. ;-)

I think you should make this a priority! Oh, and don't forget to
mention me in the acknowledgements as a motivating factor in its
generation

Will do. ;-)

-- Jan Hidders

Oh, you publication whores, you!

#**186**

Jon Heggland wrote:

Quote:

Keith Duggar wrote:

I'm not trying to have anything. I'm trying to understand what
the "write DEF" prescription buys us over say the "Interactive
Mathematical Proof System" of Farmer, Guttman, and Thayer that
has exactly the property I described that any formula is false
if any variable is NULL. Again, I am failing to grasp what the
"write DEF" prescription buys us. I would like to understand.

In this system, how can you check whether a given variable actually is
NULL or not?

I'm not so sure what you mean by "check". Any proposition in
IMPS is FALSE if any of its arguments is undefined. So as an
example (x OR TRUE) is false if x is NULL. Does this suffice
for what you mean by "check"?

KHD

#**187**

Bob Badour wrote:

Quote:

Keith Duggar wrote:

I'm not trying to have anything. I'm trying to understand what
the "write DEF" prescription buys us over say the "Interactive
Mathematical Proof System" of Farmer, Guttman, and Thayer that
has exactly the property I described that any formula is false
if any variable is NULL. Again, I am failing to grasp what the
"write DEF" prescription buys us. I would like to understand.

KHD

Error detection. It forces one to acknowledge that one understands the
attribute can be undefined and that one is ignoring those propositions
for which it is undefined.

So one kind of error detection it allows is checking that a
user understands an attribute can be undefined? How helpful
would that be in preventing common query errors? Or does it
allow error detection beyond NULL understanding checks?

Thanks for help.

KHD

#**188**

Keith H Duggar wrote:

Quote:

Bob Badour wrote:

Keith Duggar wrote:

I'm not trying to have anything. I'm trying to understand what
the "write DEF" prescription buys us over say the "Interactive
Mathematical Proof System" of Farmer, Guttman, and Thayer that
has exactly the property I described that any formula is false
if any variable is NULL. Again, I am failing to grasp what the
"write DEF" prescription buys us. I would like to understand.

KHD

Error detection. It forces one to acknowledge that one understands the
attribute can be undefined and that one is ignoring those propositions
for which it is undefined.

So one kind of error detection it allows is checking that a
user understands an attribute can be undefined? How helpful
would that be in preventing common query errors? Or does it
allow error detection beyond NULL understanding checks?

Thanks for help.

KHD

It would be very helpful. Take my favourite example:

SUM(A) + SUM(B) = SUM(A+B)

The above identity does not hold in SQL.

(SELECT SUM(A) FROM T) + (SELECT SUM(B) FROM T)
does not equal (SELECT SUM(A+B) FROM T)
because the terms are really:

SELECT SUM(A) FROM T WHERE DEF T.A : TRUE

SELECT SUM(B) FROM T WHERE DEF T.B : TRUE

SELECT SUM(A+B) FROM T WHERE DEF T.A AND DEF T.B : TRUE

Being forced to acknowledge the potentially undefined highlights the
difference. While that is just one example of a common pitfall, I use it
because the accountants don't like it when the numbers don't balance.

To balance, one really has to write the original identity as:
SUM(ISNULL(A,0)) + SUM(ISNULL(B,0)) = SUM(ISNULL(A,0) + ISNULL(B,0))

(Presumably under Jan's model a similar ISUNDEF or COALESCE operator
will exist.)

SQL doesn't give a warning or an error. It just returns incorrect
answers, and naive users are reassured that SQL handles missing
information because it has NULL.

While it might be tedious to do it right the first time, it costs the
organization a whole lot more when the external auditor complains than
when the compiler complains.

#**189**

paul c wrote:

Quote:

Bob Badour wrote:
...

While it might be tedious to do it right the first time, it costs the
organization a whole lot more when the external auditor complains than
when the compiler complains.

The cynical view is that once one problem is removed, the auditors will
find another in order to justify their existence. Still, I suspect most
auditors are willing puppets of the SQL lobby, just as insidious in its
way as the auto lobby.

It's much better if they justify their existence catching the occasional
embezzler or lost receipt than meeting with the C-levels to discuss the
meaningless discrepancy on some marginally relevant report.

#**190**

Bob Badour wrote:

Quote:

Keith H Duggar wrote:
Bob Badour wrote:

Keith Duggar wrote:

I'm not trying to have anything. I'm trying to understand what
the "write DEF" prescription buys us over say the "Interactive
Mathematical Proof System" of Farmer, Guttman, and Thayer that
has exactly the property I described that any formula is false
if any variable is NULL. Again, I am failing to grasp what the
"write DEF" prescription buys us. I would like to understand.

KHD

Error detection. It forces one to acknowledge that one understands the
attribute can be undefined and that one is ignoring those propositions
for which it is undefined.

So one kind of error detection it allows is checking that a
user understands an attribute can be undefined? How helpful
would that be in preventing common query errors? Or does it
allow error detection beyond NULL understanding checks?

Thanks for help.

KHD

It would be very helpful. Take my favourite example:

SUM(A) + SUM(B) = SUM(A+B)

The above identity does not hold in SQL.

(SELECT SUM(A) FROM T) + (SELECT SUM(B) FROM T)
does not equal (SELECT SUM(A+B) FROM T)
because the terms are really:

SELECT SUM(A) FROM T WHERE DEF T.A : TRUE

SELECT SUM(B) FROM T WHERE DEF T.B : TRUE

SELECT SUM(A+B) FROM T WHERE DEF T.A AND DEF T.B : TRUE

Being forced to acknowledge the potentially undefined highlights the
difference. While that is just one example of a common pitfall, I use it
because the accountants don't like it when the numbers don't balance.

To balance, one really has to write the original identity as:
SUM(ISNULL(A,0)) + SUM(ISNULL(B,0)) = SUM(ISNULL(A,0) + ISNULL(B,0))

(Presumably under Jan's model a similar ISUNDEF or COALESCE operator
will exist.)

SQL doesn't give a warning or an error. It just returns incorrect
answers, and naive users are reassured that SQL handles missing
information because it has NULL.

While it might be tedious to do it right the first time, it costs the
organization a whole lot more when the external auditor complains than
when the compiler complains.

Ok, I think I'm seeing the point now. Please follow me through a
hypothetical scenario to see if I get the point.

Suppose in version 1 of a database schema A and B are defined as
NOT-NULL. A muggle is tasked with writing a function that a some
point computes the sum you described above:

SELECT SUM(A+B) FROM T

All is well, accounts balance. Then database schema version 1.01
comes along and removes the NOT-NULL constraints on A and B. Now
users might input NULL for one or both attributes.

The SQL DBMS goes merrily about it's way until one day a NULL is
entered. Bang! Accounts don't balance auditors from the ministry
of magical database management apparate in. Not good.

Had they used Jan's DBMS the compiler would have issued a static
diagnostic along the lines of "ERROR : A and B may be undefined"
forcing the maintainers to examine the code and choose one of:

1)

SELECT SUM(ISNULL(A,0) + ISNULL(B,0)) FROM T

2)

SELECT SUM(A+B) FROM T WHERE DEF T.A AND DEF T.B : TRUE

where under 1) accounts balance and under 2) they do not balance
but the maintainers chose this (or were drinking butter beers on
the job) so the DBMS happily obliges.

Is that the point?

Now for LUTINS (the logic of the "Interactive Mathematical Proof
System") instead of being a static type error the runtime result
of the SUM(A+B) function would be NULL. Of course similar syntax
to 1) and 2) would allow you to code the desired runtime result.
The key difference is static vs dynamic error detection correct?

KHD