SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
RK: Every IFF language inductively generates a set of
expressions in the usual way.
<sordid stuff about sorts>
JA: I find it difficult to understand this way of talking.
I will need to ask some questions before I can even hope
to make a translation. Stylistically, it seems to me that
it would be better just to stick to the category-theoretic
language and not drag in all this excess of syntacticism,
which seems to cast a lot of superficial distinctions in
stone and to prevent one from recognizing the underlying
connections.
RK: All references to the current IFF language namespace document at:
RK: http://suo.ieee.org/IFF/metalevel/lower/namespace/type-language/version20021205.pdf.
RK: You and Chris Menzel
(see Chris's message:
http://grouper.ieee.org/groups/suo/email/msg08772.html
and my response:
http://grouper.ieee.org/groups/suo/email/msg08786.html)
keep trying to put me in a linguistic straight-jacket.
I know, I know, I should be more clear and expansive.
More like I'm just trying to escape from mine,
but one good Houdini deserves another in this
Mobiustrip world ...
RK: Although I do not trumpet it for fear of alienating folks, I really intend
the IFF to be as abstract and category-theoretic as possible. And here it
is no different.
Well, it's not the abstract purity that I'm after
so much as the flexibility of application and the
brands of invariance that give you "objectivity".
Will have to put the rest of this on the other burner
until I can get my feet back on the ground with some
more concrete and simple examples.
But just skimming ahead, some of it reminds me of the
Lambek & Scott material, and some of it makes me think
of the Manes & Arbib approach to Program Semantics that
I once studied. Here is a sample of excerpts from that:
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
SEM. Program Semantics
Preface
01. http://suo.ieee.org/ontology/msg03884.html
1. An Introduction to Denotational Semantics
1.1. Syntax and Semantics
02. http://suo.ieee.org/ontology/msg03885.html
03. http://suo.ieee.org/ontology/msg03886.html
04. http://suo.ieee.org/ontology/msg03887.html
1.2. A Simple Fragment of Pascal
05. http://suo.ieee.org/ontology/msg03890.html
06. http://suo.ieee.org/ontology/msg03895.html
07. http://suo.ieee.org/ontology/msg03896.html
08. http://suo.ieee.org/ontology/msg03898.html
09. http://suo.ieee.org/ontology/msg03904.html
10. http://suo.ieee.org/ontology/msg03905.html
1.3. A Functional Programming Fragment
11. http://suo.ieee.org/ontology/msg03906.html
12. http://suo.ieee.org/ontology/msg03909.html
13. http://suo.ieee.org/ontology/msg03910.html
14. http://suo.ieee.org/ontology/msg03911.html
15. http://suo.ieee.org/ontology/msg03912.html
16. http://suo.ieee.org/ontology/msg03915.html
17. http://suo.ieee.org/ontology/msg03919.html
1.4. Multifunctions
18. http://suo.ieee.org/ontology/msg03926.html
19. http://suo.ieee.org/ontology/msg03927.html
20. http://suo.ieee.org/ontology/msg03929.html
1.5. A Preview of Partially Additive Semantics
21. http://suo.ieee.org/ontology/msg03930.html
22. http://suo.ieee.org/ontology/msg03932.html
23. http://suo.ieee.org/ontology/msg03933.html
24. http://suo.ieee.org/ontology/msg03934.html
25. http://suo.ieee.org/ontology/msg03935.html
26. http://suo.ieee.org/ontology/msg03938.html
27. http://suo.ieee.org/ontology/msg03939.html
28. http://suo.ieee.org/ontology/msg03942.html
29. http://suo.ieee.org/ontology/msg03944.html
30. http://suo.ieee.org/ontology/msg03945.html
2. An Introduction to Category Theory
31. http://suo.ieee.org/ontology/msg03946.html
2.1. The Definition of a Category
32. http://suo.ieee.org/ontology/msg03947.html
33. http://suo.ieee.org/ontology/msg03949.html
34. http://suo.ieee.org/ontology/msg03950.html
35. http://suo.ieee.org/ontology/msg03953.html
36. http://suo.ieee.org/ontology/msg03954.html
2.2. Isomorphism, Duality, and Zero Objects
37. http://suo.ieee.org/ontology/msg03955.html
38. http://suo.ieee.org/ontology/msg03956.html
39. http://suo.ieee.org/ontology/msg03958.html
40. http://suo.ieee.org/ontology/msg03960.html
41. http://suo.ieee.org/ontology/msg03963.html
42. http://suo.ieee.org/ontology/msg03977.html
43. http://suo.ieee.org/ontology/msg03979.html
44. http://suo.ieee.org/ontology/msg04013.html
2.3. Products and Coproducts
45. http://suo.ieee.org/ontology/msg04014.html
46. http://suo.ieee.org/ontology/msg04015.html
47. http://suo.ieee.org/ontology/msg04018.html
48. http://suo.ieee.org/ontology/msg04037.html
The above material is excerpted from:
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
[Keep >>>--->>>]
RK: [starting on page 6 op. cit.]
>
> An IFF language L is most definitely intended to be an abstract object.
> It has two components consisting of
> a reference Set-morphism
> refer(L) : var(L) --> ent(L)
> and a signature Set-morphism
> sign(L) : rel(L) --> sign(refer(L))
> which satisfy the pullback constraint
> tgt(sign(L)) = sign(refer(L)).
> We then define the variables, entity types, and relation types to be the
> reference source, reference target, and signature source, respectively
> an variable Set-object var(L) ^= src(refer(L)),
> an entity type Set-object ent(L) ^= tgt(refer(L)),
> a relation type Set-object rel(L) ^= src(sign(L)).
>
> Note, although this has the base category Set, you can lift this to any base
> category that has suitable properties, such as completeness/cocompleteness
> properties, etc.
>
> [starting on page 37 op. cit.]
>
> When I say "inductive" or "recursive", I am still speaking
> category-theoretically. I intend *initial algebras* or *final algebras* or
> whatever is appropriate. As you may know, these have been used in the past
> to specify recursive data structures, such as stacks, queues, automata,
> lists, binary trees, general trees, s-expressions, etc.
>
> But in particular here, to specify expressions we will need to solve a
> recursive set equation involving a particular endofunctor on Set. As usual,
> for initial algebras we need to make sure the endofunctor is appropriately
> cocontinuous, most likely omega-continuous; that is, cocontinuous with
> respect to omega-shaped diagrams in Set.
>
> Now the endofunctor in question has
> the set constant rel(L),
> an isomorphic part for negation,
> products for conjunction, disjunction, implication and equivalence,
> certain kinds of coproducts for the two quantifiers (the case construction),
> and a certain kind of "exponential" for substitution.
>
> These need to be checked for omega-continuity.
>
> Again, you can lift this to any base category that has suitable properties.
>
> We go on to define an expression endofunctor on Language, which is part of a
> (category-theoretic) monad (see Mac Lane CWM chapter VI) on Language with
> the language interpretations being morphisms in the Kleisli category for
> this monad.
>
> Robert E. Kent
> rekent@ontologos.org
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o