Re: [isabelle] unhelpful comment in Term.ML



> 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).

Jasmin





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