A head-to-head comparison of de Bruijn indices and names

Stefan Berghofer and Christian Urban, from LFMTP 2006, available from the Nominal Isabelle research group’s website:

Often debates about pros and cons of various techniques for formalising lambda-calculi rely on subjective arguments, such as de Bruijn indices are hard to read for humans or nominal approaches come close to the style of reasoning employed in informal proofs. In this paper we will compare four formalisations based on de Bruijn indices and on names from the nominal logic work, thus providing some hard facts about the pros and cons of these two formalisation techniques. We conclude that the relative merits of the different approaches, as usual, depend on what task one has at hand and which goals one pursues with a formalisation.

5 Responses to “A head-to-head comparison of de Bruijn indices and names”

  1. 1 Samuel Gélineau October 6, 2009 at 8:41 pm

    As usual, here’s how to count variable occurrences using, this time, de Bruijn indices. It’s not that bad!

    -- first, define lambda calculus terms
    data Term (n : Nat) : Set where
      var : Fin n → Term n  -- Fin n has exactly n elements
      lam : Term (suc n) → Term n
      app : Term n → Term n → Term n
    -- next, count the variable occurrences
    countV : ∀ {n}
           → Fin n
           → Term n
           → Nat
    countV x (var y)     = if eq? x y then 1 else 0
    countV x (lam e)     = countV (suc x) e  -- increment x to
                                             -- avoid capture
    countV x (app e₁ e₂) = countV x e₁ + countV x e₂
  2. 2 Samuel Gélineau October 30, 2009 at 6:57 pm

    Come to think of it, it’s also not that bad using mere strings for variables. Perhaps counting variable occurrences isn’t best at highlighting the advantages of each solution, then… any other idea for a small yet representative benchmark?

    -- first, define lambda calculus terms
    data Term = Var String | App Term Term | Lam String Term
    -- next, count the variable occurrences
    countV :: String -> Term -> Int
    countV x (Var y)   | x == y    = 1
    countV x (Var y)   | otherwise = 0
    countV x (App u v) = countV x u
                       + countV x v
    countV x (Lam y e) | x == y    = 0
                       | otherwise = countV x e
    • 3 Name Binding Admin November 4, 2009 at 11:04 am

      I’m not sure there is a canonical piece of code you can write to highlight the advantages/disadvantages of each approach. Counting variables seems like a decent idea. I know that people working with nominal techniques often like to show off alpha-inequality, as its hard to do with HOAS, but these examples aren’t going to be general enough for a meaningful comparison.

      • 4 Samuel Gélineau November 25, 2009 at 12:13 am

        (sorry for the delay, I forgot to register to follow-up comments)

        Well, let’s think about the problem a bit longer. What is the goal of encoding variables using something more complicated than strings? There seems to be several, possibly conflicting goals. Here are those I can think of.

        – obtaining substitution for free
        – obtaining alpha-equivalence for free
        – comparing terms for equivalence
        – having distinct types for open and closed terms
        – obtaining weakening for free
        – readability
        – comparing variables for equality
        – examining and transforming expressions

        Strings make the last three easy, HOAS makes the first two easy, and the various other approaches probably make compromises.

        What’s the smallest example which would test most of the above? Counting variable occurrences only tests the last two, and POPLmark is too large. Can we find something in between?

      • 5 Samuel Gélineau November 25, 2009 at 12:45 am

        How about this: “given two terms A and B with exactly one free variable, find a closed term X, if there is one, such that the result of substituting X in A is alpha-equivalent to B.”

        The algorithm I have in mind is the following.
        1) examine A and B side to side until the free variable is found
        2) store the term in B corresponding to the variable in A
        3) if this tentative result contains any free variable, return false (since we need a closed term)
        4) substitute the tentative result for A’s free variable
        5) the result will be a closed term, weaken it
        6) compare the weakened term with B

        This short example tests open types, substitution, weakening, examining expressions, comparing variables for equality, and comparing terms for alpha-equivalence.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: