headers
Mitchell Wand | 1 Jun 1988 03:59

Natural Deduction vs. Sequenzen systems

Thank you for the elucidation of this difference.  On the other hand, the
"typical" usage I have seen is

Gamma |- M:t

where Gamma ranges over "sets of type hypotheses" or sometimes "maps from
variable symbols to types" (or typeschemes), the language about Gamma being a
set or (finite) map is intended to embrace the missing structural rules.

Keeping track of the sets of assumptions in such an explicit way seems
important if the system is to be easily mechanizable.

What would you call this kind of formulation?

Mitchell Wand
College of Computer Science
Northeastern University
360 Huntington Avenue #161CN
Boston, MA 02115

CSNet:  wand@...
Permalink | Reply | 0 comments |
headers
rdt%QUCIS.BITNET | 1 Jun 1988 19:32
Picon

specification logic and call by name

Kurt:  A few comments on your note.

1.  The use of deferred evaluation of parameters ("call by name")
    does not require that "only thunks" (state-dependent expression
    meanings) be used.  I agree with Reynolds on the former, but agree
    with you that it can be convenient to have "pure" value-denoting
    identifiers.  This can be done by introducing a new class of
    phrase types, say val[t], for each data type t, with
    [[val[t]]] = [[t]] lifted, and then [[exp[t]]] = S -> [[val[t]]],
    where S is the set of states (or, more generally, the states
    functor).  Then value phrases are state-independent, and so
    are not "expression-like".  For example, a swapping procedure
    could be specified in specification logic as follows:

    all x,y:var[t]. all x0,y0:val[t]. gv(x) & gv(y) & y#x =>
             {x=x0 and y=y0} swap(x,y) {x=y0 and y=x0}

    which avoids a lot of distracting non-interference assumptions
    about x0 and y0 (compare with the Craft of Programming, page 240).
    But such value phrases would still be called-by-name in the sense
    of deferred evaluation.  Conceivably, location-denoting phrase
    types could be added in the same fashion, with a coercion from
    locations to variables, but I'm not convinced that the low-level
    concept of location has any advantages.

2.  You suggest that call by name is easy to reason about yet has
    "unexpected behaviour".  Depends on what kind of behaviour one
    expects!  I think the behaviour seems unexpected primarily to
    programmers who are more familiar with FORTRAN and PASCAL
    than with ALGOL 60.  With the well-known example swap(i, a[i]),
(Continue reading)

Permalink | Reply | 0 comments |
headers
Uday S. Reddy | 3 Jun 1988 01:40
Picon

denotational versus operational semantics

/* Written  8:04 pm  May 30, 1988 by sieber%fb10vax.i@... */

begin
var i: integer; 
var a: array of integer;
procedure P(x: integer):                           % x name parameter
x := 0; while i>0 do x := x + i; i := i-1 od       % i global variable
end P;
 ...
i := 10;
P(a[i])                       % changes the contents of a[10], ... a[1]
 ...
end

It's not hard to see (or to prove formally), what this program does.
So what's unexpected ?  
...
Kurt. 
/* End of text */

I believe that has an easy answer.  Call the procedure (\x.P).  We can
prove using an equational calculus of assignment programs (see for
example the "Laws of Programming" calculus of Hoare et al.  CACM, Aug
87) and a little induction that
	P = P'	(assuming i >= 0)
where P' is
	(x,i) := (i*i, 0)
If we have a Church-Rosser property for our calculus, then the
equality
	((\x.P) a[i]) = ((\x.P') a[i])
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jon Riecke | 3 Jun 1988 15:01
Picon

Seminar announcement


		    *****SEMINAR ANNOUNCEMENT****

This past Wednesday, we began discussing the recent work of Luke Ong
on the "lazy" lambda calculus.  There seems to be enough interest in
discussing more papers this summer, so we propose to have an informal
occasional seminar at MIT.  Some possible topics:
      1. Plotkin's partial function models and his metalanguage for
         denotational semantics;
      2. ML type inference;
      3. Moggi's thesis;
      4. Other recent work in semantics or type theory.
The first meeting (maybe two) will be spent finishing Ong's paper;
people can still join the current discussion quite easily.

We propose Tuesday or Thursday afternoons as a meeting time, since
Wednesdays seem to be a bad time for many people.  (The seminar
will meet intermittently, given the usual slate of conferences and
vacations.)  If you are interested, please send e-mail to either
of us with times you CANNOT come, and topics you would like to discuss
and/or present.

--Jon Riecke and Bard Bloom
  riecke@..., bard <at> theory.lcs.mit.edu
Permalink | Reply | 0 comments |
headers
John Mitchell | 8 Jun 1988 02:51
Picon

Church-Rosser for typed systems

A year or two ago, Furio Honsell pointed out to me that
beta,eta-reduction on terms that look like typed lambda
terms, but are not well-typed, is not Church-Rosser.
The example he showed me was from van Dalen's thesis,
and also mentioned earlier by Nederpelt, so certainly 
well-known to the Automath group. A simple example is

   \x:A. (\ y:B. y) x

which beta-reduces to \x:A.x, and eta-reduces to \y:B.y.
These are not alpha equivalent (assuming A and B are different).
In particular, this example shows that C-R FOR TYPED LAMBDA
CALCULUS DOES NOT FOLLOW FROM C-R FOR UNTYPED LAMBDA CALCULU,
at least not immediately, and not in any other way I can see.
Any proof of C-R must take the typing rules into account.
(NOTE: I am only speaking about beta, eta-reduction. The
situation is different for beta only.)

I would also like to emphasize that this has nothing to do with
the fact that types are written explicitly using \x:A notation,
instead of the somewhat more common practice of giving each
variable a fixed type. In the alternate presentation,
alpha-conversion must be restricted so that we only replace 
one bound variable by another with the same type. With this 
restriction, the above example still applies, since \x.x
and \y.y  are not alpha-convertible as typed terms when the
types of x and y differ.
Permalink | Reply | 0 comments |
headers
Val Breazu-Tannen | 8 Jun 1988 04:33

Church-Rosser for typed systems


In what you call the alternate (actually, historically first)
presentation of the simply typed lambda calculus (Barendregt, Appendix
A), you have a different way of defining terms, and
        A     B
      \x . (\y . y) x 
is not a term at all. For this presentation, it seems to me that typed
CR follows from

1) CR for the untyped calculus built on typed variables (assume that
the sets of variables of distinct types are disjoint and take the set
of variables of the untyped calculus to be the union of all the sets
of typed variables; the (well-)typed terms will be a subset of these
untyped terms

2) well-typedness is preserved by beta and eta reduction.

                      --- * ---

For the other presentation, one defines "raw" terms, such as
      \x:A. (\ y:B. y) x
and then gives rules for deriving typing judgements about raw terms
under type assignments to variables.

As you point out, CR fails for raw terms, otherwise we would invoke a
subject-reduction-theorem-like result (which holds) and obtain CR for
reductions on derivable typing judgements.

However, one can at least preserve the IDEAS of the proof of CR for
the untyped calculus. First prove that beta, by itself, is
(Continue reading)

Permalink | Reply | 0 comments |
headers
John Mitchell | 8 Jun 1988 05:10
Picon

Re: Church-Rosser for typed systems

The point of the example is this. It is often claimed that
CR for typed lambda calculus follows immediately from CR 
for untyped lambda calculus, because every typed term (in
the usual formulation) looks just like an untyped term.
However, that argument applies equally well to the term
\x.(\y.y)x, where x and y have different types. But since
confluence fails from this term (assuming beta, eta), the
reasoning that led you to conclude CR for typed lambda calculus
is flawed. Have I clarified it for you?

John
Permalink | Reply | 0 comments |
headers
Bard Bloom | 8 Jun 1988 01:25
Picon

Church-Rosser for typed systems


> In what you call the alternate (actually, historically first)
> presentation of the simply typed lambda calculus (Barendregt, Appendix
> A), you have a different way of defining terms, and
>         A     B
>       \x . (\y . y) x 
> is not a term at all. 

In the simply typed lambda calculus, Val is of course right.

How about in a lambda calculus with subtyping, in which a term of type A can
be interpreted as one of type B?  Yes, it's not the classical simply typed
case, but it's reasonably common in real life.  Say, nat is the type of
naturals (0,1,2,3..) and int is integers (...-2,-1,0,1,2...).  Every nat can
be understood as an int (nat is a subtype of int); consider:
     \x:nat. (\y:int . y) x
It beta-reduces to \x:nat.x, and eta-reduces to \y:int.y.

This one is somewhat persuasive.  There's an implicit coercion going on, but
in a simply typed calculus with subtypes it is hard to say formally just what
the coercion is.  When I try to say, "(\y:int.y) coerced to be nat->nat", I
find myself saying "\x:nat. (\y:int.y) x".    

In any event, this term is certainly well-typed, and does not conflue (*)
under beta+eta.  I'll say "M conflues" for "the reduction relation restricted
to descendents of M is confluent", mostly because it sounds funny.

It might conflue if we throw in a suitable subtyping rule: 
   If s is a subtype of t, then \x:t.M --> \x:s.M.
This rule seems plausible in the sense that subtyping is plausible, and
(Continue reading)

Permalink | Reply | 0 comments |
headers
Kurt Sieber | 8 Jun 1988 11:32
Picon

specification logic and call by name


Thanks for your clarifying comments.  I think I haven't done a good
job by mixing
- the denotational/operational discussion,
- my critique in specification logic.
Let's talk only about specification logic now.

1. Using value identifiers	

You are right: We can ADD value identifiers to specification logic,
without throwing away name parameters.  But I don't think that this is
only CONVENIENT (as you expressed it), I consider it as IMPORTANT.

Here is an example:

c is a VALUE identifier and x is a LOCATION identifier (which I
would also like to add; I can't see why location-returning thunks
should be less problematic than value-returning thunks). 

Let the second order procedure P be specified by:
spec(P):   (all c,Q. {x=c} Q {x = c+1} => {x=c} P(Q) {x=c+2})
In words: Whenever the parameter Q increments x by 1, then P(Q)
increments x by 2.   

Let the parameterless procedure Q' be specified by:
spec(Q'):   all c. {x=c and c>5} Q' {x=c+1}
In words: Q' increments x by 1, provided its initial contents is >5.

Now we want to prove 
(*)   (spec(P) & spec(Q')) => all c. ({c>5 and x=c} P(Q') {x=c+2})
(Continue reading)

Permalink | Reply | 0 comments |
headers
kim | 8 Jun 1988 15:40
Picon

Re: Bard's message on subtypes

It's a bit off of the subject, but I wanted to point out something subtle going on in Bard's example:
	\x:nat. (\y:int . y) x
and that is that this term does NOT have type nat -> nat.  Straightforward
use of the typing rules in Cardelli or Cardelli & Wegner shows that
the application of (\y:int . y) to x will only take place if x is first typed
as (coerced to be) an int.  Thus the function has type nat -> int.  The eta
reduction gives a function of type int -> int which of course can also be typed as nat -> int.  However int -> int
and nat -> nat are incompatible types and in
general a function from int to int canNOT be "coerced to be nat -> nat".
   Finally note that in "Bounded Fun" (the extension of second order lambda
calculus with bounded type quantification), 
	\x:nat . (\t<=int. \y:t. y) (nat) x
does have type nat -> nat.
   It's a bit off of the main subject, but worthwhile keeping track of since
subtypes end up being fairly slippery in typing.
	Kim Bruce
	Kim Bruce
Permalink | Reply | 0 comments |

Gmane