Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm

In this article we formalize in Mizar [1], [2] the maximum number of steps taken by some number theoretical algorithms, “right–to–left binary algorithm” for modular exponentiation and “Euclidean algorithm” [5]. For any natural numbers a, b, n, “right–to–left binary algorithm” can calculate the natur...

Full description

Bibliographic Details
Main Authors: Okazaki Hiroyuki, Nagao Koh-ichi, Futa Yuichi
Format: Article
Language:English
Published: Sciendo 2019-04-01
Series:Formalized Mathematics
Subjects:
Online Access:https://doi.org/10.2478/forma-2019-0009
id doaj-b8a2fd7a85f240f0855c2e9c16c19d67
record_format Article
spelling doaj-b8a2fd7a85f240f0855c2e9c16c19d672021-09-05T21:01:04ZengSciendoFormalized Mathematics1426-26301898-99342019-04-01271879110.2478/forma-2019-0009Maximum Number of Steps Taken by Modular Exponentiation and Euclidean AlgorithmOkazaki Hiroyuki0Nagao Koh-ichi1Futa Yuichi2Shinshu University, Nagano, JapanKanto Gakuin University, Kanagawa, JapanTokyo University of Technology, Tokyo, JapanIn this article we formalize in Mizar [1], [2] the maximum number of steps taken by some number theoretical algorithms, “right–to–left binary algorithm” for modular exponentiation and “Euclidean algorithm” [5]. For any natural numbers a, b, n, “right–to–left binary algorithm” can calculate the natural number, see (Def. 2), AlgoBPow(a, n, m) := ab mod n and for any integers a, b, “Euclidean algorithm” can calculate the non negative integer gcd(a, b). We have not formalized computational complexity of algorithms yet, though we had already formalize the “Euclidean algorithm” in [7].https://doi.org/10.2478/forma-2019-0009algorithmspower residueseuclidean algorithm68w4011a0511a1503b35
collection DOAJ
language English
format Article
sources DOAJ
author Okazaki Hiroyuki
Nagao Koh-ichi
Futa Yuichi
spellingShingle Okazaki Hiroyuki
Nagao Koh-ichi
Futa Yuichi
Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
Formalized Mathematics
algorithms
power residues
euclidean algorithm
68w40
11a05
11a15
03b35
author_facet Okazaki Hiroyuki
Nagao Koh-ichi
Futa Yuichi
author_sort Okazaki Hiroyuki
title Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
title_short Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
title_full Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
title_fullStr Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
title_full_unstemmed Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
title_sort maximum number of steps taken by modular exponentiation and euclidean algorithm
publisher Sciendo
series Formalized Mathematics
issn 1426-2630
1898-9934
publishDate 2019-04-01
description In this article we formalize in Mizar [1], [2] the maximum number of steps taken by some number theoretical algorithms, “right–to–left binary algorithm” for modular exponentiation and “Euclidean algorithm” [5]. For any natural numbers a, b, n, “right–to–left binary algorithm” can calculate the natural number, see (Def. 2), AlgoBPow(a, n, m) := ab mod n and for any integers a, b, “Euclidean algorithm” can calculate the non negative integer gcd(a, b). We have not formalized computational complexity of algorithms yet, though we had already formalize the “Euclidean algorithm” in [7].
topic algorithms
power residues
euclidean algorithm
68w40
11a05
11a15
03b35
url https://doi.org/10.2478/forma-2019-0009
work_keys_str_mv AT okazakihiroyuki maximumnumberofstepstakenbymodularexponentiationandeuclideanalgorithm
AT nagaokohichi maximumnumberofstepstakenbymodularexponentiationandeuclideanalgorithm
AT futayuichi maximumnumberofstepstakenbymodularexponentiationandeuclideanalgorithm
_version_ 1717781754077511680