Scheme - why Bill-semantics is not DS

Author

why Bill-semantics is not DS

William D Clinger

2004-07-14, 8:58 pm

Introduction
------------

Bill Richter has argued that small-step operational semantics are
compositional, and should therefore be regarded as denotational.
Furthermore he argues that this approach, called Bill-semantics
to distinguish it from a real denotational semantics, is simpler
because it doesn't involve any domain theory.

Because small-step operational semantics are not compositional in
the generally accepted meaning of that term, Bill has adopted the
following definitions, which are based on Theorem 3.13 in David A.
Schmidt's textbook on denotational semantics [Schmidt].

Bill's Definitions
------------------

Suppose the abstract syntax of a programming language L is generated
by a context-free grammar G with nonterminals B_1 through B_n and
productions

B_i ::= Option_i1 | ... | Option_im_i

Let S_ij1 through S_ijk be the nonterminals that appear in Option_ij.

Definition. A Bill-semantics is a semantics that defines a semantic
domain D_i for each nonterminal B_i and a set of valuation functions

E_i: L(B_i) --> D_i

where L(B_i) is the language generated by nonterminal B_i.

Definition. A Bill-semantics is Bill-compositional if there exists
a family of functions

f_ij: D_ij1 x ... x D_ijk --> D_i

where D_ijl is the semantic domain corresponding to the nonterminal
S_ijl, such that each E_i is equal to the corresponding

B_i: L(B_i) --> D_i

that is uniquely defined by structural induction using the equations

B_i [ Option_ij ] = f_ij (B_ij1 (S_ij1), ..., B_ijk (S_ijk))

where B_ijl is the B_i that corresponds to nonterminal S_ijl.

Definition. Any old semantics s: L --> D is Bill-compositional if
there exists a Bill-compositional Bill-semantics such that s is one
of the valuation functions E_i defined by the Bill-semantics.

We will now define the syntax and several different varieties of
semantics for a toy programming language.

Abstract Syntax
---------------

M ::= V | (A M M) | (ifzero? M M M) | (M M)

V ::= n | x | (lambda (x) M)

A ::= + | - | *

n ::= 0 | pos | -pos

pos ::= d | pos 0 | pos d

d ::= 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

x ::= z pos

The productions for numerals n and variables x would normally be
omitted, but this has led to confusion so they are shown above.
The unusual productions for n ensure a bijection between numerals
and integers.

Examples may use variable names like x, y, and z as abbreviations
for z24, z25, and z26.

Denotations of Numerals and Variables
-------------------------------------

The standard denotations of numerals, digits, and variables are
defined compositionally (i.e. by structural induction) from

E_n [ 0 ] = 0
E_n [ pos ] = E_pos [ pos ]
E_n [ -pos ] = - E_pos [ pos ]

E_pos [ d ] = E_d [ d ]
E_pos [ pos 0 ] = 10 * E_pos [ pos ]
E_pos [ pos d ] = 10 * E_pos [ pos ] + E_d [ d }

E_d [ 1 ] = 1
...
E_d [ 9 ] = 9

E_x [ z pos ] = x_{E_pos [ pos ]}

Let Num: Z --> L(n) and Var: { x_i } --> L(x) be the unique total
functions such that

E_n [ Num(z) ] = z

E_x [ Var(x_i) ] = x_i

Contexts and Redexes
--------------------

The following productions define contexts and redexes.

C ::= [] | (A C M) | (A V C) | (ifzero? C M M) | (C M) | (V C)

R ::= (A V V) | (ifzero? V M M) | (V V)

Lemma. If m is a value V, then there do not exist a context c and
a redex r such that m = c[r].

Proof: By examination of the productions for V and C, the only
possibility is that c is []. This would imply m = r, but no value
is itself a redex.
QED

Theorem. If m is a term M, then m is a value V or else there exists
a unique context c and a unique redex r such that m = c[r].

Proof: By structural induction on M. In the base case, m is a value V.
For the induction cases, suppose the theorem holds for all subterms of m.

If m = (a m1 m2), there are three subcases.

If both m1 and m2 are values, then c is [] and r is m. Neither m1 nor m2
can be decomposed into a reduction context and redex, so this decomposition
is unique.

If m1 is not a value, let m1 = c1[r1] be the unique decomposition of m1.
Then c is (a c1 m2), and m = c[r1] is the unique decomposition of m.

If m1 is a value but m2 is not, let m2 = c2[r2] be the unique decomposition
of m2. Then c is (a m1 c2), and m = c[r2] is the unique decomposition of m.

If m = (ifzero? m0 m1 m2), and m0 is a value, then c is [] and r is m;
m0 cannot be decomposed, so this decomposition is unique. If m0 is not
a value, let m0 = c0[r0] be the unique decomposition of m0. Then c is
(ifzero? c0 m1 m2), and m = (ifzero? c0[r0] m1 m2) is the unique
decomposition of m.

If m = (m1 m2), then the proof is essentially the same as for (a m1 m2).

End of proof.

Reduction
---------

The one-step reduction relation -> is defined as follows.

(a v1 v2) -> 0 if v1 or v2 is not a numeral

(+ n1 n2) -> Num (E_n[n1] + E_n[n2])
(- n1 n2) -> Num (E_n[n1] - E_n[n2])
(* n1 n2) -> Num (E_n[n1] * E_n[n2])

(ifzero? 0 m1 m2) -> m1
(ifzero? v m1 m2) -> m2 if v is not 0

(v1 v2) -> 0 if v1 is not a lambda term

((lambda (x) m) v2) -> m[v2/x] with alpha-conversion as necessary

If r -> m, then c[r] -> c[m].

Operational Semantics
---------------------

Let ->* be the transitive closure of ->.

The operational semantics of a term m is os[[ m ]], where os[[ . ]] is
defined by

os [[ m ]] = v if m ->* v
os [[ m ]] = bottom otherwise

Note that os[[ . ]] is a total function from M to Z_bottom, but it
is not a computable function.

Bill-semantics
--------------

The Bill-semantics uses a new nonterminal P, which stands for a
complete program. For convenient reference, we repeat the other
relevant productions as well:

P ::= M

M ::= V | (A M M) | (ifzero? M M M) | (M M)

V ::= n | x | (lambda (x) M)

A ::= + | - | *

The valuation functions are

E_P: P --> Z_bottom

E_M: M --> M

E_V: V --> V

defined by structural induction from

E_P [[ m ]] = os [[ E_M[[ m ]] ]]

E_M [[ v ]] = E_V[[ v ]]

E_M [[ (a m1 m2) ]] = (a E_M [[ m1 ]] E_M [[ m2 ]])

E_M [[ (ifzero? m0 m1 m2) ]]
= (ifzero? E_M [[ m0 ]] E_M [[ m1 ]] E_M [[ m2 ]])

E_M [[ (m1 m2) ]] = (E_M [[ m1 ]] E_M [[ m2 ]])

E_V [[ n ]] = Num(E_n[n])

E_V [[ x ]] = Var(E_x[x])

E_V [[ (lambda (x) m) ]] = (lambda (E_V [[ x ]]) E_M [[ m ]])

Bill-compositionality
---------------------

Theorem. The Bill-semantics shown above is Bill-compositional.

Proof: Immediate by the definition of Bill-compositionality. QED

Lemma. E_M and E_V are the identity functions on M and V, respectively.

Proof: By simultaneous structural induction on M and V. QED

Corollary. For any term m, E_P [[ m ]] = os [[ m ]].

Therefore the original operational semantics is Bill-compositional.

Analysis
--------

From the above, it is obvious that *any* small-step operational
semantics can be formulated as a Bill-compositional Bill-semantics.
All we need is one new nonterminal, whose valuation function is
defined to be the total, non-computable function os [[.]] defined
by the operational semantics. The other valuation functions are
identity functions whose only purpose is to fulfill the formal
requirements of Bill-compositionality.

The fact that these identity functions can be defined by structural
induction over syntax does not imply that os [[.]] can be defined
by structural induction over syntax.

Therefore the Bill-compositionality of os [[.]] does not imply
that os [[.]] is compositional.

It should also be apparent that this kind of Bill-compositional
Bill-semantics offers no advantages over a small-step operational
semantics.

In particular, no two subphrases of a program will have the same
meaning unless they are syntactically identical. For example, the
meaning of the term (+ 1 2) has nothing to do with the meaning of
the term (+ 2 1), despite the fact that these terms would have
exactly the same meaning when considered as programs.

In other words, the Bill-semantics is not very abstract at all.

Full Abstraction
----------------

Suppose we have both an operational and a denotational semantics
for some language. We would like for these two semantics to
have something to do with each other.

For example, it seems like two terms should have the same denotation
if and only if they behave the same in all contexts. This property
is called full abstraction.

Definition. The denotational semantics ds[[.]] is fully
abstract if, for every pair of terms m1 and m2,

ds [[ m1 ]] = ds [[ m2 ]

if and only if

for all contexts c, os [[ c[m1] ]] = os [[ c[m2] ]].

Theorem. The Bill-semantics defined above is fully abstract.

Proof. E_M [[ m1 ]] = m1 and E_M [[ m2 ]] = m2. m1 and m2
are just syntax, so m1 = m2 means m1 and m2 are syntactically
equal. If they are syntactically equal, then

os [[ c[m1] ]] = os [[ c[m2] ]]

That takes care of the forward implication. For the reverse,
consider the context c = (lambda (x) []). By definition of os[[.]],

os [[ c[m1] ]] = (lambda (x) m1)

os [[ c[m2] ]] = (lambda (x) m2)

If these values are equal, then m1 = m2 as syntax, which implies
E_M [[ m1 ]] = E_M [[ m2 ]].

End of proof.

In other words, one of the most un-abstract semantics that could
be imagined is fully abstract. Examples like this are part of
the reason full abstraction is no longer regarded as a terribly
useful concept.

It turns out that full abstraction is more easily achieved by
making the operational semantics *less* abstract than by making
the denotational semantics *more* abstract. Hence a fully
abstract pair of semantics is likely to be *less* abstract than
a pair of semantics that are *not* fully abstract.

Beyond Full Abstraction
-----------------------

We can make our operational semantics more abstract by hiding
information. Let the more abstract operational semantics of a
term m be os2[[ m ]], where os2[[ . ]] is defined by

os2 [[ m ]] = n if m ->* n
os2 [[ m ]] = bottom if m ->* x
os2 [[ m ]] = bottom if m ->* (lambda (x) m1)
os2 [[ m ]] = bottom otherwise

Our Bill-semantics is not fully abstract with respect to this
more abstract operational semantics, but that's to be expected.
Our Bill-semantics was defined in terms of the less abstract
operational semantics.

What if we use os2 instead of os to define the Bill-semantics?

That Bill-semantics still won't be fully abstract. For example,
(lambda (x) (+ 1 2)) and (lambda (x) (+ 2 1)) will behave the
same in all contexts, but their denotations will be different.

Is it possible to define a denotational semantics that is fully
abstract with respect to os2?

Tricky question. We'll have to think about that a bit.

Maybe we should start by trying to come up with a Bill-semantics
that assigns the same meaning to (lambda (x) (+ 1 2)) and to
(lambda (x) (+ 2 1)).

Will

Bill Richter

2004-07-16, 3:57 am

cesuraSPAM@verizon.net (William D Clinger) wrote:

Will, this is great, even though you don't capture my work. But you
seem to have replicated my feat: turning OpS into Bill-compositional
semantic functions. The only thing you're missing is why
Bill-compositionality = c.l.s-compositionality, but maybe we can get
there from here, now that you've proved a result up my alley.

I worked my way through your proof of Bill-compositionality, with
mucho strugglings (see below) and I'll cut to the chase right here:

Analysis
--------

From the above, it is obvious that *any* small-step operational
semantics can be formulated as a Bill-compositional Bill-semantics.

That's a nice proof, but I didn't and can't use your proof, because of
the difference between my syntactic domain Exp and my "hybrid" set
LC_v Exp, which is Exp modulo alpha equivalence.

That is, F-F show that their partial function eval_v^s defined on LC_v
Exp captures pure define-less Scheme. That's a deep result, which I
piggyback on. Their standard reduction arrow |-->_v certainly sounds
like OpS, but it's not defined on
Exp,
but LC_v Exp instead.

If you claim that F-F could've re-done things so that their arrows
|-->_v & eval_v^s are defined on Exp (i.e. no alpha modding), then you
know more about it than me. I certainly couldn't prove it, and I'm
not sure it's true. My understanding of F-F's notes requires the deep
fact that beta_v reduction makes sense modulo alpha-equivalence,
because I think you need that to prove that the Y_v combinator gives a
fixed point operator, and that's where recursion comes from in LC_v.

But this is a technical objection. Perhaps you know of other
languages with small-step reduction arrow strictly on Exp. And then
your proof works fine.

All we need is one new nonterminal, whose valuation function is
defined to be the total, non-computable function os [[.]] defined
by the operational semantics. The other valuation functions are
identity functions whose only purpose is to fulfill the formal
requirements of Bill-compositionality.

Right! Just take all your other syntactic domains and denote them by
the identity, including M in Exp, and throw in P ::= M! Then
compositionality amounts to nothing but your equation

E[[ m ]] = os[ m ]

That's great! I keep saying I respect your skills, and this
definitely deserves respect. I wouldn't have seen this.

The fact that these identity functions can be defined by structural
induction over syntax does not imply that os [[.]] can be defined
by structural induction over syntax.

Correct.

Therefore the Bill-compositionality of os [[.]] does not imply
that os [[.]] is compositional.

Correct. I hope you're not going to then claim that
Bill-compositionality is different from c.l.s.-compositionality.

Now I don't do things your way, but I certainly never claimed that my
(non-semantic) function

E: LC_v Exp ---> Value_bottom

was compositional, and I don't even know what that might mean, since
we've modded out by alpha equivalence.

It should also be apparent that this kind of Bill-compositional
Bill-semantics offers no advantages over a small-step operational
semantics.

In your case, that sounds true! For me, that's not quite fair.
First, I demand, as a non-paid member of my Pure Math tribe, to have
total functions such as my semantic function

EE_1: Exp ---> Value_bottom

That doesn't rule out your work. But furthermore, I was forced to
prove a result which looks obvious, but the 2nd took me 7 hours to
post it, I errata-ed twice, and I'm still not happy with the proof:

E[(op M N)] = op( E[M], E[N] )

E[(M N)] = Phi( E[M], E[N] )

where my Phi = f_14 was defined in terms of E. To me, this is an
important fact about Scheme: to evaluate a combination, we evaluate
the arguments, and the 1st argument must return a function which we
then apply to the value of the other argument. That's a really

fact about Scheme, it's what makes Scheme semantics so "simple": it's
mostly just this one rule! And I had to fight my way through it. You
did not, with your derivation below.

In particular, no two subphrases of a program will have the same
meaning unless they are syntactically identical.

I think that's true for you, but not for me.

For example, the meaning of the term (+ 1 2) has nothing to do with
the meaning of the term (+ 2 1), despite the fact that these terms
would have exactly the same meaning when considered as programs.

Did you say what you meant? I think you meant to compare the
subphrases of the two "programs"

X = (+ (+ 5 6) 7)

Y = (+ 11 7)

You're saying that even though

E_P[[ (+ (+ 5 6) 7) ]] = E_P[[ (+ 11 7) ]] = 18

it's not true that

E_M[[ (+ 5 6) ]] = E_M[[ 11 ]]

because (+ 5 6) != 11

For me, that isn't true: EE_1[[ (+ 5 6) ]] = EE_1[[ 11]], and we have

EE_1[[ (+ (+ 5 6) 7) ]] = +( E[ (+ 5 6) ], E[7]) = +( E[ 11 ], E[7])

= +(11, 7) = 18

In other words, the Bill-semantics is not very abstract at all.

Obviously my Bill-semantics is more abstract than yours, but how much
more? Would you want even more?

Introduction
------------

Bill Richter has argued that small-step operational semantics are
compositional,

Certainly not in general, this is your result. Just Scheme for me.

and should therefore be regarded as denotational.

No, Shriram talked me out of that. As I understood Shriram, DS is a
human field, with certain practices, e.g. Scott models, and so my work
ought to fit into the other field OpS.

Furthermore he argues that this approach, called Bill-semantics to
distinguish it from a real denotational semantics, is simpler
because it doesn't involve any domain theory.

I think I said that, and below you kinda show that approach is not
what I meant at all. Thanks. I guess I'd say that I like my
Bill-compositional-semantics, which is not yours below, because it's
making total functions out of LC_v, plus proving the important
Scheme-like compositionality equations. That is, I like all 3
ingredients, and you've shown how to get Bill-compositional-semantics
with just the 1st ingredient: total functions.

Because small-step operational semantics are not compositional in
the generally accepted meaning of that term,

Now I still claim that's false, and now maybe we can go through my
proof that any Bill-compositional-semantics is c.l.s-compositional.

Now it's all boring technical objections to something I don't
understand real well:

Bill has adopted the following definitions, which are based on
Theorem 3.13 in David A. Schmidt's textbook on denotational
semantics [Schmidt].

Bill's Definitions
------------------

Suppose the abstract syntax of a programming language L is
generated by a context-free grammar G with nonterminals B_1 through
B_n and productions

B_i ::= Option_i1 | ... | Option_im_i

Let S_ij1 through S_ijk be the nonterminals that appear in
Option_ij.

Does Schmidt say "context-free grammar"? That's good you said
Option_{i, m_i}, but then you should also have said
S_ij1 through S_{i,j,k_ij}, and of course we can have k_ij = 0,
i.e. Option_ij can be a terminal symbol.

Definition. A Bill-semantics

OK, if you're gonna use Joe's term, we won't say BS, all right?

is a semantics that defines a semantic domain D_i for each
nonterminal B_i and a set of valuation functions

E_i: L(B_i) --> D_i

where L(B_i) is the language generated by nonterminal B_i.

I assume L(B_i) is Schmidt's syntactic domain B_i. As Schmidt defines
B_i to be a domain, I disliked his BNF B_i ::= .... So you've solved
this overloading of B_i in a different way? Fine.

Definition. A Bill-semantics is Bill-compositional if there exists
a family of functions

f_ij: D_ij1 x ... x D_ijk --> D_i

where D_ijl is the semantic domain corresponding to the nonterminal
S_ijl,

again, that should be D_{i,j,k_ij}, and if k_ij = 0, then we
understand this product to be a 1-point set, so that we really have

f_ij in D_i.

such that each E_i is equal to the corresponding

B_i: L(B_i) --> D_i

that is uniquely defined by structural induction using the equations

B_i [ Option_ij ] = f_ij (B_ij1 (S_ij1), ..., B_ijk (S_ijk))

where B_ijl is the B_i that corresponds to nonterminal S_ijl.

That's not either my definition or the c.l.s def. What you wrote down
is the c.l.s. accepted definition of the B_i being compositional, plus
the obvious fact that if 2 sets of functions are equal, the 2 sets
have the same properties. You can't tell equal functions apart.

I proved a theorem that this definition is equivalent to
Bill-compositionality, which means that the E_i satisfy the equations

E_i [ Option_ij ] = f_ij (E_ij1 (S_ij1), ..., E_ijk (S_ijk))

That is, by Schmidt's 3.13, my E_i must be equal to your B_i. You've
argued this point, but I think you'll see it after you see why my
ISWIM is Bill-compositional.

Definition. Any old semantics s: L --> D is Bill-compositional if
there exists a Bill-compositional Bill-semantics such that s is one
of the valuation functions E_i defined by the Bill-semantics.

I don't know what the point of this definition would be, and I never
used this definition. I don't know why you defined this, because you
don't use it below either.

Reduction
---------

The one-step reduction relation -> is defined as follows.

You don't say where this relation lives. If you keep the 0's below,
then maybe it's a relation

R subset L(M) x L(M).

(a v1 v2) -> 0 if v1 or v2 is not a numeral

don't you mean bottom instead of 0?

(+ n1 n2) -> Num (E_n[n1] + E_n[n2])
(- n1 n2) -> Num (E_n[n1] - E_n[n2])
(* n1 n2) -> Num (E_n[n1] * E_n[n2])

(ifzero? 0 m1 m2) -> m1
(ifzero? v m1 m2) -> m2 if v is not 0

(v1 v2) -> 0 if v1 is not a lambda term

again, bottom, not 0?

((lambda (x) m) v2) -> m[v2/x] with alpha-conversion as necessary

As I said up top, I'm really nervous here. I'm only willing to
perform your beta_v reduction above if we've already modded out by
alpha-equivalence. For instance, the proof that the Y_v combinator
gives a fixed point uses the fact that we've modded out by
alpha-equivalence, and that means we're using the deep fact that
beta_v reduction makes sense modulo alpha-equivalence.

So maybe what you're doing makes sense, but I certainly wouldn't do
it. You're on your own here.

Operational Semantics
---------------------

Let ->* be the transitive closure of ->.

The operational semantics of a term m is os[[ m ]], where os[[ . ]]
is defined by

os [[ m ]] = v if m ->* v
os [[ m ]] = bottom otherwise

With the 0s above, I don't know why any m goes to bottom. I don't
claim to understand this very well, though.

Note that os[[ . ]] is a total function from M to Z_bottom, but it
is not a computable function.

The target Z_bottom doesn't look right. suppose m = (lambda (x) n).
That's already a value, so os [[ m ]] = m, which is not in Z_bottom.
Same thing for m = x: that's a value, so os [[ x ]] = x.

You could maybe fix this easily by changing the target to Value, as I
do, and saying that os is a total function

os: L(M) ---> L(V)_bottom

BTW every time I said something was a "function", I meant a total
function. I would definitely say "partial function" if it was
partial, but with _bottom, we can always get total functions.

Bill-semantics
--------------

The Bill-semantics uses a new nonterminal P, which stands for a
complete program.

I certainly never mentioned this is my ISWIM posts.

For convenient reference, we repeat the other relevant productions
as well:

P ::= M

M ::= V | (A M M) | (ifzero? M M M) | (M M)

V ::= n | x | (lambda (x) M)

A ::= + | - | *

The valuation functions are

E_P: P --> Z_bottom

E_M: M --> M

E_V: V --> V

Wait, I'm new at this. So you've defined 3 semantic domains D_i, and
the 2nd 2 are the syntactic domains? Can I say
D_1 = Z_bottom
L(B_2) = D_2
L(B_3) = D_3

So I think you should've said (being fully pedantic)

E_P: L(P) --> Z_bottom

E_M: L(M) --> L(M)

E_V: L(V) --> L(V)

defined by structural induction from

And (slow me again) now you need f_ij functions, but you just directly
write down the compositionality equations.

E_P [[ m ]] = os [[ E_M[[ m ]] ]]

So the 1st map you need is f_11: L(M) ---> Z_bottom, and it's the
function

m |--> os [[ E_M[[ m ]] ]].

E_M [[ v ]] = E_V[[ v ]]

Some trouble: This is for the 1st option M ::= V, so you need

f_21: L(V) ---> L(M)

so I guess you forgot to compose with the obvious inclusion

L(V) >---> L(M)

E_M [[ (a m1 m2) ]] = (a E_M [[ m1 ]] E_M [[ m2 ]])

E_M [[ (ifzero? m0 m1 m2) ]]
= (ifzero? E_M [[ m0 ]] E_M [[ m1 ]] E_M [[ m2 ]])

E_M [[ (m1 m2) ]] = (E_M [[ m1 ]] E_M [[ m2 ]])

E_V [[ n ]] = Num(E_n[n])

E_V [[ x ]] = Var(E_x[x])

E_V [[ (lambda (x) m) ]] = (lambda (E_V [[ x ]]) E_M [[ m ]])

Bill-compositionality
---------------------

Theorem. The Bill-semantics shown above is Bill-compositional.

Proof: Immediate by the definition of Bill-compositionality. QED

Yeah, follows immediately from the Lemma & Cor below. That's great!

Lemma. E_M and E_V are the identity functions on M and V,
respectively.

Proof: By simultaneous structural induction on M and V. QED

Good. You made a false claim of that sort about my post, but it's
true for you here.

Corollary. For any term m, E_P [[ m ]] = os [[ m ]].

Sure!

Therefore the original operational semantics is Bill-compositional.

Nice work! With all the reservations above.

Full Abstraction
----------------

For example, it seems like two terms should have the same
denotation if and only if they behave the same in all contexts.
This property is called full abstraction.

Will, isn't this about observational equivalence? And didn't you post
2 yrs ago that this is false for R5RS DS: you found X & Y which were
observational equivalent, but

curly-E[[ X ]] != curly-E[[ Y ]]

I thought you posted that we can just create a new meaningless
environment that changes the location patterns, in a non-essential
way.

In other words, one of the most un-abstract semantics that could be
imagined is fully abstract. Examples like this are part of the
reason full abstraction is no longer regarded as a terribly useful
concept.

That's interesting. Thanks. There's an important DS point here: It
seems like we're abandoning the idea that curly-E maps an expression
to it's "meaning". If we're going to go cultural about the meaning of
meaning, then maybe we'd insist on observational equivalence. I'm
against the cultural meaning of meaning discussion myself. I only
want to insist that curly-E capture the "meaning-meaning" of whole
programs, via

curly-E[[ X ]](r0, s0, k0) in Answers

And that's true.

Ray Dillinger

2004-07-16, 8:59 pm

For the non-mathematicians in the group, this discussion has grown
increasingly mystifying. I have to admit that I no longer think I
know what the discussion is even about.

My formal semantics got as far as domain theory applied to expert
systems. And we worked mostly with operational rather than
denotational forms for that matter. For me the Denotational
semantics section in the scheme standard is uphill work in the
first place. Whatever point you're discussing, as far as I can
tell, lies outside my limited understanding of it.

Bear

William D Clinger

2004-07-17, 3:58 pm

Ray Dillinger <bear@sonic.net> wrote:
> For the non-mathematicians in the group, this discussion has grown
> increasingly mystifying. I have to admit that I no longer think I
> know what the discussion is even about.
>
> ....Whatever point you're discussing, as far as I can
> tell, lies outside my limited understanding of it.

Shriram suggested that (the only way?) some good might come of this
discussion is for someone to write a tutorial that explains why we
don't use the approach that Bill is advocating. I'm trying to write
that tutorial in a form that someone like Shriram could use as the
basis for his own lecture notes in the first or second w

of a
graduate course on semantics of programming languages. There are
perhaps half a dozen readers of this newsgroup who might teach such
a course, and perhaps another 50 or so who have taken such a course,
and I'm writing mainly for them.

My tutorial might make more sense after you see parts 1a, 1b, and 2,
but I'm not going to guarantee that.

Another way of looking at it is that this tutorial provides a way
for me to answer Bill without getting involved in arguments as to
which of his mistakes were mere typos and which were serious. I
will simply prove that it would be a serious mistake to do things
in certain ways, and let Bill argue with himself as to whether he
has done things in those ways.

Will

William D Clinger

2004-07-17, 3:58 pm

Errata for part 1
-----------------

In section "Contexts and Redexes":

I need two different kinds of contexts, and I should have stated
a trivial lemma and defined a notation, as follows.

The following productions define term contexts TC, evaluation
contexts EC, and redexes R. Term contexts are used only in the
section on full abstraction.

TC ::= [] | (lambda (x) TC) | (A TC M) | (A M TC)
| (ifzero? TC M M) | (ifzero? M TC M) | (ifzero? M M TC)
| (TC M) | (M TC)

EC ::= [] | (A EC M) | (A V EC) | (ifzero? EC M M)
| (EC M) | (V EC)

R ::= (A V V) | (ifzero? V M M) | (V V)

Lemma. Every term context and every evaluation context contains
exactly one occurrence of the "hole" [].

Proof: By structural induction. QED

Definition. If c is a term context or evaluation context, and m is
a term, then c[m] is the result of replacing the hole in c by m.

----------------

In section "Reduction":

I should have remarked that any deterministic, state-less algorithm
for performing alpha conversion can be used. In the absence of such,
we would have to work with terms modulo alpha conversion, which would
be a minor complication.

----------------

In section "Operational Semantics":

As Bill Richter pointed out, the range of os[[.]] is not just
Z_bottom. I should have written:

Note that os[[ . ]] is a total function from M to a set that includes
bottom, but it is not a computable function.

----------------

In section "Bill-semantics":

As Bill Richter pointed out, I should have noted the simplifying
abuse of notation that is involved in writing E_M: M -> M instead
of E_M: L(M) -> L(M).

My definition of the Bill-semantics didn't quite fit the definition
of Bill-compositionality because my grammar defined a nonterminal A
for which I did not define a valuation function E_A. That valuation
function should have been used in this equation for E_M:

E_M [[ (a m1 m2) ]] = (E_A [[ a ]] E_M [[ m1 ]] E_M [[ m2 ]])

and E_A should have been defined by

E_A: A --> A

E_A [[ + ]] = +
E_A [[ - ]] = -
E_A [[ * ]] = *

----------------

In section "Full Abstraction":

The contexts of this section are term contexts, not evaluation
contexts.

Definition. The denotational semantics ds[[.]] is fully
abstract if, for every pair of terms m1 and m2,

ds [[ m1 ]] = ds [[ m2 ]

if and only if

for all term contexts tc, os [[ tc[m1] ]] = os [[ tc[m2] ]].

Theorem. The Bill-semantics defined above is fully abstract.

Proof. E_M [[ m1 ]] = m1 and E_M [[ m2 ]] = m2. m1 and m2
are just syntax, so m1 = m2 means m1 and m2 are syntactically
equal. If they are syntactically equal, then

os [[ tc[m1] ]] = os [[ tc[m2] ]]

That takes care of the forward implication. For the reverse,
consider the term context tc = (lambda (x) []). By definition
of os[[.]],

os [[ tc[m1] ]] = (lambda (x) m1)

os [[ tc[m2] ]] = (lambda (x) m2)

If these values are equal, then m1 = m2 as syntax, which implies
E_M [[ m1 ]] = E_M [[ m2 ]].

End of proof.

----------------

William D Clinger

2004-07-17, 3:58 pm

Part 1b of a tutorial on
why Bill-semantics is not DS
by William D Clinger

BR-style Bill-semantics
-----------------------

Bill Richter has argued that a semantics of the following form,
which I will call BR-style, is different in some important way
from the Bill-semantics presented in part 1 of this tutorial.

(Richter's own semantics is incomplete and somewhat confusing,
but appears to differ from the one shown below in at least two
ways: he identifies alpha-convertible terms, and rewrites type
errors as something other than zero. These differences do not
amount to much, but would require several minor changes in our
toy language and its semantics, so we leave the elimination of
these differences as an exercise for the diligent reader.)

The BR-style Bill-semantics of our toy language is identical to
the earlier Bill-semantics except for these two changes:

1. The nonterminal P and its single production P ::= M is
replaced by the nonterminal Q and its four productions
shown below.

2. The semantic function E_P is replaced by E_Q.

The other productions and semantic functions remain as before.

Definition. A value v is proper iff it is not bottom.

Q ::= V | (A M M) | (ifzero? M M M) | (M M)

E_Q: Q --> V_bottom

E_Q [[ v ]] = v

E_Q [[ (a m1 m2) ]]
= f_12 (arith(a), E_Q [[ m1 ]], E_Q [[ m2 ]])

E_Q [[ (ifzero? m0 m1 m2) ]]
= f_13 (E_Q [[ m0 ]], E_Q [[ m1 ]], E_Q [[ m2 ]])

E_Q [[ (m1 m2) ]] = f_14 (E_Q [[ m1 ]], E_Q [[ m2 ]])

where arith, f_12, f_13, and f_14 are defined by

arith (+) = the usual + function
arith (-) = the usual - function
arith (*) = the usual * function

f_12 (g, v1, v2) = bottom if either v1 or v2 is bottom

f_12 (g, v1, v2) = 0
if v1 and v2 are both proper but not both integers

f_12 (g, v1, v2) = g (v1, v2) if both v1 and v2 are integers

f_13 (bottom, v1, v2) = bottom
f_13 (0, v1, v2) = v1
f_13 (v0, v1, v2) = v2 if v0 is proper but not 0

f_14 (v1, v2) = bottom if either v1 or v2 is bottom

f_14 (v1, v2) = 0
if both v1 and v2 are proper, and v1 is not a lambda expression

f_14 (v1, v2) = os [[ m[v2/x] ]]
if v1 = (lambda (x) m) and v2 is proper

(Note: In Bill Richter's original formulation of his own BR-style
Bill-semantics, he attempted to define f_14 in terms of E_Q, which
would prevent the semantics from being Bill-compositional: The
quantifier structure of the definition of Bill-semantics requires
the f_ij to be given before the semantic functions B_i are defined
by structural induction. This is discussed at some length below,
in the section on "BR-style Nonsense".)

Theorem. The BR-style Bill-semantics is Bill-compositional.

Proof: Immediate by the definition of Bill-compositionality. QED

To prove the equivalence of this BR-style Bill-semantics with our
original Bill-semantics, we will need the following interpolation
lemmas.

Lemma. If there exists a proper value v such that (a m1 m2) ->* v,
then there exist proper values v1 and v2 such that m1 ->* v1,
m2 ->* v2, and

(a m1 m2) ->* (a v1 m2) ->* (a v1 v2) ->* v

Proof. By induction on the number of reduction steps. Let c and
r be the unique evaluation context and redex such that (a m1 m2)
= c[r], and let r -> r'. If c is [], then m1 and m2 are the
proper values v1 and v2, and r' is v. If c is (a c1[r] m2),
then (a c1[r] m2) -> (a c1[r'] m2) ->* v so by the induction
hypothesis there exist proper v1 and v2 such that

m1 -> c1[r'] ->* v1
m2 ->* v2
(a m1 m2) -> (a c1[r'] m2) ->* (a v1 m2) ->* (a v1 v2) -> v

If c is (a v1 c2[r]), then v1 is proper and there exists a proper v2
such that

m1 = v1
m2 -> c2[r'] ->* v2
(a m1 m2) -> (a v1 c2[r']) ->* (a v1 v2) -> v

QED

Lemma. If there exists a proper value v such that
(ifzero? m0 m1 m2) ->* v, then there exists a proper value v0 such
that (ifzero? m0 m1 m2) ->* (ifzero? v0 m1 m2) ->* v. Furthermore
either v0 is 0 and m1 ->* v, or v0 is not 0 and m2 ->* v.

Proof: By induction on the number of reduction steps, as above.
QED

Lemma. If there exists a proper value v such that (m1 m2) ->* v,
then there exist proper values v1 and v2 such that
(m1 m2) ->* (v1 m2) ->* (v1 v2) ->* v.

Proof: By induction on the number of reduction steps, as above.
QED

Our main lemma is:

Lemma. If v is a proper value and m ->* v, then E_Q [[ m ]] = v.

Sketch of proof: By induction on the number of reduction steps in
m ->* v. The proof proceeds by exhaustive examination of the syntactic
cases for m, applying the appropriate interpolation lemma for each case.

Leaving most of these cases as exercises for the dedicated reader,
the most difficult case occurs when m is an application (m1 m2).
Let v1 and v2 be proper values such that m1 ->* v1, m2 ->* v2, and

(m1 m2) ->* (v1 m2) ->* (v1 v2) ->* v

By the induction hypothesis, E_Q [[ m1 ]] = v1 and E_Q [[ m2 ]] = v2
so E_Q [[ m ]] = f_14 (v1, v2).

If v1 is not a lambda expression, then

v = 0 = f_14 (v1, v2) = E_Q [[ m ]]

by the definitions of -> and E_Q.

Otherwise m1 is some lambda expression (lambda (x) m3), and

m ->* ((lambda (x) m3) v2) -> m3[v2/x] ->* v

Therefore

E_Q [[ m ]] = f_14 (v1, v2) = os [[ m3[v2/x] ]] = v

End of sketch of proof.

Lemma. If v is proper and E_Q [[ m ]] = v, then m ->* v.

Proof: Left as an exercise for the dutiful reader.

Corollary. For all m in L(P) = L(Q),

E_Q [[ m ]] = E_P [[ m ]] = os [[ m ]]

BR-style Nonsense
-----------------

In this section we consider the consequences of writing E_Q instead
of os in our definition of f_14:

f_14 (v1, v2) = bottom if either v1 or v2 is bottom

f_14 (v1, v2) = 0
if both v1 and v2 are proper, and v1 is not a lambda expression

f_14 (v1, v2) = E_Q [[ m[v2/x] ]]
if v1 = (lambda (x) m) and v2 is proper

The first thing to notice is that this change would prevent our
semantics from being Bill-compositional. The quantifier structure
of the definition of Bill-compositional requires the f_ij to be
given *before* the semantic functions are defined by structural
induction. Since E_Q is one of those semantic functions, f_14
cannot refer to it.

This is why David Schmidt, in his presentation of Theorem 3.13,
says the boldface B_i are fresh (or uninterpreted) function symbols.
That means they cannnot occur free in the definition of the f_ij.
Hence the use of E_Q instead of os in the definition of f_14 would
prevent us from using Schmidt's Theorem 3.13 to establish the
existence or uniqueness of a function that satisfies the equations
for E_Q.

The problem is that the mutual recursion between f_14 and E_Q
makes it impossible for us to use structural induction to prove
the existence of an actual function corresponding to E_Q. For
a concrete example of the problem, let m be the M-term

(lambda (x) (x x))

and consider the Q-term (m m). By the alleged definition of E_Q,

E_Q [[ (m m) ]]
= f_14 (E_Q [[ m ]], E_Q [[ m ]])
= f_14 (m, m)
= E_Q [[ (x x)[m/x] ]]
= E_Q [[ (m m) ]]

Thus we have an infinite regress in our definition of E_Q. This
infinite regress means that our definition of E_Q doesn't define
anything if we try to regard it as a definition by structural
induction.

If we really insist on mutual recursion between f_14 and E_Q, then
we might be able to find some other way of looking at the equations
for E_Q that would allow us to interpret them as the definition of
a genuine function. For example, we might regard the equations for
E_Q as the definition of a partial recursive function. One problem
with this is that partial recursive functions are normally defined
over integers, not syntactic structures, so we might have to figure
out some way to encode terms as integers. We could do that, but it
would be inconvenient.

A more serious problem with regarding the definition of E_Q as the
definition of a partial recursive function is that E_Q would no
longer be total. In particular, E_Q would be undefined on the
Q-term ((lambda (x) (x x)) (lambda (x) (x x))).

Since E_Q would be a computable partial function that is not total,
it would not be equal to the non-computable total function os[[.]],
making it impossible for us to prove our main theorem. We would
probably be able to prove that the non-computable totalization of
E_Q is equal to os[[.]], however, since os[[.]] is itself the
non-computable totalization of a partial function.

Alternatively, we could bring in the machinery of Scott domains
and least fixed points to establish that the equations for E_Q
define a computable partial function. This approach might be more
convenient than using integers to encode terms, but terms would
themselves become points in a Scott domain, and we would no longer
be able to prove theorems by structural induction over terms.

To summarize: If we try to use mutual recursion between one of
the f_ij and one of the semantic functions E_i, then our semantics
will no longer be Bill-compositional, structural induction will
no longer suffice to establish existence of the semantic functions
E_i, we will have to use some fairly sophisticated mathematics to
establish the existence of the semantic functions, and the semantic
functions are unlikely to be total functions. A semantic function
that is not total implies that some well-formed programs will not
have any meaning.

So mutual recursion between the f_ij and semantic functions E_i
is a bad move all around.

Analysis of BR-style
--------------------

When formulated correctly, a BR-style Bill-semantics is Bill-compositional
and is equivalent to a Bill-compositional Bill-semantics in our original
form, with a single nonterminal P whose sole production is of the form
P ::= M.

Hence all of our main results concerning our original Bill-semantics
carry over to the BR-style Bill-semantics.

The BR-style is obviously more complicated. If your goal as a
semanticist is to obscure the meanings of programs and to hide
the mathematical properties of your semantics, then the unnecessary
complexity of BR-style is its primary advantage. For example, the
fact that E_Q is just a disguised form of the operational semantics
os[[.]] required several lemmas to prove. With our original
Bill-semantics E_P, that identity was obvious.

The BR-style nonsense is another example of this. If your goal is to
fool people into thinking that your Bill-semantics is Bill-compositional
when it is not, then you will prefer BR-style because its unnecessary
complexity will make it harder for people to spot mutual recursion
between the f_ij and the semantic functions E_i.

Will

Marcin 'Qrczak' Kowalczyk

2004-07-18, 3:59 pm

On Wed, 14 Jul 2004 15:56:56 -0700, William D Clinger wrote:

> Because small-step operational semantics are not compositional in
> the generally accepted meaning of that term, Bill has adopted the
> following definitions, which are based on Theorem 3.13 in David A.
> Schmidt's textbook on denotational semantics [Schmidt].

What is the correct definition of a compositional semantics?

--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/

William D Clinger

2004-07-18, 8:59 pm

Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> wrote
>
> What is the correct definition of a compositional semantics?

The definition of a semantics is compositional if it proceeds
by structural induction over the syntax of program phrases.

Thus it is really the definition that is compositional, not
the semantic functions that the definition defines. For an
example, see how the B_i functions are defined in my definition
of Bill-compositional, and see how the E_i functions are defined
in the rest of my tutorial on why Bill-semantics is not DS.

A compositional semantics is parametric in the f_ij functions.
This means we can define families of related semantics by
varying the f_ij functions, and we can prove relationships
between those semantics from relationships that hold between
the f_ij functions that were used to define those semantics.
That's how abstract interpretation works. That's also how
we prove the correctness of some program transformations and
compiler optimizations.

A Bill-compositional semantics is a family of semantic functions,
not a definition, so in the strictest sense a Bill-compositional
semantics cannot be compositional. In particular, a semantics
that is merely Bill-compositional does not come with a canonical
definition that we can use to perform abstract interpretation or
to prove the correctness of transformations and optimizations.

I'm not sure why Bill Richter is so concerned to tell us that
our notion of a compositional definition doesn't make any sense.
My guess is that he just doesn't know very much about algebra
and logic and other branches of mathematics, philosophy, and
computer science that concern themselves as much with the forms
of definitions as with the things being defined.

Hope that helps.

Will

Bill Richter

2004-07-19, 3:57 am

cesuraSPAM@verizon.net (William D Clinger) wrote in message news:<fb74251e.0407170705.86b080e@posting.google.com>...

In this section we consider the consequences of writing E_Q instead
of os in our definition of f_14:
[...]
f_14 (v1, v2) = E_Q [[ m[v2/x] ]]
if v1 = (lambda (x) m) and v2 is proper

But that would crazy, wouldn't it Will? Since you're defining E_Q by
structural induction via the f_ij, you can't have E_Q as part of the
definition of f_14!

So if I had written that, it would be nonsense. In the other thread,
you said I did this nonsense in my original 350-line post. I read
your post mostly to see how you misinterpreted my 350-line post.

BUT YOU CITE MY 350-LINE POST AT ALL!!!

I just looked at it myself. I don't use the "structural" at all. I
only use the word "induction" to talk about my inductive construction
of E, and really only in the one sentence

"We define the iterative composites R^n by induction,"

I'm defining my function E, which is something like your os[[.]]
function from your first post.

The problem is that the mutual recursion between f_14 and E_Q
makes it impossible for us to use structural induction to prove
the existence of an actual function corresponding to E_Q.

It sure would!!!! Good thing I didn't do it!

This is why David Schmidt, in his presentation of Theorem 3.13,
says the boldface B_i are fresh (or uninterpreted) function
symbols. That means they cannnot occur free in the definition of
the f_ij.

In one sense, you're correct, Will. If we wish to define the BB_i (BB
for boldface) by structural induction via the f_ij, then the BB_i
cannot occur free in the definition of the f_ij. It doesn't even make
sense. The BB_i aren't defined when the structural induction begins.

But your wrong in another sense. The statement of Schmidt's Theorem
3.13 actually says nothing of the sort. From Joe's quote:

If, for each B_i in L's definition and each Option_ij of B_i's
rule, there exists an equation of the form:

BB_i(Option_ij)
= f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ijk))

where f_ij is a function of functionality
D_ij1 x D_ij2 x ... D_ijk -> D_i,
then the set of equations uniquely defines a family of functions
BB_i: B_i -> D_i for 1<=i<=n.

As I posted earlier (you didn't respond), this means exactly:

Given functions f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i,

for i = 1,..,n, j = 1,...,m, there is a unique family of functions
BB_i: B_i -> D_i for 1<=i<=n satisfying the equations

BB_i(Option_ij)
= f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ijk))

So there's no structural induction in the statement of 3.13, or
insistence that the f_ij not us the BB_i. Possibly you're being

by his strange locution,

If [...] there exists an equation of the form:

BB_i(Option_ij) = f_ij (BB_ij1 (S_ij1), ...)

Of course there exists an equation of the form! He just wrote it
down! And of course at this point, the BB_i are just your fresh (or
uninterpreted) function symbols. But that's not interesting. The
point is that we want to solve these equations, and that's his

then the set of equations uniquely defines a family of functions
BB_i: B_i -> D_i for 1<=i<=n.

So Schmidt is merely being wordier than I was in my restatement.

On to your post. BTW your errata looked good. Thanks for the plugs.

The BR-style Bill-semantics of our toy language is identical to the
earlier Bill-semantics except for these two changes:

1. The nonterminal P and its single production P ::= M is
replaced by the nonterminal Q and its four productions
shown below.

2. The semantic function E_P is replaced by E_Q.

The other productions and semantic functions remain as before.

Definition. A value v is proper iff it is not bottom.

Q ::= V | (A M M) | (ifzero? M M M) | (M M)

E_Q: Q --> V_bottom

E_Q [[ v ]] = v

This looks closer to what I did than before. I'm a little

,
especially since so much is deferred to your previous post, but maybe
you have more "special-forms" than I did. In any case, you proved
below some (without modding out by alpha-equivalence!!) a version of
my only difficult step, my Bill-compositionality equations

E[(op M N)] = op( E[M], E[N] )

E[(M N)] = Phi( E[M], E[N] )

where my Phi is defined in terms of E by: For U, V in Value,

Phi(U, V) = bottom, if U is a number or a variable

E[ R[y <- V] ], if U = (lambda (y) R)

So you've now done as much work as I did anyway. I now declare your
semantics here to not be "meaningless" anymore, since you've re-proved
my result, and quite likely you've cleaned up the proof as well.

(Note: In Bill Richter's original formulation of his own BR-style
Bill-semantics, he attempted to define f_14 in terms of E_Q, which
would prevent the semantics from being Bill-compositional: The
quantifier structure of the definition of Bill-semantics requires
the f_ij to be given before the semantic functions B_i are defined
by structural induction. This is discussed at some length below,
in the section on "BR-style Nonsense".)

This is false. I merely had a typo, corrected in my 2nd ISWIM post,
but at no time did I ever define E, or EE_1 or anything like E_Q by
structural induction.

Anyway, in both of my ISWIM posts, I defined f_13 in terms of E, which
isn't an error, since I'm not using structural induction.

Bill Richter

2004-07-19, 3:57 am

cesuraSPAM@verizon.net (William D Clinger) wrote in message news:<fb74251e.0407170513.441931d@posting.google.com>...

Shriram suggested that (the only way?) some good might come of this
discussion is for someone to write a tutorial that explains why we
don't use the approach that Bill is advocating.

Shriram's advice sounds really good to me, Will, but I don't see that
you're taking it. My guess is that Shriram wants is something I'd
like to see: What are the advantages of the usual Scott model CPO
approach? Not: why does Bill's stuff violate compositionality?

Now I'm glad that you started a new thread, and I'm glad you're
writing articles. I think it's a real good idea for you to be stating
& proving things. But so far, these are articles for me, mostly.

Shriram Krishnamurthi

2004-07-19, 3:57 am

richter@math.northwestern.edu (Bill Richter) writes:

> Shriram's advice sounds really good to me, Will, but I don't see that
> you're taking it. My guess is that Shriram wants is [...]

Given that Will, Joe and I spent a leisurely 2-3 hours together last
w

, I suspect Will understands my intent pretty well. (-:

> What are the advantages of the usual Scott model CPO
> approach? Not: why does Bill's stuff violate compositionality?

It's obvious what the advantages of the usual Scott/Strachey models
are. They let you define a denotational semantics. Any DS textbook
demonstrates that, in gory detail.

What a student *will* wonder is, "Whatever was Scott thinking? Why
not try the following, monstrously simpler thing instead?" Will's
notes show the consequence, a sobering reminder to hunker down and get
back to your domain theory.

Shriram

William D Clinger

2004-07-19, 4:01 pm

Bill Richter is a prolix chomper.

Responding to Bill in the "interpreters & semantics" thread, I have
already refuted most of the nonsense he wrote in the message to
which I am responding now. To make that earlier response easier for
readers of this thread to find, I gave it a new subject line:

Richter's Fallacy 3.13 implies GRH, P=NP

richter@math.northwestern.edu (Bill Richter) wrote:
>
> In this section we consider the consequences of writing E_Q instead
> of os in our definition of f_14:
> [...]
> f_14 (v1, v2) = E_Q [[ m[v2/x] ]]
> if v1 = (lambda (x) m) and v2 is proper
>
> But that would crazy, wouldn't it Will? Since you're defining E_Q by
> structural induction via the f_ij, you can't have E_Q as part of the
> definition of f_14!
>
> So if I had written that, it would be nonsense. In the other thread,
> you said I did this nonsense in my original 350-line post. I read
> your post mostly to see how you misinterpreted my 350-line post.
>
> BUT YOU CITE MY 350-LINE POST AT ALL!!!

I was being kind.

But since you insist, here are the relevant excerpts from your
350-line post:

> Schmidt's 3.13 then demands some f_ij functions....

You then proceeded to define all of the f_ij except for the really
important one, f_14. For that one, you defined only its domain and
range, and gave it the alias "Phi":

> f_14 = Phi: Value x Value ---> Value
>
> is the hard one, coming from (M N), and not defined yet, but I want to
> give it a name.

Then you defined the equations that, according to Schmidt's Theorem
3.13, have a unique solution that's parametric in the f_ij:

> ******* the compositionality equations *******
>
> Apart from the terminals symbols handled above, the compositionality
> equations are only for M in Exp:
>
> E: Expr ---> Value_bottom
>
> E[x] = x
>
> E[n] = n
>
> E[(lambda (x) M)] = (lambda (x) M)
>
> E[(M N)] = Phi( E[M], E[N])
>
> E[ (alpha M M) ] = alpha(m, n), if E[M] = m, E[N] = n
> bottom, otherwise
>
>
> Any solution of these equations in E and Phi will show that E is
> Bill-compositional, which have agreed to assume is equivalent to
> Will-compositionality. I'll first define Phi in terms of E, and then
> define E, and then show these equations are actually satisfied.

In other words, you said yourself that you defined f_14 = Phi in
terms of E, which you are overloading to serve as all the function
symbols BB_i (boldface) B_i in Schmidt's Theorem 3.13.

As I pointed out, defining the f_ij in terms of the function symbols
BB_i (your E) is forbidden by Schmidt's Theorem 3.13 but not by
your misinterpretation of Schmidt's theorem, which I refer to as
Richter's Fallacy 3.13.

Here is your actual "definition" of f_14 = Phi:

> So Phi: Value x Value ---> Value_bottom
>
> will be defined (after defining E) by
>
> Phi(U, V) = E[ P[y <- V] ], if U = (lambda (y) P),
> bottom, otherwise

You then rewrite the relevant semantic equation for E as

> E[(M N)] = E[ P[y <- E[N]] ], if E[M] = (lambda (y) P),
> bottom, otherwise

and applied Richter's Fallacy 3.13 to conclude that your equations
for E have a unique solution.

I addressed the remainder of your message in my proof that
"Richter's Fallacy 3.13 implies GRH, P=NP".

> This is false. I merely had a typo, corrected in my 2nd ISWIM post,
> but at no time did I ever define E, or EE_1 or anything like E_Q by
> structural induction.

It is now clear that your definition of f_14 = Phi in terms of E
was not just a typo. The typo to which you refer was probably
unrelated, but your explanation of it was so unclear that I thought
you had retracted your definition of f_14 = Phi without giving a
correct definition. What really happened is that you never
understood that your definition of f_14 = Phi was incorrect in
the first place.

> Anyway, in both of my ISWIM posts, I defined f_13 in terms of E, which
> isn't an error, since I'm not using structural induction.

I quoted this to underline the fact that you do not recognize the
structural induction in Schmidt's Theorem 3.13, that you are quite
deliberately defining your f_ij in terms of the function symbols
BB_i (your overloaded E), and that both the existence and the
uniqueness of your semantic functions therefore depend upon
Richter's Fallacy 3.13.

Which is one way of saying you have not yet proved your semantic
functions even exist, let alone that they're unique.

Will

Joe Marshall

2004-07-19, 8:58 pm

richter@math.northwestern.edu (Bill Richter) writes:

> If, for each B_i in L's definition and each Option_ij of B_i's
> rule, there exists an equation of the form:
>
> BB_i(Option_ij)
> = f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ijk))
>
> where f_ij is a function of functionality
> D_ij1 x D_ij2 x ... D_ijk -> D_i,
> then the set of equations uniquely defines a family of functions
> BB_i: B_i -> D_i for 1<=i<=n.
>
>
> As I posted earlier (you didn't respond), this means exactly:
>
> Given functions f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i,
>
> for i = 1,..,n, j = 1,...,m, there is a unique family of functions
> BB_i: B_i -> D_i for 1<=i<=n satisfying the equations
>
> BB_i(Option_ij)
> = f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ijk))

Huh?! It means *precisely* what it says: if there exists semantic
functions BB_ij1, BB_ij2, ... that define meaning for the selected
(S_ij1, S_ij2, ...) subelements of Option_ij, and there exists a
well-defined function f_ij that define the meaning of BB_i(Option_ij)
by composing the meanings of the subelements, and all the options are
covered, then the BB_i functions are a well-defined semantic function.

It's a high-falutin' way of saying that a semantics defined by
composition over the syntax is well-defined even if it is recursive.
It most definitely does *not* say that the existence of

f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i

is a sufficient precondition for the existence of the various BB_i and
BB_ijk.

> So there's no structural induction in the statement of 3.13, or
> insistence that the f_ij not use the BB_i.

f_ij surely cannot use the BB_i because f_ij is of the form

f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i

while BB_i is of the form

expression -> denotation

> Possibly you're being

Bill Richter

2004-07-20, 3:57 am

cesuraSPAM@verizon.net (William D Clinger) responded to me:

Will, this is progress. You're explaining how you concluded that I
was using structural induction. I conclude that either you didn't
understand my def of Bill-compositionality, or you concluded it was
nonsense and replaced it with something you thought made more sense.
I implore you: do not make such silent replacements!

richter@math.northwestern.edu (Bill Richter) wrote:
>
> In this section we consider the consequences of writing E_Q
> instead of os in our definition of f_14:
> [...]
> f_14 (v1, v2) = E_Q [[ m[v2/x] ]]
> if v1 = (lambda (x) m) and v2 is proper
>
> But that would crazy, wouldn't it Will? Since you're defining
> E_Q by structural induction via the f_ij, you can't have E_Q as
> part of the definition of f_14!
>
> So if I had written that, it would be nonsense. In the other
> thread, you said I did this nonsense in my original 350-line
> post. I read your post mostly to see how you misinterpreted my
> 350-line post.
>
> BUT YOU CITE MY 350-LINE POST AT ALL!!!

I was being kind.

Please spare me such kindness in the future! It drags the discussion
on endlessly. I stand by what I wrote. If you silently change what I
wrote, and respond to that, I can't refute you!

But since you insist, here are the relevant excerpts from your
350-line post:

Thank you!

> Schmidt's 3.13 then demands some f_ij functions....

That's certainly correct.

You then proceeded to define all of the f_ij except for the really
important one, f_14.

Yes.

For that one, you defined only its domain and range, and gave it
the alias "Phi":

> f_14 = Phi: Value x Value ---> Value
>
> is the hard one, coming from (M N), and not defined yet, but I
> want to give it a name.

Yes.

Then you defined the equations that, according to Schmidt's Theorem
3.13, have a unique solution that's parametric in the f_ij:

> ******* the compositionality equations *******
>
> Apart from the terminals symbols handled above, the compositionality
> equations are only for M in Exp:
>
> E: Expr ---> Value_bottom
>
> E[x] = x
>
> E[n] = n
>
> E[(lambda (x) M)] = (lambda (x) M)
>
> E[(M N)] = Phi( E[M], E[N])
>
> E[ (alpha M M) ] = alpha(m, n), if E[M] = m, E[N] = n
> bottom, otherwise
>
>
> Any solution of these equations in E and Phi will show that E is
> Bill-compositional,

That's the important point, Will. I'm only showing that my EE_i are
Bill-compositional. I.e. that the EE_i and the f_ij satisfy some
equations together. It makes no difference for Bill-compositionality
which order the functions are defined in.

> which have agreed to assume is equivalent to
> Will-compositionality. I'll first define Phi in terms of E, and
> then define E, and then show these equations are actually
> satisfied.

In other words, you said yourself that you defined f_14 = Phi in
terms of E,

Yes.

which you are overloading to serve as all the function symbols BB_i
(boldface) B_i in Schmidt's Theorem 3.13.

No, that's wrong, in 2 different ways.

1) As I've said many times, and it's completely corrected in my 2nd
ISWIM post, I goofed only by confusing E with EE_1. EE_1 is a
composite of E with modding out by alpha-equivalence. In no sense did
E ever stand for all my EE_i functions. Only EE_1

2) I'm not using Schmidt's Theorem 3.13 in your preferred way. I'm
not defining the BB_i by structural induction. If you had thought
that Bill-compositionality required this, then you'd maybe have an
issue here. But that's merely a misinterpretation of of my definition
of Bill-compositionality. Let's talk about that.

As I pointed out, defining the f_ij in terms of the function symbols
BB_i (your E) is forbidden by Schmidt's Theorem 3.13

I didn't do any such thing. It's certainly nonsense.

but not by your misinterpretation of Schmidt's theorem, which I
refer to as Richter's Fallacy 3.13.

It's no fallacy, but that's what we must discuss. I'll respond to
that post eagerly.

Here is your actual [definition] of f_14 = Phi:

> So Phi: Value x Value ---> Value_bottom
>
> will be defined (after defining E) by
>
> Phi(U, V) = E[ P[y <- V] ], if U = (lambda (y) P),
> bottom, otherwise

yes.

You then rewrite the relevant semantic equation for E as

> E[(M N)] = E[ P[y <- E[N]] ], if E[M] = (lambda (y) P),
> bottom, otherwise

yes.

and applied Richter's Fallacy 3.13 to conclude that your equations
for E have a unique solution.

I did not. Schmidt proves these equations have a unique solution.

> This is false. I merely had a typo, corrected in my 2nd ISWIM
> post, but at no time did I ever define E, or EE_1 or anything
> like E_Q by structural induction.

It is now clear that your definition of f_14 = Phi in terms of E
was not just a typo.

Correct.

The typo to which you refer was probably unrelated, but your
explanation of it was so unclear that I thought you had retracted
your definition of f_14 = Phi without giving a correct definition.

OK, fine.

What really happened is that you never understood that your
definition of f_14 = Phi was incorrect in the first place.

No, it was correct, for Bill-compositionality. It would be nonsense
for Will-compositionality.

> Anyway, in both of my ISWIM posts, I defined f_13 in terms of E,
> which isn't an error, since I'm not using structural induction.

I quoted this to underline the fact that you do not recognize the
structural induction in Schmidt's Theorem 3.13,

You're just mistaken, but we'll do this on the other thread. I'll
only repeat here: there's no mention of structural induction in the
*statement* of Schmidt's Theorem 3.13.

Bill Richter

2004-07-20, 3:57 am

cesuraSPAM@verizon.net (William D Clinger) wrote in message news:<fb74251e.0407181628.14a80640@posting.google.com>...

Thus it is really the definition that is compositional, not the
semantic functions that the definition defines.

Will, as I've several times posted, this contradicts what you wrote:

> And it's not what Cartwright and Felleisen say in their
> "Extensible Denotational" paper. They say:
>
> [The map from syntactic domains to semantic domains]
> satisfies the law of compositionality: the interpretation of
> a phrase is a function of the interpretation of the
> sub-phrases.

That's almost the same as Schmidt's definition, and the difference
is a very minor mistake by Cartwright and Felleisen: They should
have said the interpretation of a phrase is defined by a function
of the interpretation of the sub-phrases.

Even sticking in these 2 words DEFINED BY, it's still the *maps* which
satisfy the `law of compositionality'. This is something you have to
clarify. You must either reject what you wrote back then, or accept
it, and reject what you wrote up top.

A Bill-compositional semantics is a family of semantic functions,
not a definition, so in the strictest sense a Bill-compositional
semantics cannot be compositional.

If you insist on saying that it's the function-definitions that
satisfy compositionality, in contradiction to your earlier post, then
it imposes only an inconvenience on me. I must tell you that it's my
2nd definition that's the compositional definition.

Bill Richter

2004-07-20, 3:57 am

Shriram Krishnamurthi <sk@cs.brown.edu> wrote in message news:<w7du0w466ap.fsf@cs.brown.edu>...
richter@math.northwestern.edu (Bill Richter) writes:

> Shriram's advice sounds really good to me, Will, but I don't see that
> you're taking it. My guess is that Shriram wants is [...]

Given that Will, Joe and I spent a leisurely 2-3 hours together
last w

, I suspect Will understands my intent pretty well. (-:

I stand corrected, Shriram. And I'm really glad to hear that you want
this compositionality issue settled. Did I get that right? And I'm
glad to hear you guys are meeting in person. I really really wish I
could talk to you guys with chalk + blackboard (and beer maybe).

> What are the advantages of the usual Scott model CPO approach?
> Not: why does Bill's stuff violate compositionality?

It's obvious what the advantages of the usual Scott/Strachey models
are. They let you define a denotational semantics. Any DS
textbook demonstrates that, in gory detail.

To me that's not a meaningful answer. I think there actually is a
meaningful answer. But Stoy's book actually defines, I believe, in
his introduction, DS to mean exactly the Scott/Strachey method. I
recall something like, "The Scott/Strachey method described here is
called "denotational semantics", or "mathematical semantics". That
was a fair definition at the time, because (I think) Stoy's and
Milne's books were the 1st 2 books on mathematical semantics.

What a student *will* wonder is, "Whatever was Scott thinking?

I wouldn't say that! I've always said that Scott was a genius for
coming up with his amazing model of LC P, where continuous maps of P
to itself are all lambda definable. Isn't that amazing:

continuous = computable!

And it seems to have 2 advantages: the obvious one that Procedure can
be a subset of Values and defined as a domain of functions on Values.
There's also the computability advantage, which Will stresses, and I
want to put off until we understand Schmidt's Thm 3.13, at least.

Why not try the following, monstrously simpler thing instead?"

One reason is that Plotkin's LC_v wasn't developed yet. Hope I'm not
blowing the dates. But simpler isn't always better, and that ought to
be the real reason for us.

Will's notes show the consequence, a sobering reminder to hunker
down and get back to your domain theory.

I say that's false, and you shouldn't say it if you're not following
the discussion. Go read Schmidt's Thm 3.13, and figure out what you
think it means. Don't just trust Will to be getting it right.

William D Clinger

2004-07-20, 4:00 pm

richter@math.northwestern.edu (Bill Richter) wrote:
>
> Thus it is really the definition that is compositional, not the
> semantic functions that the definition defines.
>
> Will, as I've several times posted, this contradicts what you wrote:
>
>
> That's almost the same as Schmidt's definition, and the difference
> is a very minor mistake by Cartwright and Felleisen: They should
> have said the interpretation of a phrase is defined by a function
> of the interpretation of the sub-phrases.
>
> Even sticking in these 2 words DEFINED BY, it's still the *maps* which
> satisfy the `law of compositionality'. This is something you have to
> clarify. You must either reject what you wrote back then, or accept
> it, and reject what you wrote up top.

No, Bill. To say "the interpretation of a phrase is defined by a
function of the interpretation of the sub-phrases" is exactly the
same as saying "the interpretation of a phrase is defined by structural
induction on its syntax", which is exactly the same as saying "the
definition of the semantic function that assigns meaning to phrases
is by structural induction".

Your problem, Bill, is that you do not understand the concept of
structural induction. In particular, you do not understand that
Schmidt's Theorem 3.13 asserts that definitions of semantic
functions by structural induction define those functions uniquely.

Hence your fallacious misinterpretation of that theorem. There
is absolutely no doubt whatsoever that your misinterpretation of
that theorem is fallacious. Please see my second post in the
"Richter's Fallacy 3.13 implies GRH, P=NP" thread.

BTW, when a mathematician says you are making a mistake in some
area of mathematics that lies well outside your own competence
but well inside his own, then you ought to pay attention.

Will

William D Clinger

2004-07-20, 4:00 pm

richter@math.northwestern.edu (Bill Richter) wrote:
>
> Will's notes show the consequence, a sobering reminder to hunker
> down and get back to your domain theory.
>
> I say that's false, and you shouldn't say it if you're not following
> the discussion. Go read Schmidt's Thm 3.13, and figure out what you
> think it means. Don't just trust Will to be getting it right.

Chomp Chomp.

The real story here is that, when it comes to mathematics, Dr Bill
Richter can't be trusted to get it right. See the "Richter's Fallacy
3.13 implies GRH, P=NP" thread.

Will

William D Clinger

2004-07-20, 4:00 pm

Chomp Chomp.

richter@math.northwestern.edu (Bill Richter) wrote:
> That's the important point, Will. I'm only showing that my EE_i are
> Bill-compositional. I.e. that the EE_i and the f_ij satisfy some
> equations together. It makes no difference for Bill-compositionality
> which order the functions are defined in.

So it was okay for me to define BB_1 = g6 in my second post of the
"Richter's Fallacy 3.13 implies GRH, P=NP" thread. It's good to
have that on the record.

> which you are overloading to serve as all the function symbols BB_i
> (boldface) B_i in Schmidt's Theorem 3.13.
>
> No, that's wrong, in 2 different ways.
>
> 1) As I've said many times, and it's completely corrected in my 2nd
> ISWIM post, I goofed only by confusing E with EE_1. EE_1 is a
> composite of E with modding out by alpha-equivalence. In no sense did
> E ever stand for all my EE_i functions. Only EE_1

I agree. I should have said you overloaded E to serve as the function
symbol BB_1. I may have made that mistake twice. It is inconsequential.

> 2) I'm not using Schmidt's Theorem 3.13 in your preferred way.

You're not using that theorem in any correct way. Please see my
alternative proof of GRH and P=NP, the one that starts from your
own definitions and uses of Richter's Fallacy 3.13.

>
> I quoted this to underline the fact that you do not recognize the
> structural induction in Schmidt's Theorem 3.13,
>
> You're just mistaken, but we'll do this on the other thread. I'll
> only repeat here: there's no mention of structural induction in the
> *statement* of Schmidt's Theorem 3.13.

I quoted this to underline the fact that you do not recognize the
structural induction in Schmidt's Theorem 3.13.

Yes, this discussion belongs in the "Richter's Fallacy 3.13 implies
GRH, P=NP" thread.

Will

Shriram Krishnamurthi

2004-07-20, 4:00 pm

NNTP-Posting-Host: pontneuf.cs.brown.edu
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: saturn.services.brown.edu 1090337757 13129 128.148.31.5 (20 Jul 2004 15:35:57 GMT)
X-Complaints-To: news@nntp.brown.edu
NNTP-Posting-Date: Tue, 20 Jul 2004 15:35:57 +0000 (UTC)
User-Agent: Gnus/5.0808 (Gnus v5.8.8) XEmacs/21.4 (Common Lisp)
Xref: number1.nntp.dca.giganews.com comp.lang.scheme:52677

cesuraSPAM@verizon.net (William D Clinger) writes:

> BTW, when a mathematician says you are making a mistake in some
> area of mathematics that lies well outside your own competence
> but well inside his own, then you ought to pay attention.

Are areas of competence paracompact?

Shriram

Joe Marshall

2004-07-20, 4:00 pm

Shriram Krishnamurthi <sk@cs.brown.edu> writes:

> cesuraSPAM@verizon.net (William D Clinger) writes:
>
>
> Are areas of competence paracompact?

Can you use Stoke's theorem to convert an area of competence into a
volume of knowledge?

William D Clinger

2004-07-20, 8:58 pm

I agree with most of what Joe Marshall said about Schmidt's
Theorem 3.13 in the post to which I am responding, except
for this curious remark:

> It most definitely does *not* say that the existence of
>
> f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i
>
> is a sufficient precondition for the existence of the various BB_i and
> BB_ijk.

When the existence of the given f_ij functions is combined
with the other assumptions of the theorem (context-free grammar,
fresh BB_i function symbols of appropriate type indexed by
nonterminals, BB_ijk = BB_a where a is the k-th nonterminal
occurring on the right hand side of production ij), then the
theorem most certainly does assert the existence and uniqueness
of the BB_i functions.

Had Schmidt anticipated Richter's fallacious interpretation
of his theorem, I'm sure he would have phrased it more clearly,
along the lines of

If functions f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i
are given, then the following set of equations in the
unknown function symbols BB_i: B_i --> D_i has a unique
solution.

But it's an upper division undergraduate text, for crying out
loud. Schmidt's formulation of the theorem isn't technically
perfect, but anyone who has enough mathematical sophistication
to be in the course or to read the book on her own ought to
have enough mathematical sophistication to realize that, when

(1) there are two different ways to interpret a slightly
ambiguous statement of a theorem, and
(2) one of those interpretations matches the proof and
makes the theorem true, while
(3) the other interpretation does not match the proof
and leads to a contradiction,

the reader should assume the author's intended interpretation
is the one that makes the theorem true.

Will

Bill Richter

2004-07-21, 3:57 am

Shriram Krishnamurthi <sk@cs.brown.edu> responds to me:

> BTW, when a mathematician says you are making a mistake in some
> area of mathematics that lies well outside your own competence
> but well inside his own, then you ought to pay attention.

Are areas of competence paracompact?

:D Shriram, compositionality is definitely in my area of competence.
Like all the pure mathematicians I know, I'm an expert on mathematical
induction, and defining functions by induction. When I tell you what
Schmidt's Theorem 3.13 says, you can rely on me. I've been an
algebraic topologist for 25 years, and I've published in some pretty
good journals, and I've had some pretty good jobs. I have no idea how
Will's competence compares with mine. We believe that Will is really
good at constructing compositional DS functions. But it doesn't
follow that he knows what the definition of compositionality is! He's
a DS expert, not a full-time pure mathematician.

And Shriram, please get involved in this thread mathematically. Your
participation may be need in order to save the incredible investment
in time that Will has made so far. I claim there are only 3 possible
ways for this thread to not be a huge waste of Will's time:

1) Will understands my proof that I've constructed compositional sem
functions, in a reasonably Scheme-like way (e.g. not introducing
too many new special forms).

2) I agree that Will proved that my sem functions do not satisfy
compositionality.

But let's say I'm the idiot/phony Will's making me out to be, and I
either can't or won't understand Will's proof. All is not lost:

3) The rest of you (Joe, MB, Lauri, you) understand Will's proof.

The 1st is looking remote, and I'm sorry, because I've learned a lot
from Will this time around. Will looks like he's maybe emotionally
incapable of understanding my proof. I hope I'm wrong.

The 2nd can't happen, unless Will comes to grips with my arguments.
It's possible I've made some crazy mistake that I've missed all along,
but I'm not making the mistakes Will's accusing me of. He hasn't
understood what I'm saying. He hasn't understood Schmidt's Thm 3.13.

The 3rd possibility might be where you come in. If you guys
understand Will's proof of how I'm flubbing it, Will will be happy.
His time will be well spent. But I don't think you guys have looked
at his proofs, or checked that the assertions he's rebutting were
actually made by me. Lauri & MB have exhibited signs of dissent even.

BTW it makes no difference if I figure out what a start symbol is.
The question is whether MB will move from his compositional example to
seeing that Will's 2 ISWIM posts were also compositional. If he does,
he'll be agreeing with me. If he doesn't, I won't claim MB's support.

Joe Marshall

2004-07-21, 3:57 am

cesuraSPAM@verizon.net (William D Clinger) writes:

> I agree with most of what Joe Marshall said about Schmidt's
> Theorem 3.13 in the post to which I am responding, except
> for this curious remark:
>
>
> When the existence of the given f_ij functions is combined
> with the other assumptions of the theorem (context-free grammar,
> fresh BB_i function symbols of appropriate type indexed by
> nonterminals, BB_ijk = BB_a where a is the k-th nonterminal
> occurring on the right hand side of production ij), then the
> theorem most certainly does assert the existence and uniqueness
> of the BB_i functions.

Perhaps I should have said that the existence of f_ij *alone* is not
sufficient (ab initio) for the existence of the various BB_i and
BB_ijk. The other assumptions (context-free grammar, etc. etc. and
don't forget that f_ij ought to be well-defined!) are *necessary*.

And it is vitally important that the domain of the semantic functions
is well-founded! This is guaranteed if the input is a context-free
grammar, but not if adjoin other potentially circular elements into
the domain.

> Had Schmidt anticipated Richter's fallacious interpretation
> of his theorem, I'm sure he would have phrased it more clearly,
> along the lines of
>
> If functions f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i
> are given, then the following set of equations in the
> unknown function symbols BB_i: B_i --> D_i has a unique
> solution.
>
> But it's an upper division undergraduate text, for crying out
> loud. Schmidt's formulation of the theorem isn't technically
> perfect, but anyone who has enough mathematical sophistication
> to be in the course or to read the book on her own ought to
> have enough mathematical sophistication to realize that, when
>
> (1) there are two different ways to interpret a slightly
> ambiguous statement of a theorem, and
> (2) one of those interpretations matches the proof and
> makes the theorem true, while
> (3) the other interpretation does not match the proof
> and leads to a contradiction,
>
> the reader should assume the author's intended interpretation
> is the one that makes the theorem true.

Not to mention
(4) one of those interpretations is fairly straightforward
(5) one of those interpretations reinforces the expository text

--
~jrm

Bill Richter

2004-07-21, 3:57 am

Joe Marshall <prunesquallor@comcast.net> responds to me:

> If, for each B_i in L's definition and each Option_ij of
> B_i's rule, there exists an equation of the form:
>
> BB_i(Option_ij)
> = f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ijk))
>
> where f_ij is a function of functionality
> D_ij1 x D_ij2 x ... D_ijk -> D_i,
> then the set of equations uniquely defines a family of
> functions
> BB_i: B_i -> D_i for 1<=i<=n.
>
>
> As I posted earlier (you didn't respond), this means exactly:
>
> Given functions f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i,
>
> for i = 1,..,n, j = 1,...,m, there is a unique family of
> functions BB_i: B_i -> D_i for 1<=i<=n satisfying the
> equations
>
> BB_i(Option_ij)
> = f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ijk))

Huh?! It means *precisely* what it says: if there exists semantic
functions BB_ij1, BB_ij2, ... that define meaning for the selected
(S_ij1, S_ij2, ...) subelements of Option_ij, and there exists a
well-defined function f_ij that define the meaning of
BB_i(Option_ij) by composing the meanings of the subelements, and
all the options are covered, then the BB_i functions are a
well-defined semantic function.

Joe, I don't quite follow, but you're using a lot of words that aren't
in the statement of Schmidt's Thm 3.13. So please address the point
that I raised: I restated 3.13. Tell me if you agree with my
restatement, or not, and if you disagree, tell me what I'm getting
wrong. Don't just make a restatement of your own!

It's a high-falutin' way of saying that a semantics defined by
composition over the syntax is well-defined even if it is
recursive.

That's not in the statement of 3.13.

It most definitely does *not* say that the existence of

f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i

is a sufficient precondition for the existence of the various BB_i
and BB_ijk.

It certainly implies that! And you believe it! Given f_ij, you know
we can construct the various BB_i by structural induction to satisfy
the big equation. Will understands this quite well.

BTW BB_ijk is just some B_p. If S_ijk = B_p, then Schmidt defines
BB_ijk = B_p.

> So there's no structural induction in the statement of 3.13, or
> insistence that the f_ij not use the BB_i.

f_ij surely cannot use the BB_i because f_ij is of the form

f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i

while BB_i is of the form

expression -> denotation

You didn't respond to what I wrote, and I have no idea what you mean.
Why don't you just respond to what I wrote!

> Possibly you're being

by his strange locution,
>
> If [...] there exists an equation of the form:
>
> BB_i(Option_ij) = f_ij (BB_ij1 (S_ij1), ...)
>
> Of course there exists an equation of the form!

Oh? It is easy enough to define a (useless) language with no
BB_ijk or ill-defined f_ij.

What does that mean?

> He just wrote it down!

I think he intended for this to be a *true* equation.

That's his intention, of course,.

I can write down any old thing, but if I qualify with `there
exists' I'm implying more than `there is a piece of paper with this
text on it'.

He implies nothing at that point. He's writing something like this:

Given an element A in LC, suppose there exists an equation in LC

A X = X

Then there is a solution of this equation, and in fact X = Y A is a
solution.

But that's just a clunky way to write. He should say:

The equation A X = X has a solution in LC: X = Y A.

Schmidt says that the functions f_ij and BB_ijk have to exist such
that you can define BB_i by composition of BB_ijk via f_ij. If
these functions exist, then BB_i is well-defined.

> And of course at this point, the BB_i are just your fresh (or
> uninterpreted) function symbols. But that's not interesting.

It isn't a very deep theorem.

I agree with you there!

> The point is that we want to solve these equations, and that's his
>
> then the set of equations uniquely defines a family of functions
> BB_i: B_i -> D_i for 1<=i<=n.

They are `solved' by inspection.

That makes no sense to me, Joe! You, Will & the others will say that
we use structural induction to solve these equations. That is, solve
for the family of functions BB_i. How do you know any such BB_i
exist? By structural induction!

Each BB_i is the result of the appropriate f_ij applied to the
meanings of the subcomponents.

That's sounds really wrong. The BB_i are constructed by structural
induction, starting with the terminal case, which he doesn't mention,
but it's the case for Option_ij when there are no terminal symbols, so
the equation

BB_i(Option_ij)
= f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ijk))

amounts to

BB_i(Option_ij) = f_ij ( * )

Schmidt doesn't explain this, and it's a real weakness of his typo of
having the same k for all ij. He should really say

S_ij1 .... S_ij{k_ij}

where k_ij can be zero, for the terminal symbol case.

Bill Richter

2004-07-21, 3:57 am

NNTP-Posting-Host: 129.105.81.5
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1090374286 2865 127.0.0.1 (21 Jul 2004 01:44:46 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 21 Jul 2004 01:44:46 +0000 (UTC)
Xref: number1.nntp.dca.giganews.com comp.lang.scheme:52690

cesuraSPAM@verizon.net (William D Clinger) responds to me:

Will, the important point is that my interpretation of Thm 3.13 is
true, and the proof is Schmidt's short proof, and my result implies
that Bill-compositionality is the same as c.l.s.-compositionality:

Theorem Bill-3.13:

Given functions f_ij: D_ij1 x D_ij2 x ... D_ijk -> D_i,

for i = 1,..,n, j = 1,...,m, there is a unique family of
functions BB_i: B_i -> D_i for 1<=i<=n satisfying the
equations

BB_i(Option_ij)
=
f_ij (BB_ij1 (S_ij1), BB_ij2 (S_ij2), ... BB_ijk(S_ij{k_ij}))

> Thus it is really the definition that is compositional, not
> the semantic functions that the definition defines.
>
> Will, as I've several times posted, this contradicts what you
> wrote:
>
>
> That's almost the same as Schmidt's definition, and the
> difference is a very minor mistake by Cartwright and
> Felleisen: They should have said the interpretation of a
> phrase is defined by a function of the interpretation of the
> sub-phrases.
>
> Even sticking in these 2 words DEFINED BY, it's still the *maps*
> which satisfy the `law of compositionality'. This is something
> you have to clarify. You must either reject what you wrote back
> then, or accept it, and reject what you wrote up top.

No, Bill. To say "the interpretation of a phrase is defined by a
function of the interpretation of the sub-phrases" is exactly the
same as saying "the interpretation of a phrase is defined by
structural induction on its syntax",

No, Will, as I explained to Shriram, it needn't mean that. But I've
let you get away with sticking these 2 extra words in. That's what we
call Will-compositionality, or c.l.s-compositionality, or just
compositionality. A lot of the trouble in this discussion is that
I've never gotten you to understand that C-F's text makes sense
without the 2 words DEFINED BY, without any consideration of
structural induction, and that's my Bill-compositionality.

which is exactly the same as saying "the definition of the semantic
function that assigns meaning to phrases is by structural
induction".

No, because that's meaningless. As I've said often, It makes no sense
to ask: "What's *the* definition of this function?". You can only
ask, "What's *a* definition of this function?" One Function may have a
variety of definitions.

Your problem, Bill, is that you do not understand the concept of
structural induction.

That's false.

In particular, you do not understand that Schmidt's Theorem 3.13
asserts that definitions of semantic functions by structural
induction define those functions uniquely.

I understand quite well that Thm 3.13 implies just this. But that's
not the *statement* of Thm 3.13. You didn't respond to my post
explaining what Thm 3.13 actually say.

BTW, when a mathematician says you are making a mistake in some
area of mathematics that lies well outside your own competence but
well inside his own, then you ought to pay attention.

As I explained to Shriram, induction & functions defined by induction
is well within my pure Math expertise. But you're making what I'd
call dumb beginner mistakes here. You're much better than I am in DS,
and I'm quite grateful for all that you've taught me, but that's not
the area we're in right now. We're in my turf right now, pure Math.

David Feuer

2004-07-21, 9:00 am

Bill Richter wrote:

> :D Shriram, compositionality is definitely in my area of competence.
> Like all the pure mathematicians I know, I'm an expert on mathematical
> induction, and defining functions by induction. When I tell you what
> Schmidt's Theorem 3.13 says, you can rely on me. I've been an
> algebraic topologist for 25 years, and I've published in some pretty
> good journals, and I've had some pretty good jobs. I have no idea how
> Will's competence compares with mine. We believe that Will is really
> good at constructing compositional DS functions. But it doesn't
> follow that he knows what the definition of compositionality is! He's
> a DS expert, not a full-time pure mathematician.

Wow. What a thing to say. A topologist may know something about
induction, formal logics, and formal languages, but a computer scientist
is truly an expert in these.

> And Shriram, please get involved in this thread mathematically. Your
> participation may be need in order to save the incredible investment
> in time that Will has made so far. I claim there are only 3 possible
> ways for this thread to not be a huge waste of Will's time:
>
> 1) Will understands my proof that I've constructed compositional sem
> functions, in a reasonably Scheme-like way (e.g. not introducing
> too many new special forms).
>
> 2) I agree that Will proved that my sem functions do not satisfy
> compositionality.

3) Will and Shriram have learned enough from your mistakes to improve
the way they teach semantics to their grad students.

> Will looks like he's maybe emotionally
> incapable of understanding my proof. I hope I'm wrong.

You are wrong. Very wrong.

> BTW it makes no difference if I figure out what a start symbol is.

>sigh<. The point is that if you don't know what a start symbol is
then you can't possibly know enough about formal languages to
understand what structural induction means.

--
David,
a math student currently studying topology, who would currently trust
Will Clinger's opinion on anything mathematical, including algebraic
topology, far more than Bill Richter's.

David Feuer

2004-07-21, 9:00 am

Bill Richter wrote:

> I say that's false, and you shouldn't say it if you're not following
> the discussion. Go read Schmidt's Thm 3.13, and figure out what you
> think it means. Don't just trust Will to be getting it right.

One thing that is clear to me in this conversation is that Schmidt
writes his theorem in the language used by computer scientists, which is
not quite the same as the language used by algebraic topologists.
Imagine, Bill, if I read an early paper on topology and didn't realize
that when the paper was written, a "topology" was what is now called a
"Hausdorff topology". I'd surely get mixed up, wouldn't I?

David

William D Clinger

2004-07-21, 9:00 am

Chomp Chomp.

It is not my responsibility to educate Bill Richter. I'm not
even sure it is possible. I therefore have no obligation to
correct his mistakes. Henceforth, to save time, I will ignore
his mistakes and trivialities, and respond only to acknowledge
his correct, non-trivial remarks.

In the message to which I am responding, there were none.

But he did tell a good joke:

> As I explained to Shriram, induction & functions defined by induction
> is well within my pure Math expertise. But you're making what I'd
> call dumb beginner mistakes here. You're much better than I am in DS,
> and I'm quite grateful for all that you've taught me, but that's not
> the area we're in right now. We're in my turf right now, pure Math.

Will

Shriram Krishnamurthi

2004-07-21, 9:00 am

richter@math.northwestern.edu (Bill Richter) writes:

> No, Will, as I explained to Shriram, it needn't mean that. But I've
> let you get away with sticking these 2 extra words in. That's what we
> call Will-compositionality, or c.l.s-compositionality, or just
> compositionality. A lot of the trouble in this discussion is that
> I've never gotten you to understand that C-F's text makes sense
> without the 2 words DEFINED BY, without any consideration of
> structural induction, and that's my Bill-compositionality.

I'm willing to bet their def will make sense if you delete a bunch of
other words also. The point several people have been trying to make
is that that is irrelevant.

C-F (I conjecture) were tossing out a definition that they assumed
their readers all knew, so they didn't pay as much attention to that
as they did to the rest of their paper (eg, their compositional
interpreter fragments, whose details they really drilled).

For you to keep quoting them like this verges on the irresponsible.
If you think their "definition" is that standard, why not find three
other unimpeachable sources that offer the same one?

> No, because that's meaningless. As I've said often, It makes no sense
> to ask: "What's *the* definition of this function?". You can only
> ask, "What's *a* definition of this function?" One Function may have a
> variety of definitions.

Welcome to computer science. You keep insisting that functions are
maps. That's what a function is in math. That's not what it is in
computer science. If you prefer, we can use the term "procedure"
instead for the CS version, to keep this distinction straight.

In math, it's meaningless to ask whether a function "halts". We can't
ask for its time or space complexity. When a function is defined as a
map, it has no spatial or temporal properties. In contrast,
procedures may or may not halt; they can have different time and space
complexities. In computer science, the form of a procedure is
therefore crucial. The quicksort and bubblesort procedural
formulations of the sorting function have differences sufficiently
profound that they are regarded as entirely different "functions".

Shriram

Kevin Millikin

2004-07-22, 3:57 am

richter@math.northwestern.edu (Bill Richter) wrote in message news:<57189ce0.0407201744.40b10ae8@posting.google.com>...
> No, because that's meaningless. As I've said often, It makes no sense
> to ask: "What's *the* definition of this function?". You can only
> ask, "What's *a* definition of this function?" One Function may have a
> variety of definitions.

So do (lambda (x) 42) and (lambda (x) (* 14 3)) define the same
function? How would you go about designing a semantics that could
prove it?

Bill Richter

2004-07-22, 3:57 am

Shriram Krishnamurthi <sk@cs.brown.edu> responded to me:

For you to keep quoting [C-F] like this verges on the
irresponsible. If you think their "definition" is that standard,
why not find three other unimpeachable sources that offer the same
one?

Shriram, that's the only def of compositionality I know, and I've
allowed Will to insert the extra 2 words. I only insist that C-F's
definition makes perfect sense without the extra 2 words, i.e. without
any structural induction. But I don't call it C-F-compositionality, I
call it Bill-compositionality. That's not irresponsible of me.

> No, because that's meaningless. As I've said often, It makes no
> sense to ask: "What's *the* definition of this function?". You
> can only ask, "What's *a* definition of this function?" One
> Function may have a variety of definitions.

Welcome to computer science. You keep insisting that functions are
maps. That's what a function is in math. That's not what it is in
computer science. If you prefer, we can use the term "procedure"
instead for the CS version, to keep this distinction straight.

OK, Shriram, but it doesn't matter here, does it? Will didn't mean
procedures, did he? It wouldn't make any sense. C-F wrote:

> [The map from syntactic domains to semantic domains] satisfies the
> law of compositionality: the interpretation of a phrase is a
> function of the interpretation of the sub-phrases.

So it's only the maps which satisfy `the law of compositionality',
right? And map = math-function, right? That's gotta be true. DS is
about math-functions from syntactic to semantic domains So even if the
maps are defined by procedures = CS-functions, it's irrelevant. C-F
are clearly not saying that the procedures satisfy the `the law of
compositionality'.

Now if you or Will want to change the definition of compositionality
so that it's the procedures th