Inside-out Procedures with Bruijn

Show & Tell
1

Hi, Racket Discourse.

I have been tinkering with the syntax of the bruijn language recently, and I thought I'd share some of the bits I've found interesting so far.

The language uses De Bruijn index-notation to name variables, which basically means that since each lambda abstraction (procedure) takes exactly one argument, one can refer to variables in terms of their respective introductory abstractions: specifically, the index indicating the number of abstractions between its use and its own abstraction.[0]

As an example, one might write something like

(lambda (x) (lambda (y) (y x))

in De Bruijn notation, as

λ λ (0 1)
| \__/ |
\______/

where we see that y := 0, because it refers to the inner-most lambda-abstraction, and x := 1 because it refers to the second, outer lambda abstraction.

bruijn is slightly different, in that it uses square brackets to indicate lambda abstractions:

 [0]  ; identity function
[[0]] ; (λ (x) (λ (y) y)) often called false
[[1]] ; (λ (x) (λ (y) x)) often called true

Although bruijn doesn't support "named" variables per se, it does have top-level definitions and let-clauses which provide static identifiers for naming (substituting) expressions.

In bruijn, you might right the well-known Y-combinator like so:

Y [[rec] [rec]] ; top-level definition
    rec 1 (0 0) ; let-clause which substitutes `rec` for `1 (0 0)`
                ; the clause is indented and on its own line

although it would be more concise to right something like

Y [[0 0] [1 (0 0)]]

I find this (former) style of "inside-out" expression to be quite pleasing.

I've written some code to try and "copy" bruijn as I learn more about it; here's an example of the Ackermann function in this form:

(define ACKERMANN #λ  ; the sigil indicating the start of De Bruijn notation
  ( Y [ [ [ rec ] ] ] ; 3 nested abstractions containing a reference to `rec`
    #:let             ; the beginning of one or more "let-clauses"
    ( rec
      IF ( ZERO? #₁ ) case-x $ IF ( ZERO? #₀ ) case-y either
      #:let                ; \__ sugar for: f $ g h -> f (g h)
      ( case-x SUCC #₀ )
      ( case-y #₂ ( PRED #₁ ) ONE )
      ( either #₂ ( PRED #₁ ) $ #₂ #₁ $ PRED #₀ )
    )                                      ; \__ sigil for zeroth De Bruijn index
  )
)
; SUCC ≈ add1
; PRED ≈ sub1


; example use
#λ( ACKERMANN TWO THREE add1 0 )
                      ; \____\__ used to convert the Church numeral to a Nat
;=> 9

Whereas the "plain" version might be:

(define ACKERMANN #λ
  [ [ [ IF ( ZERO? #₁ )
           ( SUCC #₀ )
           ( IF ( ZERO? #₀ )
                ( #₂ ( PRED #₁ ) ONE )
                ( #₂ ( PRED #₁ ) ( #₂ #₁ ( PRED #₀ ) ) )
           )
      ]
    ]
  ]
)

bruijn also supports "open terms", which is to say, De Bruijn indexes which refer to abstractions outside of their immediate context.

As far as I can tell, this owes to the way the language is compiled, similar perhaps to Oleg Kiselyov's λ to SKI, Semantically, although I am just guessing and not quite at the point where I understand enough to have an opinion.

It would be quite interesting to implement a compiler to convert these lambda-calculus terms into combinators.

I recently read Chris Okasaki's Flattening combinators: surviving without parentheses, which describes a way of evaluating expressions written in terms of the X combinator, specifically using two combinators called P for "push" and A for "apply".

(define S #λ[[[#₂ #₀ $ #₁ #₀]]])
(define K #λ[[#₁]])
(define X #λ[#₀ S [[[#₂]]]])
; K ≈ X X
; S ≈ X K

(define Stk TRUE) ; Stk ≡ Nil
(define Cmd FALSE)

(define Cons  #λ[[[[[#₀ #₄ #₃]]]]])
(define Lcase #λ[[[#₂ Stk #₁ #₀]]])

(define B #λ[#₀ Cmd A]) ; B starts a sequence, but turns out to be unnecessary
(define P #λ[[[#₀ Cmd $ Cons X #₁]]])
(define A #λ
  [ #₀ Stk
    [ Lcase #₀ 'error
      [ [ Lcase #₀ #₁
          [ [ [ #₀ Cmd $ Cons (#₂ #₄) #₁
              ]
            ]
          ]
        ]
      ]
    ]
  ]
)

(define s #λ
  ( P P A P P A A A )
) ; B P => P Cmd A ≈> P P A

(define k #λ
  ( P P A P A A )
)

#λ( S K K 3 ) ;; S K K ≈ I, or identity
#λ( s k k 3 )
;=> 3 3

Combining the algorithm from Oleg's paper with Chris' method for compiling the expressions, seems promising. The author of bruijn, Marvin Borner, seems to enjoy code-golfing and as such mentions Tromp's binary lambda-calculus a couple of times (it is used in the language's internals from what I remember).

I wonder if the P and A combinators--mapped to 0 and 1--would be suitable for golfing combinator-compilation, in the same way that Tromp's BLC seems so well-suited to the task (although the latter is isomorphic to the lambda-terms themselves, whereas the former would merely be equivalent in behaviour).

I'd love to hear the thoughts of those who know more about this.

Mooiloop.

[0] I prefer the zero-indexed version of this, because it is easier to state, in my opinion.

2 Likes