Re: [CZT-Devel] schema composition type rule - query

[Mark U. <ma...@cs...>]

Leo,

Seems fine to me.  It is only the *matching* undashed-dashed pairs that are
unified.

In some kinds of framing schemas, it is useful to have other non-matching
primed (or unprimed) variables.

If you see a problem, you need to say what problem you see :-)

Mark


On 30 November 2011 03:38, Leo Freitas <leo...@ne...> wrote:

> Hi guys,
>
> I think there was discussion about this, but I don't know the details.
> From the Standard (13.2.6.22), I infer that
> the type for (LHS \semi RHS) is given by intricate filtering of bindings
> as follows:
>
> a) match = all the bindings of RHS that are NextStroke decorated in LHS
> (e.g., match set)
> b) B3       = LHS bindings  MINUS bindings of match decorated with
> NextStroke
> c) B4    = RHS bindings MINUS match
> d) result = B3 cup B4
>
> ex:
>
> S == [ x: \nat ]
> T == [ y: \nat ]
> LHS == [ \Delta S; in? : \nat ]
> RHS == [ \Delta S; out!: \nat ]
> Op == LHS \semi RHS
>
> what are the bindings of Op? I would expect them to be x, x', in?, out!
> but int I/O gets filtered out by the Std def?
> What if the composition is not homogenous like in
>
> LHS == [ \Delta S; \Delta T; in? : \nat ]
> RHS == [ \Delta S; out!: \nat ]
> Op == LHS \semi RHS
>
> or
>
> LHS == [ \Delta S;  in? : \nat ]
> RHS == [ \Delta S; \Delta T; out!: \nat ]
> Op == LHS \semi RHS
>
> bindings of Op given by the typechecker are x, x', y, y', in?, out!....
> That is despite the fact there might be more dashed
> variables in one side than the other. Any thoughts?
>
> Similarly, how to trust the definition for piping?
>
> Best,
> Leo
>
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure
> contains a definitive record of customers, application performance,
> security threats, fraudulent activity, and more. Splunk takes this
> data and makes sense of it. IT sense. And common sense.
> http://p.sf.net/sfu/splunk-novd2d
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>