Outline

### Giving

[
Entity given-value
Funcon initialise-giving
Funcon give
Funcon given
Funcon no-given
Funcon left-to-right-map
Funcon interleave-map
Funcon left-to-right-repeat
Funcon interleave-repeat
Funcon left-to-right-filter
Funcon interleave-filter
Funcon fold-left
Funcon fold-right
]
Meta-variables
T, T′ <: values
T? <: values?
Entity
given-value(_:values?) |- _ ---> _

The given-value entity allows a computation to refer to a single previously-computed V:values. The given value ( ) represents the absence of a current given value.

Funcon
initialise-giving(X:( )=>T′) : ( )=>T′
~> no-given(X)

initialise-giving(X) ensures that the entities used by the funcons for giving are properly initialised.

Funcon
give(_:T, _:T=>T′) : =>T′

give(X, Y) executes X, possibly referring to the current given value, to compute a value V. It then executes Y with V as the given value, to compute the result.

Rule
given-value(V) |- Y ---> Y′
------------------------------------------------
given-value(_?) |- give(V:T, Y) ---> give(V, Y′)
Rule
give(_:T, W:T′) ~> W
Funcon
given : T=>T

given refers to the current given value.

Rule
given-value(V:values) |- given ---> V
Rule
given-value( ) |- given ---> fail
Funcon
no-given(_:( )=>T′) : ( )=>T′

no-given(X) computes X without references to the current given value.

Rule
given-value( ) |- X ---> X′
------------------------------------------------
given-value(_?) |- no-given(X) ---> no-given(X′)
Rule
no-given(U:T′) ~> U

#### Mapping

Maps on collection values can be expressed directly, e.g., list(left-to-right-map(F, list-elements(L))).

Funcon
left-to-right-map(_:T=>T′, _:(T)*) : =>(T′)*

left-to-right-map(F, V*) computes F for each value in V* from left to right, returning the sequence of resulting values.

Rule
left-to-right-map(F, V:T, V*:(T)*)
~> left-to-right(give(V, F), left-to-right-map(F, V*))
Rule
left-to-right-map(_, ( )) ~> ( )
Funcon
interleave-map(_:T=>T′, _:(T)*) : =>(T′)*

interleave-map(F, V*) computes F for each value in V* interleaved, returning the sequence of resulting values.

Rule
interleave-map(F, V:T, V*:(T)*)
~> interleave(give(V, F), interleave-map(F, V*))
Rule
interleave-map(_, ( )) ~> ( )
Funcon
left-to-right-repeat(_:integers=>T′, _:integers, _:integers) : =>(T′)*

left-to-right-repeat(F, M, N) computes F for each value from M to N sequentially, returning the sequence of resulting values.

Rule
is-less-or-equal(M, N) == true
-------------------------------------------------------------------------
left-to-right-repeat(F, M:integers, N:integers)
~> left-to-right(give(M, F), left-to-right-repeat(F, int-add(M, 1), N))
Rule
is-less-or-equal(M, N) == false
----------------------------------------------
left-to-right-repeat(_, M:integers, N:integers) ~> ( )
Funcon
interleave-repeat(_:integers=>T′, _:integers, _:integers) : =>(T′)*

interleave-repeat(F, M, N) computes F for each value from M to N interleaved, returning the sequence of resulting values.

Rule
is-less-or-equal(M, N) == true
-------------------------------------------------------------------
interleave-repeat(F, M:integers, N:integers)
~> interleave(give(M, F), interleave-repeat(F, int-add(M, 1), N))
Rule
is-less-or-equal(M, N) == false
-------------------------------------------
interleave-repeat(_, M:integers, N:integers) ~> ( )

#### Filtering

Filters on collections of values can be expressed directly, e.g., list(left-to-right-filter(P, list-elements(L))) to filter a list L.

Funcon
left-to-right-filter(_:T=>booleans, _:(T)*) : =>(T)*

left-to-right-filter(P, V*) computes P for each value in V* from left to right, returning the sequence of argument values for which the result is true.

Rule
left-to-right-filter(P, V:T, V*:(T)*)
~> left-to-right(when-true(give(V, P), V), left-to-right-filter(P, V*))
Rule
left-to-right-filter(_) ~> ( )
Funcon
interleave-filter(_:T=>booleans, _:(T)*) : =>(T)*

interleave-filter(P, V*) computes P for each value in V* interleaved, returning the sequence of argument values for which the result is true.

Rule
interleave-filter(P, V:T, V*:(T)*)
~> interleave(when-true(give(V, P), V), interleave-filter(P, V*))
Rule
interleave-filter(_) ~> ( )

#### Folding

Funcon
fold-left(_:tuples(T,T′)=>T, _:T, _:(T′)*) : =>T

fold-left(F, A, V*) reduces a sequence V* to a single value by folding it from the left, using A as the initial accumulator value, and iteratively updating the accumulator by giving F the pair of the accumulator value and the first of the remaining arguments.

Rule
fold-left(_, A:T, ( )) ~> A
Rule
fold-left(F, A:T, V:T′, V*:(T′)*) ~> fold-left(F, give(tuple(A, V), F), V*)
Funcon
fold-right(_:tuples(T,T′)=>T′, _:T′, _:(T)*) : =>T′

fold-right(F, A, V*) reduces a sequence V* to a single value by folding it from the right, using A as the initial accumulator value, and iteratively updating the accumulator by giving F the pair of the the last of the remaining arguments and the accumulator value.

Rule
fold-right(_, A:T′, ( )) ~> A
Rule
fold-right(F, A:T′, V*:(T)*, V:T) ~> give(tuple(V, fold-right(F, A, V*)), F)

 From the PLanCompS Project CBS-beta issuesâ€¦ Suggest an improvementâ€¦