Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:immutable_abstract_data_types [2008/05/28 05:01] vkuncak |
sav08:immutable_abstract_data_types [2008/05/28 05:03] (current) vkuncak |
||
---|---|---|---|
Line 34: | Line 34: | ||
**Value construction consequence:** Let $v$ be a value of an immutable ADT computed by a (potentially mutable) function in a type safe language. Then there exists a finite expression tree whose nodes are operations of ADT and whose leaves are either nullary operations of ADT or non-ADT values, such that this expression tree evaluates to value $v$. | **Value construction consequence:** Let $v$ be a value of an immutable ADT computed by a (potentially mutable) function in a type safe language. Then there exists a finite expression tree whose nodes are operations of ADT and whose leaves are either nullary operations of ADT or non-ADT values, such that this expression tree evaluates to value $v$. | ||
- | Note that this consequence does not rely on any properties of the function computing $v$. The function could be arbitrarily complex. The expression tree is the part of the computation that is relevant for computing $v$ (for non-ADT values, it need not keep track how they are computed). | + | Note that this consequence does not rely on any properties of the function computing $v$. The function could be arbitrarily complex, and need not terminate for all inputs, as long as we consider an evaluation that computed $v$. The expression tree is the part of the computation that is relevant for computing $v$ (for non-ADT values, it need not keep track how they are computed). |
In the previous example, we are sure that all natSet values computed in any code that uses the ADT are obtained by starting from empty and applying operations insert,remove,union. | In the previous example, we are sure that all natSet values computed in any code that uses the ADT are obtained by starting from empty and applying operations insert,remove,union. | ||