Properties of Expressions#

  • Helpful: Always sends a negative result when it has finished publishing (0 or more results).
  • Side-effect free: Does not have any side-effects and all information produced is in the forms of publications.
    e >> stop =~~= stop
    An asynchronous side-effect free expression can be replaced with an expression v1 | v2 | ... | vn where vi are all the publications of the expression. A synchronous side-effect free expression is equivalent to: Rwait(t1) >> v1 | Rwait(t2) >> v2 | ... | Rwait(tn) >> vn where each pair (ti, vi) is a publication time and value.
  • Pure: Its publications (0 or more) are always the same given the same arguments or values for free variables, and it is side-effect free. This is a generalization of pure functions similar to pure non-deterministic functions.
  • Pure Functional: Always publishes exactly 1 value and is pure. Equivalent to a total mathematical function.
    e =~~= x <x< e
    e >> stop =~~= stop
  • Asynchronous: Ordering of publications of subexpressions does not affect the set of possible results of the expression. (TODO: is this correct?)
  • Silent: Never publishes a value.
    e =~= e >> stop
  • Deterministic: Will always produce the same result regardless of order of publication or scheduling. Note that asynchronous expressions can still be non-deterministic. (TODO: is this correct?)
  • Resilient: The expression will not terminate if pruned.
  • Atomic: The expression e is not effected by concurrently running expressions (including other copies of e). This is probably both atomic and co-atomic (in Kitchen terms).
  • Blocking: The expression will always eventually respond.
  • Strict: All free variables in e are needed without delay. All site calls are strict. The charactature for strict on x is:
    e <x< f =~~= e <x<$ f
    where <x<$ performs termination but not late binding. Expressions can also be strict in specific variables and non-strict in others.
  • Idempotent: Executing an expression more than once has the same effect as executing it once.
    e | e =~~= e
    This is not be an accurate characture because e may not be atomic so it might conflict with itself. However e >> e =~~= e would not be correct either unless e is asynchronous.
  • Talkative: Publishes at least once.
  • Terminating: Will eventually terminate even if it is not pruned.

There are probably a few more that would be useful. This is a work in progress.

Many of these properties have characteristic identities which totally encode their meaning. For instance, an expression e is silent iff the following statement is true.

e =~= e >> stop
(where =~= is equivalence of expression in the semantics.) Similar statements can and should be written for other properties. However this may not be not possible for all; what about purity it needs to be expressed in terms of all evaluations producing the same publications given the same input.

Decidability#

Some of there properties are decidable based on axioms about sites. However most are not. For the undecidable properties it would still be possible to create a conservative estimate that will detect many useful cases of the property.
  • Side-effect free is decided by:
    sideEffectFree (f | g) = sideEffectFree f && sideEffectFree g
    sideEffectFree (f >x> g) = sideEffectFree f && (if not silent f then sideEffectFree g else true)
    sideEffectFree (f <x< g) = sideEffectFree f && sideEffectFree g
    sideEffectFree (f ; g) = sideEffectFree f && (if not talkative f then sideEffectFree g else true)
    (this has not been proved correct)

This section should be completed with deciders and estimates for other properties.

Related Pages#

  • Deparallelization: Has some interesting properties and identities that may be useful.
  • Identities: A list of algebraic identities some of which depend on these properties.

Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-7) was last changed on 17-Oct-2012 17:33 by Arthur Peters