Re: [isabelle] unhelpful comment in Term.ML



> On 11 Nov 2015, at 18:43, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
>
>>
>> On 11.11.2015, at 00:25, Michael Norrish <Michael.Norrish at nicta.com.au> wrote:
>>
>> The comment is
>>
>> (*Substitute arguments for loose bound variables.
>> Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
>> Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
>>       and the appropriate call is  subst_bounds([b,a], c) .
>> Loose bound variables >=n are reduced by "n" to
>>    compensate for the disappearance of lambdas.
>> *)
>>
>> The behaviour is to substitute the first term in the list for Bound 0, the second for Bound 1, etc.  This doesn't seem to be what the second line of the comment is implying.
>
> I believe the comment is fine, or at least internally consistent. The second line does say "replacing (Bound i) with (argi)", which is what you found out too.
>
> The first half of line 2, about "beta-reduction of arg(n-1)...arg0 into t", did not immediately deliver its meaning to me, but the example "subst_bounds([b,a], c)" (with [b, a] and not [a, b]) illustrates what is meant. In your example, this means you must write
>
>    Term.subst_bounds ([ at {term "f::'a => 'b"}, @{term "x::'a"}], Bound 0 $ Bound 1)
>
> to obtain f $ x, which is consistent with the beta-reduction
>
>    (%y g. g y) x f == f x
>
> i.e. the beta-redex has x f, the list argument to "subst_bounds" has [f, x] in reverse (cf. arg(n-1)...arg0).

Right, but why does it then list the args in the order

  arg(n-1), ... arg1, arg0

?

I read that as meaning that Bound 0 gets replaced with arg0, and that arg0 is the rightmost element of the list.

If it makes sense to everyone else, I don't mind.

Michael

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.