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