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.

### Like this:

Like Loading...

*Related*

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

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?

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.

(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?

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.