# Inside-out Procedures with Bruijn
**URL:** https://racket.discourse.group/t/inside-out-procedures-with-bruijn/4028
**Category:** Show & Tell
**Created:** [November 27, 2025, 10:06pm UTC](https://racket.discourse.group/t/inside-out-procedures-with-bruijn/4028 "2025-11-27T22:06:48Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)
#### Post date: [November 27, 2025, 10:06pm UTC](https://racket.discourse.group/t/inside-out-procedures-with-bruijn/4028/1 "2025-11-27T22:06:48Z")
Hi, Racket Discourse.
I have been tinkering with the syntax of the [`bruijn`](https://bruijn.marvinborner.de/) 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](https://en.wikipedia.org/wiki/De_Bruijn_index) 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
```scheme
(lambda (x) (lambda (y) (y x))
```
in De Bruijn notation, as
```scheme
λ λ (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:
```scheme
[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:
```scheme
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
```scheme
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](https://en.wikipedia.org/wiki/Ackermann_function) in this form:
```scheme
(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:
```scheme
(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](https://okmij.org/ftp/tagless-final/ski.pdf)_, 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](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/3E99993FE5464986AD94D292FF5EA275/S0956796802004483a.pdf/theoretical-pearls-flattening-combinators-surviving-without-parentheses.pdf)_, 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".
```scheme
(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](https://tromp.github.io/cl/Binary_lambda_calculus.html) 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.
---
### Author:  [@jasonhemann](https://racket.discourse.group/u/jasonhemann)
#### Post date: [December 5, 2025, 5:11pm UTC](https://racket.discourse.group/t/inside-out-procedures-with-bruijn/4028/2 "2025-12-05T17:11:03Z")
Howdy! I like this kinda stuff too. If you haven't seen it before, another fun thing to look at is Iota and Jot. [https://web.archive.org/web/20160823182917id\_/http://semarch.linguistics.fas.nyu.edu/barker/Iota/](https://web.archive.org/web/20160823182917id_/http://semarch.linguistics.fas.nyu.edu/barker/Iota/). I learned the word "syncategorematic" from that post.