logchi / concepts Goto Github PK

Proof by Structural Induction

To prove that a proposition IH(s) is true for all structures s, prove the following:

1. IH is true on simple structures (those without substructures).
2. If IH is true on the substructures of s, then it is true on s itself.

The Smaller-Subproblem Principle

If we can reduce a problem to a smaller subproblem, we can call the procedure that solves the problem to solve the subproblem.

Follow the Grammar!

When defining a procedure that operates on inductively defined data, the structure of the program should be patterned after the structure of the data.

More precisely

• Write one procedure on each nonterminal in the grammar. The procedure will be responsible for handling the data corresponding to that nonterminal, and nothing else.
• In the procedure, write one alternative for each production corresponding to that nonterminal. You may need additional case structure, but this will get you started. For each nonterminal that appears in the right-hand side, write a recursive all to the procedure for that nonterminal.