Comments on draft-ietf-idnabis-defs-10
Andrew Sullivan
ajs at shinkuro.com
Wed Aug 26 04:17:18 CEST 2009
On Tue, Aug 25, 2009 at 06:53:02PM -0700, Paul Hoffman wrote:
> >We could go so far as to define IDNA-equivalent
> >A-labels and U-labels formally. […]
> The first part is fine (other than needing to say "remove the 'xn--'
> before decoding), but the bringing in U-label2 and A-label2 is quite
> confusing. It is not clear where they came from. I think that this
> might be trying too hard,
This is part of the formalism. When I used to do formalising
exercises for sentences as a way to pass the time, one of the rules
you usually had was "each step has exactly one well-formed-formula for
it, and then you just add them together with conjunction". So, as
apparently confusing as it might be the way I wrote it down, each step
has a separate proof: first, you prove that A1 and U1 are equivalent.
Then you prove that A2 and U2 are equivalent. Then you prove that
(A1==A2 AND U1==U2), and then you're done. But I also think this is
more gilding than lily, and I'm happy to have it left out.
A
--
Andrew Sullivan
ajs at shinkuro.com
Shinkuro, Inc.
More information about the Idna-update
mailing list