Rosetta Code

Greatest common divisor: Difference between revisions

Page Discussion

Greatest common divisor (view source)

Revision as of 14:25, 19 February 2022

147 bytes added ,  2 years ago
→‎{{header|ATS}}
Line 593:
{{works with|ATS|Postiats 0.4.1}}
 
==Stein’s algorithm (without proofs)==
You can compile with as simple a command as ‘patscc -o gcd gcd.dats’, although
ATS code really likes to have you turn on the C compiler’s optimizations.
For example, ‘patscc -O3 -march=native -o gcd gcd.dats’
 
<lang ats>(********************************************************************)
(*
Line 603 ⟶ 600:
https://en.wikipedia.org/w/index.php?title=Binary_GCD_algorithm&oldid=1072393147
 
This is an implementation without proofproofs of correctness, althoughanything.
I do also show some proofs about the gcd.
 
The implementations shown here require the GCC builtin functions
Line 610 ⟶ 606:
that supports those functions, you are fine. Otherwise, one could
easily substitute other C code.
 
Compile with ‘patscc -o gcd gcd.dats’.
 
*)
Line 621 ⟶ 619:
(********************************************************************)
(* *)
(* ForDeclarations of the sakefunctions. of interest, here is a tiny bit of proof work *)
(* about the gcd. *)
(* *)
 
(* Definition of the gcd by Euclid’s algorithm, using subtractions;
gcd(0,0) is defined to equal zero. (I do not prove that this
definition is equivalent to ‘greatest common divisor’; that’s not a
sort of thing ATS is good at.) *)
dataprop GCD (int, int, int) =
| GCD_0_0 (0, 0, 0)
| {u : pos}
GCD_u_0 (u, 0, u)
| {v : pos}
GCD_0_v (0, v, v)
| {u, v : pos | u <= v}
{d : pos}
GCD_u_le_v (u, v, d) of
GCD (u, v - u, d)
| {u, v : pos | u > v}
{d : pos}
GCD_u_gt_v (u, v, d) of
GCD (u - v, v, d)
| {u, v : int | u < 0 || v < 0}
{d : pos}
GCD_u_or_v_neg (u, v, d) of
GCD (abs u, abs v, d)
 
(* Here is a proof, by construction, that the gcd of 12 and 8 is 4. *)
prfn
gcd_12_8 () :<prf>
GCD (12, 8, 4) =
let
prval pf = GCD_u_0 {4} ()
prval pf = GCD_u_le_v {4, 4} {4} (pf)
prval pf = GCD_u_le_v {4, 8} {4} (pf)
prval pf = GCD_u_gt_v {12, 8} {4} (pf)
in
pf
end
 
(* A lemma: the gcd is total. That is, it is defined for all
integers. *)
extern prfun
gcd_istot :
{u, v : int}
() -<prf>
[d : int]
GCD (u, v, d)
 
(* Another lemma: the gcd is a function: it has a unique value for
any given pair of arguments. *)
extern prfun
gcd_isfun :
{u, v : int}
{d, e : int}
(GCD (u, v, d),
GCD (u, v, e)) -<prf>
[d == e] void
 
(* Proof of gcd_istot. This source file cannot be compiled unless the
proof is valid. *)
primplement
gcd_istot {u, v} () =
let
prfun
gcd_istot__nat_nat__ {u, v : nat | u != 0 || v != 0} .<u + v>.
() :<prf> [d : pos] GCD (u, v, d) =
sif v == 0 then
GCD_u_0 ()
else sif u == 0 then
GCD_0_v ()
else sif u <= v then
GCD_u_le_v (gcd_istot__nat_nat__ {u, v - u} ())
else
GCD_u_gt_v (gcd_istot__nat_nat__ {u - v, v} ())
 
prfun
gcd_istot__int_int__ {u, v : int | u != 0 || v != 0} .<>.
() :<prf> [d : pos] GCD (u, v, d) =
sif u < 0 || v < 0 then
GCD_u_or_v_neg (gcd_istot__nat_nat__ {abs u, abs v} ())
else
gcd_istot__nat_nat__ {u, v} ()
in
sif u == 0 && v == 0 then
GCD_0_0 ()
else
gcd_istot__int_int__ {u, v} ()
end
 
(* Proof of gcd_isfun. This source file cannot be compiled unless the
proof is valid. *)
primplement
gcd_isfun {u, v} {d, e} (pfd, pfe) =
let
prfun
gcd_isfun__nat_nat__ {u, v : nat}
{d, e : int}
.<u + v>.
(pfd : GCD (u, v, d),
pfe : GCD (u, v, e)) :<prf> [d == e] void =
case+ pfd of
| GCD_0_0 () =>
{
prval GCD_0_0 () = pfe
}
| GCD_u_0 () =>
{
prval GCD_u_0 () = pfe
}
| GCD_0_v () =>
{
prval GCD_0_v () = pfe
}
| GCD_u_le_v pfd1 =>
{
prval GCD_u_le_v pfe1 = pfe
prval _ = gcd_isfun__nat_nat__ (pfd1, pfe1)
}
| GCD_u_gt_v pfd1 =>
{
prval GCD_u_gt_v pfe1 = pfe
prval _ = gcd_isfun__nat_nat__ (pfd1, pfe1)
}
in
sif u < 0 || v < 0 then
{
prval GCD_u_or_v_neg pfd1 = pfd
prval GCD_u_or_v_neg pfe1 = pfe
prval _ = gcd_isfun__nat_nat__ (pfd1, pfe1)
}
else
gcd_isfun__nat_nat__ (pfd, pfe)
end
 
(********************************************************************)
(* *)
(* Now declarations of the actual, executable functions. *)
(* *)
 
Line 843 ⟶ 704:
 
(* Looping is done by tail recursion. There is no proof
the function terminates; this fact is indicated by ‘<!ntm>’. *)
‘<!ntm>’. *)
fun {tk : tkind}
main_loop (xx_odd : t, y : t) :<!ntm> t =
let
(* Remove twos from y, giving an odd number y1. *)
val y1 = Note gcd(yx_odd,y_odd) >> nonneg= gcd(ctz x_odd,y). *)
val y_odd = (y >> nonneg (ctz y))
in
if xx_odd = y1y_odd then
xx_odd
else
let
(* SwapIf xy_odd and y1 if< necessary,x_odd renamingthen themswap px_odd and qy_odd.
PerhapsThis the Coperation compilerdoes cannot convertaffect the computationgcd. of*)
val x_odd = pmin and(x_odd, q to branchless instructions. Notice that they_odd)
and y_odd = ATSmax compiler needed a hint that the values of p and(x_odd, qy_odd)
were of type t. *)
val p = (if x < y1 then x else y1) : t
val q = (if x < y1 then y1 else x)
in
main_loop (px_odd, qy_odd - px_odd)
end
end
Line 876 ⟶ 736:
val y = (v >> nonneg n)
 
(* Remove twos from x, giving an odd number. *)
Note gcd(x_odd,y) = gcd(x,y). *)
val x_odd = (x >> nonneg (ctz x))
 
Line 885 ⟶ 746:
val z = $effmask_ntm (main_loop (x_odd, y))
in
(* Put the common factors of two back in. *)
(z << nonneg n)
end
 
(* If v < u then swap u and v. This operation does not
affect the gcd. *)
val u = min (u, v)
and v = max (u, v)
in
if iseqz u then
v
else if iseqz v then
u
else if u = v then
u
else
u_and_v_both_positive (u, v)
Line 924 ⟶ 787:
assertloc (gcd (~10, 0) = gcd (0U, 10U));
assertloc (gcd (~6L, ~9L) = 3UL);
assertloc (gcd (40902LL, ~24140LL) = 34ULL);
assertloc (gcd (40902LL, ~24140LL) = 34ULL);
assertloc (gcd (~40902LL, 24140LL) = 34ULL);
assertloc (gcd (~40902LL, ~24140LL) = 34ULL);
assertloc (gcd (24140LL, 40902LL) = 34ULL);
assertloc (gcd (~24140LL, 40902LL) = 34ULL);
assertloc (gcd (24140LL, ~40902LL) = 34ULL);
assertloc (gcd (~24140LL, ~40902LL) = 34ULL)
end
 
(********************************************************************)</lang>
 
==Proving theorems about the gcd==
 
For the sake of interest, here is some use of ATS’s proof system. There is no executable code in the following.
 
<lang ats>(* Typecheck this file with ‘patscc -tcats gcd-proofs.dats’. *)
 
(* Definition of the gcd by Euclid’s algorithm, using subtractions;
gcd(0,0) is defined to equal zero. (I do not prove that this
definition is equivalent to the common meaning of ‘greatest common
divisor’; that’s not a sort of thing ATS is good at.) *)
dataprop GCD (int, int, int) =
| GCD_0_0 (0, 0, 0)
| {u : pos}
GCD_u_0 (u, 0, u)
| {v : pos}
GCD_0_v (0, v, v)
| {u, v : pos | u <= v}
{d : pos}
GCD_u_le_v (u, v, d) of
GCD (u, v - u, d)
| {u, v : pos | u > v}
{d : pos}
GCD_u_gt_v (u, v, d) of
GCD (u - v, v, d)
| {u, v : int | u < 0 || v < 0}
{d : pos}
GCD_u_or_v_neg (u, v, d) of
GCD (abs u, abs v, d)
 
(* Here is a proof, by construction, of the proposition
‘The gcd of 12 and 8 is 4’. *)
prfn
gcd_12_8 () :<prf>
GCD (12, 8, 4) =
let
prval pf = GCD_u_0 {4} ()
prval pf = GCD_u_le_v {4, 4} {4} (pf)
prval pf = GCD_u_le_v {4, 8} {4} (pf)
prval pf = GCD_u_gt_v {12, 8} {4} (pf)
in
pf
end
 
(* A lemma: the gcd is total. That is, it is defined for all
integers. *)
extern prfun
gcd_istot :
{u, v : int}
() -<prf>
[d : int]
GCD (u, v, d)
 
(* Another lemma: the gcd is a function: it has a unique value for
any given pair of arguments. *)
extern prfun
gcd_isfun :
{u, v : int}
{d, e : int}
(GCD (u, v, d),
GCD (u, v, e)) -<prf>
[d == e] void
 
(* Proof of gcd_istot. This source file will not pass typechecking
unless the proof is valid. *)
primplement
gcd_istot {u, v} () =
let
prfun
gcd_istot__nat_nat__ {u, v : nat | u != 0 || v != 0} .<u + v>.
() :<prf> [d : pos] GCD (u, v, d) =
sif v == 0 then
GCD_u_0 ()
else sif u == 0 then
GCD_0_v ()
else sif u <= v then
GCD_u_le_v (gcd_istot__nat_nat__ {u, v - u} ())
else
GCD_u_gt_v (gcd_istot__nat_nat__ {u - v, v} ())
 
prfun
gcd_istot__int_int__ {u, v : int | u != 0 || v != 0} .<>.
() :<prf> [d : pos] GCD (u, v, d) =
sif u < 0 || v < 0 then
GCD_u_or_v_neg (gcd_istot__nat_nat__ {abs u, abs v} ())
else
gcd_istot__nat_nat__ {u, v} ()
in
sif u == 0 && v == 0 then
GCD_0_0 ()
else
gcd_istot__int_int__ {u, v} ()
end
 
(* Proof of gcd_isfun. This source file will not pass typechecking
unless the proof is valid. *)
primplement
gcd_isfun {u, v} {d, e} (pfd, pfe) =
let
prfun
gcd_isfun__nat_nat__ {u, v : nat}
{d, e : int}
.<u + v>.
(pfd : GCD (u, v, d),
pfe : GCD (u, v, e)) :<prf> [d == e] void =
case+ pfd of
| GCD_0_0 () =>
{
prval GCD_0_0 () = pfe
}
| GCD_u_0 () =>
{
prval GCD_u_0 () = pfe
}
| GCD_0_v () =>
{
prval GCD_0_v () = pfe
}
| GCD_u_le_v pfd1 =>
{
prval GCD_u_le_v pfe1 = pfe
prval _ = gcd_isfun__nat_nat__ (pfd1, pfe1)
}
| GCD_u_gt_v pfd1 =>
{
prval GCD_u_gt_v pfe1 = pfe
prval _ = gcd_isfun__nat_nat__ (pfd1, pfe1)
}
in
sif u < 0 || v < 0 then
{
prval GCD_u_or_v_neg pfd1 = pfd
prval GCD_u_or_v_neg pfe1 = pfe
prval _ = gcd_isfun__nat_nat__ (pfd1, pfe1)
}
else
gcd_isfun__nat_nat__ (pfd, pfe)
end</lang>
 
=={{header|AutoHotkey}}==
Chemoelectric
1,448

edits

Retrieved from "https://rosettacode.org/wiki/Special:MobileDiff/51905"