Justin Lloyd's Thinkering

Today I read a published paper titled “A Higher-Order Implementation of Rewriting”

I am really trying to wrap my head around theorem provers and theorem solvers and automatic discovery of theorems. My knowledge of programming is solid but I don’t understand the science. I don’t think I will ever understand the science.

The abstract is:

Many automatic theorem-provers rely on rewriting. Using theorems as rewrite rules helps to simplify the subgoals that arise during a proof LCF is an interactive theorem-prover intended for reasoning about computation. Its implementation of rewriting is presented in detail. LCF provides a family of rewriting functions, and operators to combine them. A succession of functions is described, from pattern matching primitives to the rewriting tool that performs most inferences in LCF proofs. The design is highly modular. Each function performs a basic, specific task, such as recognizing a certain form of tautology. Each operator implements one method of building a rewriting function from simpler ones. These pieces can be put together in numerous ways, yielding a variety of rewrit- ing strategies. The approach involves programming with higher-order functions. Rewriting functions are data values, produced by computation on other rewriting functions. The code is in daily use at Cambridge, demonstrating the practical use of functional programming.

Today I read a published paper titled “The Foundation of a Generic Theorem Prover”

Taking another crack at understanding proofs and how they can be automatically (interactively) solved. Still don’t get it. I feel so fucking dumb.

The abstract is:

Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework’) in which the object-logics are formalized. Isabelle is now based on higher-order logic — a precise and well-understood foundation. Examples illustrate use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment. Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet’s higher-order unification procedure.

Today I read a published paper titled “Natural Deduction as Higher-Order Resolution”

Dense. Maybe I am not cut out to understand programming and will always be a little computer hacker and nothing more.

The abstract is:

An interactive theorem prover, Isabelle, is under development. In LCF, each inference rule is represented by one function for forwards proof and another (a tactic) for backwards proof. In Isabelle, each inference rule is represented by a Horn clause. Resolution gives both forwards and backwards proof, supporting a large class of logics. Isabelle has been used to prove theorems in. Quantifiers pose several difficulties: substitution, bound variables, Skolemization. Isabelle’s representation of logical syntax is the typed lambda-calculus, requiring higher- order unification. It may have potential for logic programming. Depth-first subgoaling along inference rules constitutes a higher-order Prolog.

Today I read a published paper titled “Proving Termination of Normalization Functions for Conditional Expressions”

I didn’t understand this at all. This knowledge is way outside of my scope of understanding and need. I mean, I “get it” but also I don’t get it. I will not be discouraged.

The abstract is:

Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure function, (2) in domain theory using LCF, (3) showing that its recursion relation, defined by the pattern of recursive calls, is well-founded. The last two proofs are essentially the same though conducted in markedly different logical frameworks. An obviously total variant of the normalize function is presented as the `computational meaning’ of those two proofs. A related function makes nested recursive calls. The three termination proofs become more complex: termination and correctness must be proved simultaneously. The recursion relation approach seems flexible enough to handle subtle termination proofs where previously domain theory seemed essential.