Funcons-beta : Generic.cbs | PRETTY | PDF

Generic abstractions

[
  Type   abstractions
  Funcon abstraction
  Funcon closure
  Funcon enact
]

Meta-variables
  T <: values
  T? <: values?

Type
  abstractions(_:computation-types)

Funcon
  abstraction(_:T?=>T) : abstractions(T?=>T)

The funcon abstraction(X) forms abstraction values from computations.

References to bindings of identifiers in X are dynamic. The funcon closure(X) forms abstractions with static bindings.

Funcon
  closure(_:T?=>T) : =>abstractions(T?=>T)

closure(X) computes a closed abstraction from the computation X. In contrast to abstraction(X), references to bindings of identifiers in X are static. Moreover, closure(X) is not a value constructor, so it cannot be used in pattern terms in rules.

Rule
  environment(Rho) |- closure(X) ---> abstraction(closed(scope(Rho, X)))

Funcon
  enact(_:abstractions(T?=>T)) : T?=>T

enact(A) executes the computation of the abstraction A, with access to all the current entities.

Rule
  enact(abstraction(X)) ~> X

↑ →