Start / Iowa Type Theory Commute / Lexicographic termination

Iowa Type Theory Commute

Lexicographic termination

11 min • 3 juni 2020

Many termination checkers support lexicographic (structural) recursion. The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases. Connections with nested recursion and ordinals discussed.

Senaste avsnitt

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

Krivine's Proof of FD, Using Intersection Types

A Measure-Based Proof of Finite Developments

16 april | 23 min

Introduction to the Finite Developments Theorem

27 mars | 16 min

Nominal Isabelle/HOL

31 januari | 16 min

Podcastbild

00:00 -00:00

Podcastbild

00:00 -00:00