[SEEK-UCSD]Re: [kepler-dev] Re: question on typing processes and higher-order functions a la map

Joseph Goguen goguen at cs.ucsd.edu
Thu Jun 3 16:29:22 PDT 2004

Dear Bertram and others,

The hardware specification and verification community has faced essentially
the same issue, since hardware units (adders, multiplexers, registers, ...)
and even transistors, prose essentially similar problems.  Here one popular
solution is to view wires as passing infinite streams of bits (or perhaps
tokens at a higher level of abstraction), and to view the units as functions
on such streams.  Sometimes it is adequate to describe the unit as a function
which is applied to the tokens currently on its inputs, thus giving rise to
an infinitary analog of the map (or mapcar) higher order function.  But more
often the state of the unit also plays a role.

The factors example is interesting because the nature of the tokens differs
from input to output: input tokens are integers, while output tokens are
lists of integers.  So we could view this actor as a function of type

	<<int>> --> <<[int]>>

where <<..>> is the stream type constructor and [..] is the list type

Proofs about infinitary data structures (like streams) are not so simple as
for the more familiar finitary data structures.  One common technique is
co-induction.  An example of a correctness proof, using coinduction, for an
optimization rule in hardware design with infinite stream semantics, can be
found at


Most of the page is the specification, the proof itself is mostly automated,
using our circular coinductive rewriting algorithm.

I hope this is of some help,


>X-Sender: eal at mho.eecs.berkeley.edu
>From: "Edward A Lee" <eal at eecs.berkeley.edu>
>Cc: "Stephen Andrew Neuendorffer" <neuendor at eecs.berkeley.edu>,
>        Bertram Ludaescher <ludaesch at sdsc.edu>, kepler-dev at ecoinformatics.org,
>        Liying SUI <lsui at cs.ucsd.edu>,
>        "ptolemy-hackers" <ptolemy-hackers at eecs.berkeley.edu>,
>        SEEK-UCSD <seek at sdsc.edu>
>X-BeenThere: seek at sdsc.edu
>X-Mailman-Version: 2.0.8
>Precedence: bulk
>List-Help: <mailto:seek-request at sdsc.edu?subject=help>
>List-Post: <mailto:seek at sdsc.edu>
>List-Subscribe: <http://lists.sdsc.edu/mailman/listinfo.cgi/seek>,
>	<mailto:seek-request at sdsc.edu?subject=subscribe>
>List-Id: SDSC/UCSD SEEK participants  <seek.sdsc.edu>
>List-Unsubscribe: <http://lists.sdsc.edu/mailman/listinfo.cgi/seek>,
>	<mailto:seek-request at sdsc.edu?subject=unsubscribe>
>List-Archive: <http://lists.sdsc.edu/pipermail/seek/>
>Date: Thu, 27 May 2004 09:08:11 -0700
>X-Spam-Flag: Spam NO
>X-Scanned-By: milter-spamc/0.15.245 (fast.ucsd.edu []); pass=YES; Thu, 27 May 2004 09:30:10 -0700
>X-Spam-Status: NO, hits=-4.80 required=5.00
>X-Spam-Level: Level 
>The issue here is that an actor with an input type of int
>and output type of int is not a function with
>type signature:
>    factors_1 :: int -->int
>The factors example is a good one.  It is a function
>with type signature:
>    factors_2 :: <int>--><int>
>The idea of applying "map" to the first version factors_1
>of this to get the second factors_2 doesn't work because the
>domain of map is functions, and the first version
>is not a function.
>It is tempting to try to define a "function" for an
>individual firing of an actor, but to do this right,
>you need to include in the domain of the function the
>state of the actor.  Thus, the factors actor could
>be viewed as having two firing functions:
>   factors_3 :: (int, int) -->int
>   factors_4 :: int -->int
>where both functions take the state of the actor (encoded as
>an int). The second function requires no input on the input port,
>but produces an output on the output port.  An execution of
>this actor starts by using factors_3, then switches to
>factors_4 until all the factors are produced, then goes back
>to factors_3.  You can build factors_2 from this, but you
>need an infinite-state automaton to do it.
>These and related semantic issues are addressed in the following
>paper, which has never been submitted anywhere for publication because
>there are still vexing open issues:
>Given this, there is no difficulty with the Ptolemy II
>type system.  The key is to recognize that every connection
>has type <t>. The type of the port is t, but that is not
>the type signature of the actor.
>It is possible to have streams of streams, e.g. <<int>>.
>A few years ago we developed multidimensional SDF (MDSDF),
>implemented in Ptolemy Classic.  To be useful, we usually
>need for all but one of the dimensions to be finite,
>otherwise there is an intrinsic ambiguity in how to make
>progress in an infinite execution.  In fact, MDSDF can
>be viewed as a way to get static analysis to ensure
>dimensional consistency without the pitfalls of
>dependent type systems (specifically, the MDSDF analysis
>is decidable, whereas in general, analysis of dependent
>types is not... for those who don't know, dependent types
>are types that are "indexed" by values, such as int[10].
>Steve is right that sometimes the undecidable problem can
>be solved, as in compiler optimizations that eliminate array
>bounds checking, but the factors example is a good illustration
>where no compiler optimization will work...  Any type inference
>on this will fail.)
>MDSDF is described in the following paper, which was submitted
>an astonishing 8 years before it was finally published (so much
>for the value of technical journals):
>At 12:59 PM 5/26/2004 -0700, Bertram Ludaescher wrote:
>>sorry for replying late.
>>Here is again the issue (see earlier posting):
>>A factors actor can be conceived of as consuming one input token I (an int)
>>and producing multiple output tokens O_1, ..., O_n, the prime factors
>>of I:   factors(I) = O_1, ... O_n
>>One way to assign a type to factors is:
>>        factors :: int --><int>
>>where <a>stands for a stream (or sequence, possibly infinite) of
>>items of type 'a'.
>>If such a type is indeed assigned, it leads to an interesting typing
>>issue, when applying the higher-order function
>>        map :: (a-->b) --><a>--><b>
>>to factors. According to the obvious type inference, the type of the
>>"pipelined" version of factors is
>>        Factors :: <int>-->< <int>>
>>where Factors is defined as being the same as map(factors).
>>If we treat <a>just as a list [a], all is well.
>>On the other hand, on Ptolemy one may look at factors as follows:
>>        factors :: int -->int
>>indicating that
>>(i) the input and output ports, respectively of factors are int (not
>>arrray of int or sequence or list of int..), and
>>(ii) stating that the token consumption rate/pattern is
>>        factors :: 1 x  int  -->n x int
>>(1 input token is consumed an n output tokens are produced)
>>Indeed a straightforward modeling in Ptolemy using the PN director
>>(not SDF as I indicated earlier) would now produce
>>        Factors <10, 20, ...>= <2, 5, 2, 2, 5, ...>
>>and thus loose the information which factors go with which number.
>>There are different ways to handle it:
>>(a) not at all (sometimes this behavior might be desired -- examples
>>(b) use a collection type (array in Java, list, etc) and type
>>        factors :: int -->[int]
>>resulting in a process of the form
>>        Factors :: <int>-->< [int] >
>>        Factors <10,20,...>= < [2,5], [2,2,5], ... >
>>(c) use a special blend (a variant of (a)!?)
>>        factors :: int --><int>
>>that when viewed as a process gives
>>        Factors <int>--><int>_;
>>where the subscript ";" indicates a punctuated stream:
>>        Factors <10, 20, ...>= < 2, 5 ; 2, 2, 5 ; ... >
>>in which special control tokens are inserted into the data streams
>>that have the purpose preserving the nesting structure of variant (b)
>>while having the streaming features of variant (a).
>>Does that make sense?
>>I'm interested in a type system than can do all of the above in a neat
>>way (and then we add semantic types)
>>>>>>>"SAN" == Stephen Andrew Neuendorffer <neuendor at eecs.berkeley.edu>
>>>At 01:08 PM 5/25/2004, Bertram Ludaescher wrote:
>>>>Liying Sui and I recently came across the following typing problem:
>>>>Consider an actor, say "factors" which computes for a given int I, all
>>>>the prime factors of I. For example factors(20) = [2,2,5]
>>>>Thus, the signature of factors is:
>>>>factors :: int -->[int]
>>>>Now assume factors is to be applied on a stream <x1, x2, x3, ...>of
>>>>integers, denoted <int>
>>>>It seems tempting to view the *process* Factors that is so created as
>>>>applying the higher-order map function to factors, i.e.,
>>>>Factors = map(factors)
>>>>There are some interesting typing issues. Let's say map has the
>>>>following type on streams:
>>>>map :: (a-->b) --><a>--><b>
>>>>That is, map takes a function of type (a-->b) and a stream of a's
>>>>(denoted <a>) and returns a stream of b's.
>>>>Therefore the type of the Factors process can be determined to be
>>>>Factors :: <int>-->< [int] >
>>>>Example: Factors( <4, 6, 10, ... >) = < [2,2], [2,3], [2,5], ... >
>>>>So far so good -- no information is lost.
>>>>It seems, however, that in practise sometimes  another process is
>>>>Factors'( <4, 6, 10, ... >) = < 2,2,2,3,2,5, ... >
>>>>Clearly this process Factors' does lose some information (the grouping
>>>>of result tuples into list of prime factors). While for this specific
>>>>example, Factors' is not desirable, such a "flattening" behavior seems
>>>>to be used in practise:
>>>I'm confused: Are you saying that this is what Ptolemy does, and you 
>>>it, or that Ptolemy does not do this, and you would like it to?
>>>Could you consider this to be another higher-order function that takes
>>>expandArray :: <[int]>-><int>?
>>>>Let say we change our original function factors to produce not a list
>>>>of ints, but a stream of them:
>>>>factors' :: int --><int>
>>>>This correspond to a token consumption/production pattern of " 1:* "
>>>>(for each input token, we might get multiple output tokens).
>>>>Is it correct that in Ptolemy II using factors' with an SDF director
>>>>produces a process Factors' on streams that has the signature:
>>>>Factors' :: <int>--><int>
>>>>In order to make this behavior type-correct it seems we may have to
>>>>say that <<int>>= <int>, because we get
>>>>map(factors') = Factors'
>>>>and the former has the type
>>>>map(factors') ::  <int>-->< <int>>
>>>>Note that the type of map(factors') is obtained by using the general
>>>>type of map above:
>>>>map :: (a-->b) --><a>--><b>
>>>>and the applying this to factors' :: int --><int>
>>>>(hence a = int and b = <int>)
>>>>So if indeed Factors' is of the said type we must accept (whether we
>>>>like it or not ;-) that <<int>>= <int>(or in general, nesting
>>>>streams in this way yields a "flat" stream).
>>>>Does Ptolemy II with an SDF director and an actor of type
>>>>myactor :: a --><b>
>>>I don't think this makes sence...  SDF actor functions don't have 
>>access to
>>>the whole stream...  they have access to a fixed length prefix of the 
>>>>produce a process
>>>>MYACTOR :: <a>--><b>
>>>>which thus can be explained as a "special map" over streams with the
>>>>type identity <<b>>= <b>??
>>>why not another HOF: expandStream :: <<b>>-><b>?
>>>I think that the advantage of expandArray over expandStream is that 
>>>are generally finite, while
>>>streams are not, and hence it is more likely that the computation I've
>>>specified actually processes the
>>>data being created...  Note that there are two ways to implement
>>>expandStream (does it produce an infinite stream consisting of the first
>>>element of each input stream, or does it produce an infinite stream that
>>>begins with the first
>>>infinite input stream, and then never gets to the other ones?)
>>>>Thanks in advance!
>>>>Bertram and Liying
>>>>Posted to the ptolemy-hackers mailing list.  Please send administrative
>>>>mail for this list to: ptolemy-hackers-request at ptolemy.eecs.berkeley.edu
>>kepler-dev mailing list
>>kepler-dev at ecoinformatics.org
>Edward A. Lee, Professor
>518 Cory Hall, UC Berkeley, Berkeley, CA 94720
>phone: 510-642-0455, fax: 510-642-2739
>eal at eecs.Berkeley.EDU, http://ptolemy.eecs.berkeley.edu/~eal

More information about the Kepler-dev mailing list