Programming with Higher-Order Logic
Book by Dale Miller and Gopalan Nadathur
***Content in this font is a presentation note only and will be hidden in the final version***
***Content in this font is a TODO and will be hidden in the final version***
Presentation Goals:
• Introduce logic as programming via proof search and *substitution* for existentially quantified variables
• Basic idea of differences between different logic programming languages
• Examples of problems that can be solved with logic programming
• Website as artifact for future reference, possibly extended with more explanation for learning and using the languages (chelsea.lol/pwhol)
MAIN TODO LIST:
Area for conventions?
Future: unification
Future: module system?
Arrow through notes?
Talk about minimal vs intuitionistic logic?
Button to toggle visibility of presentation notes?
Page of definitions and links throughout page
Page with instructions on using lambda-prolog, linux, etc
Introduction
Objective:
Use (higher-order) typed logic to express relational specifications of computations and construct valid proofs of contextual queries
The first-order and higher-order distinction will be explored more later
We're used to defining functions to operate on data, e.g. a function for reversing lists that takes a list as input and returns the passed list reversed, but here we are seeing things relationally; a relation representing list reversal is between two lists, where one is the reverse of the other; usually the last argument represents the "output", but the whole expression is a formula
Example:
• Encode terms of type list and predicates to define reversal
• $\mathtt{reverse \; L_1 \; L_2}$ is true or false and can mean $\mathtt{L_2}$ is the reverse of $\mathtt{L_1}$
Example:
Encode and reason about other logics and languages
Approach:
Using sequent calculus, computation is goal-directed proof search, so we start with what we want to prove at the root of a proof tree
$\longrightarrow$
$\vdots$
$\dots$
$\longrightarrow$
$\vdots$
$\longrightarrow$
Contrast this view of computation with:
• Computation in functional languages as reductions to a normal form
• Computation in imperative languages as updates to state