objects and messages

[RE01 Rice Brian T. EM2]

>[about declarative programming]
>Yes, we ultimately want some more declarative programming.
>However, there are difficult problems with declarative programming:
>modularity, consistent partial extraction/reification, etc.



>[about syntax]
>syntax matters in as much as we need it to communicate the semantics below.
>textual syntax is sequential just because text is sequential. (btw, it looks
>like some bottleneck forces individual humans to acquire data sequentially).

I'd like to see you're evidence of that bottleneck, especially
considering the multiplicity of ontologies on human actions.  (i.e.
breathing while walking: is it one action or two?)  any bottleneck would
be a society-wide symptom of a disease of the consciousness, and
certainly not worthy of consideration as a Tunes constraint.

>> What are types?
>Usually, they are some "abstract interpretation" of runtime values
>(this is a well-defined term in academia).

(In order to shock you)  Bullshit.  That's relative to an ontology, and
you know it.  We're not here to kow-tow to standards, even if advocated
by academic tradition.  Interpretation can be considered an action of an
object known as the interpreter (not the standard computer term, but the
abstract idea).  In a reflective system, the interpreter is the one
thing which should rarely be a constant.  By changing the interpreter
(reflecting), you will inherently change the meaning of the
'abstraction' action itself.  So, abstraction is not some implicitly
atomic thing with clear meaning.  We're dealing with a system where the
user benefits from having as many conceptual frameworks apply to her/his
goal as is possible.  The last thing they need is to be forced to say
"this is a such-and-such" in order to have it act like a such-and-such.
This is another example of the mis-use of extensionality in order to
require more effort on the part of the user rather than the computer to
resolve meaning.

>(web search keywords: +Patrick +Cousot +abstract +interpretation).
>They may also be considered as a lower approximation
>to the full logical "type" of elements
>(set of logical properties verified by the element).
>In some typed formalisms with decidable ground type verification,
>they can be rather seen as sorts of a many-sorted structure.

How can you advocate a general-programming reflective system where truth
is implicitly absolute?  How then could you define multiple ontologies
and then transform "their truth" into "the truth" for the sake of
argumentation within the system?  These ideas are contradictory.

>> How can we create 'intensional' systems of semantics
>> where referral is never implicit?
>I'm not sure I understand what "referral is never implicit" means exactly.
>Intrinsically, we may only manipulate ground observation, i.e. syntax;
>semantics we observe only indirectly as an epiphenomenon of this syntax.

I'm hypothesizing that intensional systems are capable of generalizing
on the referral mechanism by having it available as a first-order
object.

>The fact that syntax be always a substrate for "computable" manipulations,
>and that in general semantics be not, proves that we can't equate them
>(well, actually, intuitionnist logicians may disagree).
>Also, simple paradoxes show that we always need some external referent;
>a useful logic can't be fully self-contained.

Yes, but what of the nature of the external referent?  Could that be the
essence of user-interface?

>> If so, how can we make it representation-independent?
>At the meta-level, this is just quotienting of syntactic objects
>up to some high-level notion of equivalence.
>Multiple syntaxes or contexts correspond to as many modalities.

Once again, I'm arguing an intensional system where the word "is" would
have no meaning, in the sense of "A is the representation of B" or "A is
an example of B" or "A is the value of B" being absolute statements.

I'd also like to restate Tril's very important question, which I have
also been pondering, "How do you implement lambda-calculus using
lambda-calculus?".  Indeed, how do you implement pi-calculus using
lambda-calculus?  More significantly, how do you pass around types with
uncountably-many axioms using lambda-calculus?  How would
lambda-calculus deal with multiple models of the same system (which
seems to violate the uniqueness of the typing mechanism, or at least
makes types always uncountably large in description size for any object
anywhere)?