*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] unhelpful comment in Term.ML*From*: Michael Norrish <Michael.Norrish at nicta.com.au>*Date*: Wed, 11 Nov 2015 08:57:30 +0000*Accept-language*: en-US, en-AU*In-reply-to*: <282EAE1C-93ED-4878-BFCC-619642F3D699@inria.fr>*References*: <DC2FC414-829D-4A26-B17E-3C68C6E694E8@nicta.com.au> <282EAE1C-93ED-4878-BFCC-619642F3D699@inria.fr>*Thread-index*: AQHRHA8kzZo7Z3S2BE+a2vSXLhFrAZ6VuNcAgAAUoQA=*Thread-topic*: [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.

**Follow-Ups**:**Re: [isabelle] unhelpful comment in Term.ML***From:*Jasmin Blanchette

**References**:**[isabelle] unhelpful comment in Term.ML***From:*Michael Norrish

**Re: [isabelle] unhelpful comment in Term.ML***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] unhelpful comment in Term.ML
- Next by Date: Re: [isabelle] unhelpful comment in Term.ML
- Previous by Thread: Re: [isabelle] unhelpful comment in Term.ML
- Next by Thread: Re: [isabelle] unhelpful comment in Term.ML
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list