AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug Contacts

AngouriMath

← Back to list of namespaces

Classes within the AngouriMath namespace

• Entity

  Summary

  This is the main class in AngouriMath.
  Every node, expression, or number is an Entity.
  However, you cannot create an instance of this class, look for the nested classes instead.
  

• EntityEvaluationExtension

• GreatestCommonDivisors

  Summary

  The greatest common divisor of two integers, and a fraction in lowest terms by it: the
  numerator and the denominator divided by their greatest common divisor. Both answer
  exactly what PeterO's Gcd(PeterO.Numbers.EInteger) and
  ToLowestTerms answer, and every greatest common divisor and
  reduction in the library goes through them instead.
  

  Remarks

  PeterO's greatest common divisor is fast on coprime operands and slow, without bound,
  when the divisor itself is large: on a pair of 2658 and 2249 bits sharing a factor of
  1117 bits it takes 1.5 s, where Euclid's algorithm takes 1.6 ms and the BCL's
  GreatestCommonDivisor(System.Numerics.BigInteger,System.Numerics.BigInteger) 14 µs; a shared factor of 5000 bits does
  not finish in 30 s. A sum of two fractions with a large common denominator is exactly
  such a pair, and every Rational is reduced on creation, so an
  integrand evaluated at a sample point whose fractions grew to a few thousand bits spent
  nearly all its time reducing them.
  Operands within 64 bits run Euclid's algorithm in machine words, which reduces the small
  fractions the simplifier makes in about half PeterO's time. Larger ones are converted to
  BigInteger by their two's-complement bytes, which both types read and write,
  and the BCL's Lehmer algorithm answers: faster than PeterO's at every size measured, from
  64 bits to 100,000, coprime or not, conversion included. Euclid's algorithm on
  EInteger is not an alternative: its divisions make it 500 ms on a coprime
  pair of 10,000 bits, where PeterO takes 3 ms and the BCL 0.1 ms.
  

• InternalAMExtensions

  Summary

  This is a set of extensions for internal use. You might be more interested
  in publicly exposed AngouriMathExtensions or function class MathS

• MathS

  Summary

  Use functions from this class

• ProofRecording

  Summary

  A scope that collects the steps by which the quantified statements decided inside it were
  decided, the way RewriteRecording collects rewrites: the proof of
  forall n in ZZ+ : sum(k, k, 1, n) = n (n + 1)/2 is the closed form read through
  its case, the proof of forall n in ZZ+ : sum(1/(k (k + 1)), k, 1, n) = n/(n + 1) is a base case and a step, each a step here. Nothing is collected outside a scope, and
  the ordinary path does not pay for one nobody opened. A decision already made is not
  made again: an entity whose Evaled is cached, or a statement parsed
  through the parser's cache and evaluated before, records nothing, so a proof is asked of
  a fresh entity (FromString(System.String,System.Boolean) with the cache off).
  

  Example

  using var proof = ProofRecording.Start();
  var verdict = "forall n in ZZ+ : sum(1/(k (k + 1)), k, 1, n) = n/(n + 1)".ToEntity().Evaled;
  foreach (var step in proof.Steps)
      Console.WriteLine(step);

• ProofStep

  Summary

  One step in the decision of a quantified statement: the statement that was decided, the
  rule that decided it, the verdict, and how deep it sits under the statement asked --
  the base case of an induction is one below the induction, the identity that settles the
  step one below that. The rule is named as the reference names it and as a checker
  would: Lemma is the Lean 4 tactic or lemma the step corresponds to, which
  is what an export to a proof checker needs and the design constraint of
  #746's proof engine.
  #1409