Changes between Version 2 and Version 3 of PIL

Timestamp:

10/03/24 11:06:50 (20 months ago)

Author:

siegel

Comment:

--

PIL

@@ -37 +37 @@
 - `$set<T>` : finite set of `T`, ops to add, contains, remove, size, ...
 - `$map<T1,T2>` : finite map from `T1` to `T2`, ops to put, get, containsKey, ...
-- `$fun<T1,T2>` : total functions from `T1` to `T2`
+- `$fun<T1,T2>` :  "logic functions":  deterministic, total, side-effect free functions from `T1` to `T2`
 - `$tuple<T,...>` : tuples of specified type (similar to struct)
 - `$rel<T,...>` : relations of specified type (set of tuples)
@@ -50 +50 @@
 - `t.i`
 - `($tuple<T1,...>){ x1, ... }`
-- `$pure $tuple<T1,...> $tuple_write($tuple<T1,...> t, $int i, Ti x);`
+- `$logic $tuple<T1,...> $tuple_write($tuple<T1,...> t, $int i, Ti x);`
 
 Mutating expressions:
@@ -60 +60 @@
 - `s1 == s2`
 - `($set<T>)$empty`   // empty set of type T
-- `$pure _Bool $set_in(T x, $set<T> s);`  // is x an element of s?
+- `$logic _Bool $set_in(T x, $set<T> s);`  // is x an element of s?
 - `$pure $set<T> $set_with($set<T> s, T x);` // s U {x}
 - `$pure $set<T> $set_without($set<T> s, T x);` // s - {x}
@@ -155 +155 @@
 === Lambda expressions
 
-These have the form
-{{{
-  $lambda (T1 x1, ..., Tn xn) {U1 v1=init1; ... Um vm=initm; expr}
-}}}
-where the `Ti` and `Uj` are types, the `xi` and `vj` are variables, and `expr` is an expression in which the only variables that can occur free are the `x1`,..., `xn`, `v1`,..., `vm`.  The initializer expressions `initj` are expressions using any variables in scope.  The expression has type `$fun<T1,...,Tn; V>`, where `V` is the type of `expr`.
+There are two kinds of lambda expressions.  The first kind defines a procedure, the second a logical function.
+
+Procedural lambda syntax:
+{{{
+  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) { S1; ... }
+}}}
+where
+* the `Ti` and `Uj` are types
+* the `xi` and `vj` are variables
+* R is a type (the return type), which may be void
+* {S1; ...} is a block (same as in function definition)
+* the only variables that can occur free in the block are the xi and vj
+* if R is not void, the block must return a value of type R
+
+The type of this expression is `R(T1, ..., Tn)`.
+
+Logic function lambda syntax:
+{{{
+  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) expr
+}}}
+where 
+* the `Ti` and `Uj` are types
+* the `xi` and `vj` are variables
+* R is a type (the return type), which cannot be void
+* `expr` is a side-effect-free expression of type R 
+* the only variables that can occur free in `expr` are the xi and vj
+
+The type of this expression is `$fun<R, T1, ..., Tn>`. 
+
+In both cases, the initializer expressions `initj` are expressions using any variables in scope.
 
 ==== Semantics
+
+FIX THIS:  difference between logic and procedural functions...
+
+
 
 The lambda expression is evaluated to yield a *closure*:  an ordered pair consisting of a dyscope and an expression.  The dyscope has variables `v1`, ..., `vm`, initialized by evaluating `init1`, ..., `initm`.  The dyscope has no parent scope, it is associated only with the closure.  The expression is `expr`.  The dyscope is destroyed whenever it becomes unreachable, i.e., whenever no part of the state is assigned the closure.