Literature.
[1] Ján Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
[3] Ján Komara. Recursive Functions. Online.
[CL] Discrimination on the constructors of numeric terms. Example(s):
[CL] Formatting the output. Use the format to display numbers as numeric terms. Try out the following simple queries
98041654 = t:Term
3,(2,(0,1),1,2),0,3 = t:Term
[CL] Structural case analysis on numeric terms. Syntax:
Example(s):
where , , and are new variables (eigen-variables).
Structural induction on numeric terms. (bonus 1 point) Show that the principle of structural induction over numeric terms is admissible in Peano arithmetic.
Remark. Prove the claim for the special case in the following theory.
[CL] Hint. Reduce structural induction on to course of values induction with measure . Recall that the pair size function , written as |x|, is defined in the module Standard.
[CL] Structural induction on numeric terms. Syntax:
where the induction formula is formed from the current sequent.
Example(s):
where , , and are new variables (eigen-variables).
where , , and are new variables (eigen-variables).
[CL] Structural induction on numeric terms (2nd form). Syntax:
where the induction formula is formed from the current sequent.
Example(s):
where , , and are new variables (eigen-variables).
where , , and are new variables (eigen-variables).
Rearranging terms into additive normal form. (bonus 6 points) Define the function such that
Verify your implementation!
Decompilation. (bonus 1 point) Define the function such that
Verify your implementation!
Hint. Define first an auxiliary binary function such that