[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Daniel C. Wang]

So, I'm curious how much work is it to extend your lambda-calculus term 
language? How, reusable is the theory so I can build arbitrary term 
languages with binders? I'll have to admit that I suspect nominal 
approaches see very appealing right now. 

Thanks, for pointing out the errors in the statement of the theorem, 
some were just typos the other were just sloppiness on my part.

So this task really is small. I'd urge everyone to give it a try. I had 
thought about doing this using standard first-order encodings and 
approaches using higher-order syntax with the usual set of tools, and 
realized all of the tools had "challenges" for this task. In any case, I 
think more "micro-benchmarks" targeted to evaluate specific aspects of a 
system are much more constructive then "macro-benchmarks".

Micro-benchmarks should be short and clearly define what part of the 
system the micro-benchmark exercises. My claim is that the lambda-height 
challenge that I've proposed tests how easy it is to reuse and integrate 
existing theories of binding and other theories such as the natural numbers.

There are perhaps other specific areas worth constructing simple 
challenge problems for such as maintaining  a context of  facts and  
induction over open terms. I think it's worth thinking about how to 
decompose the features needed to do "real proofs"  rather than just 
trying to jump into large scale proving without a clear idea of where 
you think the challenges will be. Coming up with micro-benchmarks forces 
you to decompose the problem into a set of concrete criteria. I think 
the current poplmark challenge fails in that respect.

Michael Norrish wrote:
> I have put a HOL4 solution onto the web at
>
>   http://users.rsise.anu.edu.au/~michaeln/poplmark/wangScript.sml
>
> It uses my existing type of lambda-calculus terms.  These support
> capture-avoiding substitution, free-variables etc. 
>
> I've commented the script a little.  Adam's proof (just posted) is
> about possibly capturing substitution, so he doesn't need to worry
> about renaming variables etc.  I can get around this by deriving a BVC
> rule induction principle, but without Isabelle's automatic support for
> doing this, the length necessarily increases.
>
> Michael.
>
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>