22
$\begingroup$

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?

|cite|improve this question
$\endgroup$
  • $\begingroup$ SKI combinators have incremental copying, are (almost) isomorphic to the lambda calculus. $\endgroup$ – augustss Aug 28 '18 at 5:49
  • $\begingroup$ To me, this looks similar to the graph-reduction algorithms for (optimal) reduction in lambda calculus. The first paper IIRC was at POPL'90 by Lamping. There, the strict notion of scope is "broken" as it happens above, and replaced with a plethora of (indexed) bracket-markers in the term graph, which is reduced using small steps as above, duplicating terms gradually. I'd recommend you have a look at it, and subsequent (simpler) graph-reduction techniques. $\endgroup$ – chi Aug 28 '18 at 8:37
  • $\begingroup$ @chi yes the reason I came up with this was to have an untyped (textual) language for Lamping's abstract algorithm. This is just a textual interpretation of that algorithm. Or do you mean he actually proposed such representation? I'm not aware of that, but would be very glad if that was the case. I'll check the paper again. $\endgroup$ – MaiaVictor Aug 28 '18 at 12:50
  • $\begingroup$ @augustss you're right, I should've clarified that I meant a language with abstractions λx. f. $\endgroup$ – MaiaVictor Aug 28 '18 at 12:50
  • $\begingroup$ I'm not terribly familiar with graph-reduction techniques for the lambda calculi. I only remember that some later variants were much simpler than Lamping's (fewer brackets/special tokens around). Perhaps there's some way to represent those "bracket" rules in a term form? I vaguely recall a presentation stating that those rules could not be used on terms -- they really need graphs --, but I am unsure. $\endgroup$ – chi Aug 28 '18 at 15:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.