Re: What databases have taught me

Bob Badour wrote:
> I find your terms confused.

I agree and my apologies. Was in a bit of a holiday hurry when I wrote and didn't exercise enough diligence. Let me try to clarify.

Bob Badour wrote:
> Keith H Duggar wrote:
> > 1) All of us agree that there is an unlimited number of
> > consistent operations O that can be defined on a set S.
>
> I am not sure exactly what you mean by 'consistent'. What
> would make 'substring' consistent or inconsistent as an
> operation on an integer data type?

I think what I had in mind when I wrote that was that all operation definitions should be consistent with any axioms stated regarding them. However, since I hadn't even stated I was thinking of type as an algebraic structure and hence no axioms, the adjective doesn't make sense that way either.

> > 2) All of us agree that mathematicians and others often
> > distinguish a subset OA of O as 'axioms'.
> >
> > Let us call OD = O - OA 'derived' operations. And let us
> > call a subset OS of OD 'scoped' operations which are
> > operations that are currently "in scope".
>
> The set OA is useful for deriving S and not for deriving
> O. Calling a set of operations 'derived' does not make
> them derivable. The set O - OA contains many operations
> one cannot derive from OA.

And here too calling those operations 'axioms' doesn't make sense. What I was referring to was the set of operations that are constrained by axioms (in the algebraic structure). What I meant by "derived" operation was any operation whose properties (as in theorems regarding) can be deduced from the axioms that constrain OA. So yeah, you are absolutely right that there are an unlimited number of operations that are not "derived".

> I suggest your use of the term 'derived' reveals a
> preconception that lies at the root of our disagreement.

It seems that it does. I think my preconception is that the only operations which /define/ a type are those that are constrained by a set of axioms either directly (OA) or as a consequence of deduction (OD).

> > 3a) I (and Marshall?) say that S + OA defines a data
> > type T.
>
> I agree that you say that, and I think you say that
> because you assume one can derive all of O from OA.

Which, you are right, is obviously false.

> > 3c) Dmitry says that S + OA + OS defines a data type T.
>
> I have Dmitry killfiled so I don't know all of what he
> says. That seems like a reasonable description based on
> what I have seen others excerpt, though.

Interesting.

> Because computing science, in a sense, is the process of
> building abstract machines and formalisms, the fact that
> one can axiomatize is very useful. The fact that one can
> arbitrarily choose different axiomatizations is useful
> too.

Ok. So it seems we agree that axiomatization is useful. I think I should have just simply said from the start that the definition of "type" that I currently find most useful in programming is "type = algebraic structure". Now, I can't remember if algebraic structures are permitted to have an unlimited number of sets, operations, and axioms. If they are then let me append "with a limited number of sets, operations, and axioms" to the definition.

Which definition(s) do you find more useful? Or what is it about the algebraic structure definition that you find not useful or insufficient?

I recall once you mentioned type theory had failed in some manner. Can you elaborate? Do you know of any alternatives or recent work in type (or category) theory that is doing better and is more useful to computer science?

Thanks!

• Keith -- Fraud 6