Greatest common divisor: Difference between revisions

Here is an implementation of Stein’s algorithm, without proofs of termination or correctness.

 

(*

 

end

 

 

 

Here is an implementation of Stein’s algorithm, this time with a proof of termination. Notice that the proof is rather ‘informal’; this is practical systems programming, not an exercise in mathematical logic.

 

(*

 

end

 

 

===Euclid’s algorithm, with proof of termination and correctness===

Here is an implementation of Euclid’s algorithm, with a proof of correctness.

 

(*

 

end

 

 

===Some proofs about the gcd===

For the sake of interest, here is some use of ATS's "props"-based proof system. There is no executable code in the following.

 

 

(* Definition of the gcd by Euclid’s algorithm, using subtractions;

else

gcd_isfun__nat_nat__ (pfd, pfe)

 

=={{header|AutoHotkey}}==