PL-Project: Asymptotic Complexity

The project for programming language course. The main goal of the project is to introduce the concept of asymptotic complexity into the proof system defined by Hoare Logic and based on Denotational Semantics.

First three sections are almost the same as the ones in proposal and mid-term check, you may skip to the last section to see proof outlines.

We failed to update lines for each definition and theorems and to include some new definitions and theorems here, due to limited time. We are very sorry for that.

Project Goals

• Define polynomial to support operations and simplifications in asymptotic bounds.
• Define various asymptotic bounds and asymptotic notations in coq.
• Update denotational semantics to include time step (done in class) and to fit our project.
• Adapt Hoare logic to include the proof system for asymptotic complexity.
  • Hoare Skip
  • Hoare Assignment
  • Hoare Sequence BigTheta
  • Hoare Sequence BigO
  • Hoare Sequence BigOmega
  • Hoare If Same
  • Hoare Loosen (New Rule)
  • Hoare While Linear
  • Hoare While General
• Prove the soundness of Hoare logic, both the basic Hoare logic and the proof system for asymptotic complexity.
  • Hoare Skip
  • Hoare Assignment
  • Hoare Sequence BigTheta
  • Hoare Sequence BigO
  • Hoare Sequence BigOmega
  • Hoare If Same
  • Hoare Loosen (New Rule)
  • Hoare While Linear
  • Hoare While General
• Prove the correctness and asymptotic complexity for some simple algorithms encountered in class using what we will build.
  • Simple While
  • Slow Addition
  • Min While

Constraints

There are several constraints that might limit what we can do or simplify what we want to do.

• We do not consider programs with control statements, i.e. break and continue. Moreover, we do not wish to alter the potential path of program execution in similar ways, which makes the execution time almost independent with the distribution of input data. This cause us unable to verify the asymptotic complexity of algorithms like Quick Sort, but will simplify our definition of what is Asymptotic Complexity.
• We will use the the toy language developed in class or the adapted version of it, which only contains very fundamental operations and statements. This will limit the scope of programs and algorithms we can take into consideration.

---

Project Overview

Our project has following files:

• Imp8.v: basic library of the toy language, from the course.
• PolyAB.v: defines polynomial and its operation, and asymptotic bounds defined on polynomials, and mathematic lemmas used later.
• Denotation.v: the denational semantics with steps, mainly from the course but modified.
• HoareLogic.v: the hoare logic with asymptotic bound, should contain rules and provable definition
• Soundness.v: the proof for the soundness of hoare logic
• Demos.v: examples of programs proved (or to be proved) using our hoare logic
• AsymptoticBound.v: pure mathematic asymptotic bound definition attempts (abandonded)

Compilation Order

Please compile the project in the following order:

• Imp8.v -> PolyAB.v -> Denotation.v -> HoareLogic.v -> Soundness.v -> Demos.v

Definitions

Polynomial (in PolyAB.v)

• poly (at line 11)
  • A list of Z, each represents a coefficient at certain term.
  • The power increases as the index goes up.
• poly_eval (at line 21)
  • A recursive function that evaluates a poly into functions that maps Z to Z based on the semantics.
• TPower: (at line 31)
  • An auxiliary recursive function that implements the power operation for logical_var.
• poly_eval_lv (at line 37)
  • A recursive function that evaluates a poly into functions that maps logical_var to term based on the semantics.
  • Might be used in defining recursive equations in Hoare While General Rule.
• poly_add (p1 +++ p2) (at line 48)
  • A recursive function that adds two polys into one poly.
• trim_0 (at line 56)
  • A recursive function that removes 0s at tail, i.e. in the highest order terms.
  • Used in determining the valid highest order term.
• poly_scalar_mult (k ** p) (at line 65)
  • A recursive function that multiplies a Z scalar to a poly to get a new poly.
• poly_mult (p1 *** p2) (at line 71)
  • A recursive function that multiplies two polys to get a new poly.

Polynomial Asymptotic Bound (in PolyAB.v)

• AsymptoticBound (at line 321)
  • An inductive type that specifies different asymptotic bounds.
• ab_eval (at line 326)
  • A function that takes Lassn, AsymptoticBound, and other Z parameters to formalize the asymptotic property defined by the asymptotic bound in Porp.
• loosen (T1 =< T2) (at line 338)
  • An inductive relation that specifies the loosening relationship between two bounds.
  • The first AB (T1) can be relaxed to the second AB (T2).
  • We did not prove the correctness in this file, but in the soundness proof of the Hoare Logic.

Command Denotation With Steps (in Denotation.v)

• skip_sem (at line 8)
  • Almost the same as the one in class, but we specify the time step for Skip to be 1.
• asgn_sem (at line 14)
  • Almost the same as the one in class, but we move the time step property outside.
• seq_sem (at line 20)
  • The same as the one in class.
• if_sem (at line 27)
  • Almost the same as the one in class, but we move the time step property outside.
• loop_sem (at line 53)
  • Almost the same as the one in class, but we move the time step property outside.
• ceval (at line 59)
  • The same as the one in class.

Hoare Logic (in HoareLogic.v)

• hoare_triple ({{ P }} c {{ Q }} $ T) (at line 11)
  • An inductive type that specifies the hoare triple.
  • Almost the same as the one in class, but with extra asymptotic bound added.
• provable (|-- tr) (at line 17)
  • An inductive relation that specifies the Hoare Logic.

Soundness (in Soundness.v)

• valid (|== tr) (at line 13)
  • A function that maps hoare_triple to Prop which specifies the validity of Hoare Rules.

Important Theorems

Polynomial (in PolyAB.v)

There are many properties about poly we have proven to support later use of it, but the following 4 theorems are the most important ones.

• poly_add_spec (at line 170)
  • Stating that the evaluation of poly_add result is correct.
• poly_scalar_mult_spec (at line 182)
  • Stating that the evaluation of poly_scalar_mult result is correct.
• poly_mult_spec (at line 191)
  • Stating that the evaluation of poly_mult result is correct.
• trim_invar (at line 205)
  • Stating that after trimming redundant 0s, the evaluation is the same as before.

Denotation (in Denotation.v)

• command_cost_time (at line 68)
  • Stating that any command would cost at least 1 time step.
  • Apply to the denotational semantics, where Skip also cost 1 time step.
  • This property is important in proving the hoare_if_same_soundness, because previously having Skip inside if statement would invalidate that rule, since unfolding if also takes time.
• Expanding If and While does not cost time
  • Instead of specify that all command cost at least 1 time step, we specify that expanding If and While statements does not cost time, because analysis of time complexity of algorithms barely counts time spent on unrolling those two statements.

Soundness (in Soundness.v)

All the Hoare Rules contain the part we have declared in class, thus we will not mention those again.

• hoare_skip_sound (at line 27)
  • Stating that Skip has Constant time complexity.
• hoare_asgn_bwd_sound (at line 68)
  • Stating that Assignment has Constant time complexity.
• hoare_seq_bigtheta_sound (at line 96)
  • Stating that the time complexity of Sequenced Command is the sum of time complexity for separate commands in the sense of Big Theta.
• hoare_if_same_sound (at line 166)
  • Stating that the time complexity of If Command is the same as those of its branches, if the time complexity of branch commands are the same.
• hoare_loosen_sound (at line 307)
  • Stating that we can relax the time complexity of certain command based on the loosen relation.
  • Auxiliary properties about poly is required to prove the loosening rule for asymptotic bounds that have the same highest order.
• hoare_while_linear_sound (at line 354)
  • Stating that if the loop variant decrease linearly, by multiplying a linear term onto the asymptotic bound for the inner command, we get the time complexity for the whole loop.
  • There are other conditions to be satisfied:
    1. (forall st La, ((st, La) |== (P AND {[b]})) -> ((st, La) |== (0 < V))): Loop invariant and the trueness of loop condition imply the status of loop variant.
    2. assn_occur n P = O /\ term_occur n V = O /\ bexp_occur n b = O: The logical variable bound to loop variant does not occur in other parts of the pre-condition.
    3. (forall x, 0 < x -> 0 <= poly_eval p x): The time cost is non-negative when input size is positive.
    4. (forall x y, x <= y -> poly_eval p x <= poly_eval p y): The time cost increases as input size increase.
• hoare_consequence_sound (at line x)
  • Stating that consequence rule holds for the Hoare logic, if time complexity stays unchanged.
• hoare_logic_sound (at line 361)
  • Stating that if a Hoare Triple is provable, then it is valid.

Demos (in Demos.v)

• simple_loop_correct (at line 79)
  • This is a simple example to test the usage of Hoare rule for while loop, which slowly decreases X to 0.
• slow_addition_correct (at line 130)
  • This example comes from the Exercise 2 of Task 2 in Assignment 2.
  • We want to prove that its time complexity is $O(m)$.
  • Due to the requirement in while rule, extra conditions are required for the logical_var bound to the loop variant.
• min_while_correct (at line 33) We did not have time to prove this.
  • This example comes from the Exercise 3 of Task 4 in Assignment 2.
  • We want to prove that its time complexity is $O(\min(a, b))$.
  • Since we try to prove something that is not a polynomial, a minimum function, using polynomial asymptotic bound, we might get stuck and might change this to something simpler.

---

Proof Ideas & Brief Informal Proofs

hoare_skip_sound

• Simple proof, no detailed informal proof is required.

hoare_asgn_bwd_sound

• Simple proof, no detailed informal proof is required.

hoare_seq_bigtheta_sound

• Construct Coefficient: The coefficient for the lower bound is the minimum of original lower bound coefficient. The coefficient for the upper bound is the maximum of original upper bound coefficient.
• Main Proof Idea for Time Complexity: Move the multiplier, i.e. the results of polynomial evaluations, inside the min and max, and by the upper and lower bounds of each term in the given condition, we can get the total of upper and lower bounds. By relaxing the minimum and maximum to one of the operands, we can proof the inequality.

hoare_if_same_sound

• Construct Coefficient: Again, the coefficient for the lower bound is the minimum of original lower bound coefficient. The coefficient for the upper bound is the maximum of original upper bound coefficient.
• Main Proof Idea for Time Complexity: Taking BigTheta case in IF branch for example:
  • 
    
  • 
    
  • The proof for ELSE branch is almost the same as the IF branch, but we will use $a1'$ and $a2'$ to relax minimum and maximum, because they are the ones specified by the command in the ELSE branch.

hoare_loosen_sound

• Main proof outline is to induct over loosen relation, and prove goals for each loosen rule.
• Since other loosen rules are relatively simple, we only briefly illustrate the proof idea behind O_Poly2Mono rule.
• In fact, one hoare_loosen rule contains a family of rules. It is exhausting to write out the informal ideas of all those rules after we proved them in Coq. You may simply look into our code to go through proofs for other simple rules.
• The main idea for the proof of this loosen rule is as follows:

Lemmas for hoare_while_linear_sound

• There are 3 lemmas for the proof of hoare_while_linear_sound. They states that if a logical variable does not occur in A, then update its value in logical assignment does not effect the meaning of A.
• The proofs are simply apply induction or mutual induction over the structure of A.

hoare_while_linear_sound

• Construct Coefficient: We reuse the coefficients from the loop body to be those of the entire loop.
• Main Proof Idea for Time Complexity: The main idea of the proof for time complexity is as follows:
• Brief Informal Proof

  First, we do induction over the loop time n'.
  
  1) If n' = 0, 
      the program does not enter the loop, thus the time cost is 0.
      By the non-negativity or the sign preserving property (3) of the polynomial p, the inequality holds.
  
  2) If n' > 0,
      Use the thoughts in (*) to prove the goal.
  
      Since the loop has carried out once,
      by the derivation from loop invariant and loop condition to status of loop variant (1) is,
      the input size should be at least 1 (**).
  
      Then we need to discuss the input size case by case.
          Because if n = 1, there is no second round of the loop,
          and we can not relax any time cost term except the one of the first round since we know nothing about other rounds.
      
      a) If n <> 1,
          combined with the status of loop variant (**) we derived before,
          we have n > 1.
          By increasingness of the bound,
          we can relax the time cost based on (*) and prove the goal.
      
      b) If n = 1,
          the time cost for later rounds, t2, is exactly 0.
          T = t1 + 0 <= a2 * P(1) <= a2 * 1 * P(1) = a2 * n * P(n)
  
          We still need to discuss loop time n' to get some properties.
          i) If n' = 0,
              no more loop is carried out,
              thus we can prove the goal.
          ii) If n' > 0,
              by the derivation from loop invariant and loop condition to status of loop variant (1),
              this case is impossible, since there is no more loop rounds.
  

hoare_consequence_sound

• Simple proof, no detailed informal proof is required.

hoare_logic_sound

• The soundness of hoare logic with time complexity is proved by induction over the structure of c, with supports of previous lemmas.

simple_loop_correct

• Simple proof, no detailed informal proof is required.

slow_addition_correct

• Note that this is different from the one in mid-term submission.
• The main proof steps are illustrated by the usages of our Hoare Rules.
  • Use hoare_consequence to adjust the pre-condition and post-condition to fit the form of hoare_while_linear.
  • Use hoare_loosen twice to adjust the time complexity to fit the form of hoare_while_linear.
  • Use hoare_while_linear to expand the while loop. Ltac forward_while_linear (line 30 in Demos.v) is defined to use hoare_while_linear easily.
  • Prove other conditions required by hoare_while_linear.
  • Use hoare_loosen twice to adjust the time complexity to fit the form of hoare_seq_bigtheta.
  • Use hoare_seq_bigtheta twice to fully expand sequenced command.
  • Use hoare_asgn_bwd on the third and second assignment command.
  • Use hoare_consequence to create room of flexibility for using hoare_asgn_bwd on the first assignment command.
  • Use hoare_asgn_bwd on the first assignment command.
  • Prove the derivation from the original pre-condition to the one generated by hoare_asgn_bwd.