rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

HI,

Rewriting of combinator expressions according to the rules
such as 
I x -> x
W f x -> f x x
S x y z -> x z (y z)

terminates if the terms are well-typed, but not in general.

This could be proved by expressing I, W, S, etc as lambda-terms
and using the termination of beta-reduction (for well-typed terms).

But proofs to do with beta-reduction have complications to do with 
substitution.  Can anyone give me pointers to published proofs
of the termination of rewriting well-typed combinator expressions,
without going via lambda-calculus and beta-reduction?

Thanks for any help

Jeremy Dawson

Re: rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

On Aug 3, 2004, at 3:31 AM, Jeremy Dawson wrote:

> [The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>
> HI,
>
> Rewriting of combinator expressions according to the rules
> such as
> I x -> x
> W f x -> f x x
> S x y z -> x z (y z)
>
> terminates if the terms are well-typed, but not in general.
>
> This could be proved by expressing I, W, S, etc as lambda-terms
> and using the termination of beta-reduction (for well-typed terms).
>
> But proofs to do with beta-reduction have complications to do with
> substitution.  Can anyone give me pointers to published proofs
> of the termination of rewriting well-typed combinator expressions,
> without going via lambda-calculus and beta-reduction?
>
> Thanks for any help
>
> Jeremy Dawson
>

Announcement: A Type-Based Analyzer for the Pi-Calculus

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

We would like to announce availability of the first implementation of
TyPiCal: a type-based static analyzer for the pi-calculus.
TyPiCal is based on a series of our work on type systems for
the pi-calculus (some of which are listed below), and can 
perform the following analyses and transformations for pi-calculus processes.

 - Lock-freedom analysis [1], which finds communications that
   will eventually succeed, without suffering from deadlocks, livelocks, etc.

 - Deadlock-freedom analysis [2], which finds communications that
   will eventually succeed unless the whole process diverges

 - Useless-code elimination [3], which eliminates communications that
   do not affect the observable behavior of the process

 - Information flow analysis [4], which finds values whose information
   is kept secret to the environment.

All the analyses and transformation above are fully automatic (no type
annotation is required), thanks to the recent result [4].

TyPiCal is available from:

   http://www.kb.cs.titech.ac.jp/~kobayasi/typical/

References
=========
  [1] Naoki Kobayashi, "A Type System for Lock-Free Processes,"

Re: rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Jeremy Dawson wrote:

>[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>
>HI,
>
>Rewriting of combinator expressions according to the rules
>such as 
>I x -> x
>W f x -> f x x
>S x y z -> x z (y z)
>
>terminates if the terms are well-typed, but not in general.
>
>This could be proved by expressing I, W, S, etc as lambda-terms
>and using the termination of beta-reduction (for well-typed terms).
>
>But proofs to do with beta-reduction have complications to do with 
>substitution.  Can anyone give me pointers to published proofs
>of the termination of rewriting well-typed combinator expressions,
>without going via lambda-calculus and beta-reduction?
>
>Thanks for any help
>
>Jeremy Dawson
>
>  

Re: rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

On Aug 4, 2004, at 6:17 AM, Thorsten Altenkirch wrote:

> I believe that one-step reduction is a bit of a historical mistake: 
> who executes their programs by
> rewriting them to normal forms (maybe mathematicans)? More realistic 
> is to define a big-step semantics which
> can be easily turned into a functional program which can be further 
> turned into a machine (by making it tail
> recursive) .

While this has nothing to do with the original question, I need to 
reply to this statement. It is of course extremely natural to have a 
one-step relation that reduces programs one step at a time, until the 
program is in a certain shape. This is exactly what the machine does, 
and it is therefore appropriate to call this form of semantics an 
abstract, text-based machine (as I have done for 20 years now).

What is wrong is to reduce to normal form. Programs (statements and 
expressions) are never evaluated to normal form on any realistic 
machine; the machines stop when it reaches a "value" i.e., something 
that we all agree is a final answer. Examples are numbers, booleans, 
and I'd hope closures. The body of the closure can be an arbitrary 
term.

As for the choice between a big-step semantics (as you call it) and a 
one-step reduction semantics, you should probably understand that it 
all depends on (1) the purpose of your model (why do you make a model 
of a programming language) and (2) what's in your programming language. 

Re: rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Matthias Felleisen wrote:
> On Aug 4, 2004, at 6:17 AM, Thorsten Altenkirch wrote:
> 
>> I believe that one-step reduction is a bit of a historical mistake: 
>> who executes their programs by
>> rewriting them to normal forms (maybe mathematicans)? More realistic 
>> is to define a big-step semantics which
>> can be easily turned into a functional program which can be further 
>> turned into a machine (by making it tail
>> recursive) .
> 
> 
> While this has nothing to do with the original question, I need to reply 
> to this statement. It is of course extremely natural to have a one-step 
> relation that reduces programs one step at a time, until the program is 
> in a certain shape. This is exactly what the machine does, and it is 
> therefore appropriate to call this form of semantics an abstract, 
> text-based machine (as I have done for 20 years now).

If somebody asks me (or you) to write an interpreter for a functional programming
language, I suspect we both would come up with something like (obviously your
versions would have more brackets):

data Tm = Var String | App Tm Tm | Lam (String,Tm)

data Val = VClos (String,Tm) Env

type Env = [(String,Val)]

Re: rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

On Aug 4, 2004, at 10:51 AM, Thorsten Altenkirch wrote:

>
>
> Matthias Felleisen wrote:
>> On Aug 4, 2004, at 6:17 AM, Thorsten Altenkirch wrote:
>>> I believe that one-step reduction is a bit of a historical mistake: 
>>> who executes their programs by
>>> rewriting them to normal forms (maybe mathematicans)? More realistic 
>>> is to define a big-step semantics which
>>> can be easily turned into a functional program which can be further 
>>> turned into a machine (by making it tail
>>> recursive) .
>> While this has nothing to do with the original question, I need to 
>> reply to this statement. It is of course extremely natural to have a 
>> one-step relation that reduces programs one step at a time, until the 
>> program is in a certain shape. This is exactly what the machine does, 
>> and it is therefore appropriate to call this form of semantics an 
>> abstract, text-based machine (as I have done for 20 years now).
>
> If somebody asks me (or you) to write an interpreter for a functional 
> programming
> language, I suspect we both would come up with something like 
> (obviously your
> versions would have more brackets):

But why would I even start with the premise of wanting to write an 
interpreter? That's just another way of saying "I want big-step 

Re: rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

At Wed, 4 Aug 2004 11:00:20 -0400, Matthias Felleisen wrote:
> > If somebody asks me (or you) to write an interpreter for a functional 
> > programming
> > language, I suspect we both would come up with something like 
> > (obviously your
> > versions would have more brackets):
> 
> But why would I even start with the premise of wanting to write an 
> interpreter? 

One reason to prefer the big-step as interpreter semantics is that it
is directly executable (which brings lots of benefits: easy
experimentation, test suites, etc etc). Of course, and perhaps in
support of Matthias's point, the one-step semantics is just as
executable. So, let me take this chance and to plug PLT Redex, one tool
that takes such semantics and executes them:

  http://people.cs.uchicago.edu/~robby/pubs/papers/rta2004-mfff.pdf

Robby

Paper: Acute - high-level programming language design for distributed computation

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Dear All,

We would like to announce the papers

 * Acute: high-level programming language design for distributed
   computation

 * Acute: high-level programming language design for distributed
   computation. Design rationale and language definition

which are available from

 http://www.cl.cam.ac.uk/users/pes20/acute

together with some example Acute code.  The first paper gives an
overview of the main design choices; the second contains an extended
design discussion, an introduction to the semantics, examples
illustrating the semantics, and the full language definition.

This work explores the design space of high-level languages for
distributed computation, focussing on typing, naming, and version
change.  We have designed, formally specified and implemented an
experimental language, Acute, which extends an OCaml core to support
distributed development, deployment, and execution, allowing type-safe
interaction between separately-built programs.  It is expressive
enough to enable a wide variety of distributed infrastructure layers
to be written as simple library code above the byte-string network and
persistent store primitives, disentangling the language runtime from

Re: rewriting of typed combinator expressions

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

> One reason to prefer the big-step as interpreter semantics is that it
> is directly executable (which brings lots of benefits: easy
> experimentation, test suites, etc etc). Of course, and perhaps in
> support of Matthias's point, the one-step semantics is just as
> executable. So, let me take this chance and to plug PLT Redex, one tool
> that takes such semantics and executes them:
> 
>   http://people.cs.uchicago.edu/~robby/pubs/papers/rta2004-mfff.pdf

Thanks for that reference. I, too, find one-step semantics more useful
when looking at operational aspects of programming language designs
(big-step hides those details, which is fine when your focus is on other
things). And yes, it is easy to get such rules wrong. 

Even non-language-designers tend to appreciate the chance to experience 
the reduction semantics of their language step-by-step, if they ever get that 
chance (mainly for learning, but occasionally also for debugging, and to get
a better feeling for resource usage). As someone who was taught functional 
programming with reduction systems in the Berkling/Kluge tradition, I can 
only say that mainstream fp systems skip over some difficult but interesting 
aspects of fpl implementation, and that mainstream functional programmers 
are worse off because of this, especially when they want to understand the
interactions with their languages' i/o or concurrency features. It is nice that 
PLT Scheme tries to fight that trend.

(to react to an earlier remark in this thread: if one takes programming with