<commit_before>---
layout: post
title: "Lexicographic Termination"
date: 2013-12-15 16:12
comments: true
external-url:
categories: termination, lexicographic ordering
author: <NAME>
published: true 
demo: LexicographicTermination.hs
---

[Previously][ref-termination] we saw how refinements can be used to prove termination
and we promised to extend our termination checker to handle "real-word" programs.

Keeping our promise, today we shall see a trick that allows liquidHaskell to prove termination on
more recursive functions, namely *lexicographic termination*.

<!-- more -->

<div class="hiddencode">
\begin{code}
module LexicographicTermination where

import Language.Haskell.Liquid.Prelude (liquidError)
\end{code}

</div>

Does Ackermann Function Terminate?<commit_msg>moving lexicographic post back<commit_after>---
layout: post
title: "Lexicographic Termination"
date: 2013-12-15 16:12
comments: true
external-url:
categories: termination, lexicographic ordering
author: <NAME>
published: true 
demo: LexicographicTermination.hs
---

[Previously][ref-termination] we saw how refinements can be used to prove termination
and we promised to extend our termination checker to handle "real-word" programs.

Keeping our promise, today we shall see a trick that allows liquidHaskell to prove termination on
more recursive functions, namely *lexicographic termination*.

<!-- more -->

<div class="hidden">

\begin{code}
module LexicographicTermination where

import Language.Haskell.Liquid.Prelude (liquidError)
\end{code}

</div>

Does Ackermann Function Terminate?
{'fraction_non_alphanumeric': 0.08778625954198473, 'fraction_numerical': 0.015267175572519083, 'mean_word_length': 5.581589958158996, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5894391', 'n_tokens_mistral': 488, 'n_tokens_neox': 438, 'n_words': 168}