[POPLmark] Meta-comment

[Robert Harper]

Hi Dan,

Your message contains two misconceptions that are rather common, so 
forgive me for correcting them here.

First, one can perfectly well encode linear logic in LF without having 
any notion of linear function.  In fact this was one of the earliest 
"test cases" for LF that we used way back when.  The trick is to take 
advantage of the explicit representation of derivations as terms 
provided by the LF methodology, and to introduce a judgement saying 
that "this is a linear derivation".

Second, you seem to confuse the possibility of doing something (using 
higher types to represent binders) with the necessity of doing so 
(precluding the use of deBruijn indices, for example).  You can 
perfectly well use first-order representations to encode a logic in LF, 
if you so desire or are otherwise compelled to do so.  However, it 
benefits you greatly (and, experience has shown time and again, it 
benefits the encoded logic greatly) to try to take advantage of 
built-in faciltiies such as higher types.  In practice you usually do, 
and it's rarely an obstacle in and of itself.

Bob

On May 11, 2005, at 2:02 AM, Daniel C. Wang wrote:

> Robert Harper wrote
> {stuff deleted}:
>
>> Third, I can certainly envision better tools, and they are coming 
>> available as we speak, but for the moment Twelf is far and away the 
>> best thing going.  It's there, it works well, we use it daily, and it 
>> deals with the drudgery of metatheory in a way that no other tool 
>> that I know of is capable of doing.  There is no fundamental need for 
>> a radical new start, but we all agree that there are clear avenues 
>> for improving on what we have.
>
> {stuff deleted}
>
> I would like point out a design philosophy about Twelf that may make 
> reasonable people want to start from scratch. The Twelf/LF approach is 
> very nice to use because one can adopt an encoding style where the 
> object logic concepts such as binding and substitution are 
> encoded/reuse metalogic equivlents. The most of the tedium of defining 
> your object logic is factored into the metalogic.. So only LF 
> designers need worry about a whole class of problems once and users 
> reap the benefits. This of course requires users understand how to 
> reflect common notions of their object logic into the structure of the 
> Twelf metalogic. Users are of course also "stuck" if the metalogic is 
> not rich enough to reflect some of their object logic properties.  For 
> example to encode linear logics in a way the reuses the binding of the 
> Twelf/LF metalogic requires extending the notion of Twelf/LF function 
> space to include linear functions.
>
> Twelf/LF in nice because many things are "baked in". So long as those 
> things are the right things to bake in everyone is happy. However, I 
> think someone people are worried that they might want to step out of 
> the what is baked in Twelf.
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark