# 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. | ||