math - What does positive_to_Qpositive_i in the QArithSternBrocot library do? -


i going through code q_denumerable.v in library qarithsternbrocot , came across.

fixpoint positive_to_qpositive_i (p:positive) : qpositive :=     match p     | xi p => nr (positive_to_qpositive_i p)    | xo p => dl (positive_to_qpositive_i p)    | xh => 1    end.  

what nr , dl mean?

the library name , documentation refers stern-brocot tree, in fact encoding variant of called calkin-wilf tree. one root of tree, number 1, , constructors nr , dl indicate 2 children: if w represents p/q (with p , q coprime, i.e. rational in irreducible form) nr w represents ((p+q)/q) , dl w represents (p/(p+q)). function qpositive_i calculates (numerator, denominator) representation of qpositive value.

the function positive_to_qpositive_i calculates calkin-wilf representation of positive integer given in binary notation.


Comments

Popular posts from this blog

google chrome - Developer tools - How to inspect the elements which are added momentarily (by JQuery)? -

angularjs - Showing an empty as first option in select tag -

php - Cloud9 cloud IDE and CakePHP -