OAI/Computability/QuantumFactoring/ExpressionSharing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NatExpr.sharedCost line 22

   Source documentation

   Only truncated subtraction duplicates its operands in the actual compiler. In particular a priority-search tail in an ite is compiled ONCE, not twice.

   def sharedCost : NatExpr v → ℕ
     | .var _ | .const _ => 1
     | .add a b | .mul a b | .div a b | .mod a b => a.sharedCost+b.sharedCost+1
     | .sub a b => 2*(a.sharedCost+b.sharedCost)+1
     | .iteLe a b c d => a.sharedCost+b.sharedCost+c.sharedCost+d.sharedCost+1

   Mentions: OAI.ExactQuantumFactoring.NatExpr

2. lemma OAI.ExactQuantumFactoring.NatExpr.compile_shared_count line 28
3. lemma OAI.ExactQuantumFactoring.NatExpr.template_shared_count line 66
4. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coveringPow_sharedCost line 82
5. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coveringPow_size line 88