A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are O(1)
(i.e., variables only occur once) and copying is an explicit, constant-time and incremental operation. Here is an example:
let (a & b) = (λx. λy. λz. y) in (a & b)
---------------------------------------- step 0
let (a & b) = (λy. λz. y) in (λx0. a) & (λx1. b)
------------------------------------------------ step 1
let (a & b) = (λz. y0 & y1) in (λx0. λy0. a) & (λx1. λy1. b)
------------------------------------------------------------ step 2
let (a & b) = y0 & y1 in (λx0. λy0. λz0. a) & (λx1. λy1. λz1. b)
---------------------------------------------------------------- step 3
(λx0. λy0. λz0. y0) & (λx1. λy1. λz1. y1)
Here, the let (a & b) = t in k
syntax substitutes the occurrences of a
and b
in k
by t
, except it does so incrementally: notice how each lambda is pulled one by one.
There is a problem, though. Eventually, you'll try to pull a lambda which has a variable that is bound in t
. That's occurs with y
behind step 1. To solve that issue, whenever that happens, the bound variable y
is replaced by y0 & y1
, which are bound to each of the two copied lambdas, respectively. The problem with that is this requires us to abandon the notion of scopes, as, now, the bound variable of a λ can occur outside its own body (such as y0
and y1
behind step 2)!
Despite sounding bizarre, the language operates very well. You can represent the usual λ-encodings on it, implement recursive algorithms and it is compatible with the oracle-free fragment of the optimal reduction algorithm. Yet, some have questioned the absence of scopes. I've spent some time reasoning about this and couldn't find a way to have both things. In fact, it looks impossible. As a sanity check, I'd like to know if my reasoning makes sense.
Thus, my question is: is that possible? Can we have both incremental copying and closed scopes in a calculus?
λx. f
. $\endgroup$ – MaiaVictor Aug 28 '18 at 12:50