LSTS: Term Type Pattern Matching

Quantified Statements are Higher-Order Abstractions for Logic Programming

In LSTS forall statements have been upgraded to become sensitive to both Term and Type contexts. A quantified statement must be proven locally. However, after the initial local proof, that statement can be applied anywhere with a simple hint to the compiler. In the following code, a forall is used to prove that incrementing an even number results in an odd number.

forall @inc_even x:Even. Odd = x + 1;
(6: Even) + 1 @inc_even : Odd

Statements are sensitive to both Term and Type level patterns

One of the really cool things about this new feature is that the patterns naturally destructure Terms while still remaining sensitive to the Type of each element of the Term. The hints also fit nicely into the Term language and can be daisy chained to prove non-trivial results in O(1) time. Time Complexity can be a non-starter for certain proof strategies, and for this feature we have made sure that there is very little friction to adopt this amazing new feature.

Dependent Types are Dynamic Types at the Type Level

The second feature interaction that I would like to highlight here is that between Quantified Statements and Dependent Types. Dependent Types have their own Term language and evaluate at the Type level dynamically. This allows for near arbitrary computation to take place throughout Type Reduction. Quantified Statements can then use this for induction or other computation heavy proof methods.

Selfie

Andrew Johnson

Open Source:

Other Platforms

Published Books:

Books that I am reading:

Top Referrers:

  1. Google Search
  2. DuckDuckGo Search
  3. Sogou Search
  4. Bing Search
  5. Baidu Search

Tools:

Weblog: