Beautify code

Stream: new members

[Pedro Minicz]

Any suggestions in how to make the following prettier?

@[derive decidable_eq]
inductive term : Type
| var : ℕ → term
| impl : term → term → term

open term

def {u} select {α : Type u} : list α → list (α × list α)
| (a :: as) := (a, as) :: list.map (bifunctor.snd (list.cons a)) (select as)
| [] := []

meta def ljt : list term → term → list term
| env t@(var x) := if t ∈ env then return t else do
  (impl a b, env) ← select env | alternative.failure,
  match a with
  | (var x) := do
    guard $ var x ∈ env,
    ljt (b :: env) t
  | (impl c d) := do
    ljt (impl d b :: env) (impl c d),
    ljt (b :: env) t
  end
| env t@(impl a b) := if t ∈ env then return t else ljt (a :: env) b

[Pedro Minicz]

I would like to make it more like the Haskell version:

import Control.Monad
import Data.Bifunctor

data Term
    = Var Char
    | Impl Term Term
    deriving (Eq, Show)

ljt :: [Term] -> Term -> [Term]
ljt env t
    | elem t env = return t
ljt env (Impl a b) = ljt (a : env) b
ljt env t = do
    (Impl a b, env) <- select env
    case a of
        Var a -> do
            guard $ elem (Var a) env
            ljt (b : env) t
        Impl c d -> do
            ljt (Impl d b : env) (Impl c d)
            ljt (b : env) t

select :: [a] -> [(a, [a])]
select (x:xs) = (x, xs) : map (second (x:)) (select xs)
select []     = []

[Pedro Minicz]

It particularly bothers me that if t ∈ env then return t else ... gets written twice in the Lean version.

[Pedro Minicz]

(Also, if anyone has any clue on how to convince Lean that ljt terminates, any help would be highly appreciated. I got it from here)

[Kyle Miller]

Here's a hack using optional parameters, but it's uglier in another axis:

import control.bifunctor

@[derive decidable_eq]
inductive term : Type
| var : ℕ → term
| impl : term → term → term

open term

def {u} select {α : Type u} : list α → list (α × list α)
| (a :: as) := (a, as) :: list.map (bifunctor.snd (list.cons a)) (select as)
| [] := []

meta def ljt : Π (env : list term) (t : term) (in_env : opt_param bool (t ∈ env)), list term
| env t tt := return t
| env t@(impl a b) ff := ljt (a :: env) b
| env t@(var x) ff := do
  (impl a b, env) ← select env | [],
  match a with
  | (var x) := do guard $ var x ∈ env,
                  ljt (b :: env) t
  | (impl c d) := do
    ljt (impl d b :: env) (impl c d),
    ljt (b :: env) t
  end

[Pedro Minicz]

Wow. I would have never though of that.

[Pedro Minicz]

Is opt_param used somewhere other than in tactics?

[Mario Carneiro]

It is used in structures to give default values for some arguments, e.g. lt in src#preorder

[Mario Carneiro]

Assuming you don't care about termination, you can get closer to the haskell version by just doing this:

meta def ljt : list term → term → list term
| env t := if t ∈ env then return t else
  match t with
  | impl a b := ljt (a :: env) b
  | _ := do
    (impl a b, env) ← select env | failure,
    match a with
    | (var x) := do
      guard $ var x ∈ env,
      ljt (b :: env) t
    | (impl c d) := do
      ljt (impl d b :: env) (impl c d),
      ljt (b :: env) t
    end
  end

[Pedro Minicz]

Thanks!

[Pedro Minicz]

I do care about termination. But the either versions look as far from being easy to convince Lean it terminates as it can be.

[Mario Carneiro]

I thought about it for a while and the termination condition is incredibly complex

[Mario Carneiro]

do you have an informal proof of termination?

[Bhavik Mehta]

I've got an informal proof but I think to convince lean it might take quite a bit of refactoring of ljt, (for instance knowing that the env after the select is the original one minus an element), but I think the maths here is mostly straightforward (plus some standard results about wellorderings which I don't believe are in mathlib)

[Kyle Miller]

@Pedro Minicz By the way, it doesn't seem you've translated the Prolog from the paper completely faithfully. The cut operator ! means to throw out all backtracking for the most recent choice point, and I'm not sure you can do that within the list monad.

This might be a more faithful rendition of the ljb algorithm (with no guarantees it's correct :smile:):

import control.bifunctor

@[derive decidable_eq]
inductive term : Type
| var : ℕ → term
| impl : term → term → term

open term

def {u} select {α : Type u} : list α → list (α × list α)
| (a :: as) := (a, as) :: list.map (bifunctor.snd (list.cons a)) (select as)
| [] := []

meta def ljb : list term → term → bool
| env t@(impl a b) := if t ∈ env then tt else ljb (a :: env) b
| env t@(var x) := if t ∈ env then tt else
  let imps : list (list term) := do
    (impl a b, env2) ← select env | [],
    match a with
    | (impl c d) := guard $ ljb (impl d b :: env2) a
    | _ := guard $ a ∈ env2
    end,
    return (b :: env2)
  in match imps with
     | [] := ff
     | (env2 :: _) := ljb env2 t
     end

[Pedro Minicz]

It has been a while since I've written the Haskell code, but I am pretty sure ! in the Prolog only exists for performance reasons. But again, that was a while ago, so I may be miss remembering it.

[Pedro Minicz]

Mario Carneiro said:

do you have an informal proof of termination?

Only a half-baked one.

[Pedro Minicz]

I believe the amount of impls in env + t can only get smaller or stay the same. I feel like working with finsets could make this clearer (or prove me wrong).

[Pedro Minicz]

Bhavik Mehta said:

I've got an informal proof but I think to convince lean it might take quite a bit of refactoring of ljt, (for instance knowing that the env after the select is the original one minus an element), but I think the maths here is mostly straightforward (plus some standard results about well founded relations which I don't believe are in mathlib)

I'd very interested in seeing it.

[Bhavik Mehta]

Pedro Minicz said:

Bhavik Mehta said:

I've got an informal proof but I think to convince lean it might take quite a bit of refactoring of ljt, (for instance knowing that the env after the select is the original one minus an element), but I think the maths here is mostly straightforward (plus some standard results about well founded relations which I don't believe are in mathlib)

I'd very interested in seeing it.

Working on the lean version right now :)

[Pedro Minicz]

Is finset a monad? How hard would it be turn it into one?

[Kyle Miller]

The cut operator is sometimes necessary. I don't think it's necessary here for correctness, but it seems like the run time would be horrendous without it.

[Pedro Minicz]

One of the saddest things about Haskell is that there is no (simple) Set monad.

[Kyle Miller]

The only real change I made was to wrap up some of the select and sub-ljb code into its own list monad, then truncate it.

[Kyle Miller]

Pedro Minicz said:

Is finset a monad? How hard would it be turn it into one?

I think it already is one -- at least, there's finset.bind if I remember correctly.

[Kyle Miller]

Actually, according to the docs there isn't a monad instance. But finset.bind is indeed the right bind operator.

[Pedro Minicz]

Yes, there is one! Wow, I didn't find it while looking for it yesterday. There doesn't seem to be a monad instance (although, it may not be possible since finset.bind : finset α → (α → finset β) → finset β needs [decidable_eq β]).

[Pedro Minicz]

Maybe there is some hack-y way to get do notation...

[Pedro Minicz]

A termination proof can be found here: https://www.cs.cmu.edu/~fp/courses/atp/cmuonly/D92.pdf (also https://research-repository.st-andrews.ac.uk/bitstream/handle/10023/16793/Dyckhoff_2018_contraction_free_JSL_1680.pdf)

[Bhavik Mehta]

alright I've got a working proof, minus the part which in that is referenced to [4], showing that the multiset ordering is wellfounded if the underlying partial order is

[Bhavik Mehta]

https://gist.github.com/b-mehta/ee89376db987b749bd5120a2180ce3df

[Bhavik Mehta]

it's pretty messy, I made a similar transformation to what Kyle did, but using Prop instead of bool

[Bhavik Mehta]

I don't think this version will compute at all well, but it might give you a better idea of how to prove termination

[Bhavik Mehta]

the two main points are to use the dershowitz-manna ordering, and that in the recursive steps you need to have access to the properties of the sub-formulae chosen (which match or select doesn't give you automatically)

[Mario Carneiro]

If you use Prop, it's pretty trivial to write this without a termination proof, since you can just use an inductive type

[Mario Carneiro]

it's probably clearer that way too

[Mario Carneiro]

This is a great example where it would be better to write the code first and the termination proof later

[Mario Carneiro]

it might be interesting to try applying that general recursion thing that Simon was working on (or using roption directly)

[Mario Carneiro]

yay:

import control.bifunctor control.fix

@[derive decidable_eq]
inductive term : Type
| var : ℕ → term
| impl : term → term → term

open term

def {u} select {α : Type u} : list α → list (α × list α)
| (a :: as) := (a, as) :: list.map (bifunctor.snd (list.cons a)) (select as)
| [] := []

def ljtF (ljt : list term → term → roption (list term)) :
  list term → term → roption (list term)
| env t := if t ∈ env then pure [t] else
  match t with
  | impl a b := ljt (a :: env) b
  | _ := list.join <$> (select env).mmap (λ te,
    match te with
    | (impl (var x) b, env) :=
      if var x ∈ env then
        ljt (b :: env) t
      else pure []
    | (impl (impl c d) b, env) :=
      (++) <$> ljt (impl d b :: env) (impl c d)
           <*> ljt (b :: env) t
    | _ := pure []
    end)
  end

def ljt (env : list term) (t : term) : roption (list term) :=
@roption.fix (list term × term) (λ _, list term)
  (λ IH ⟨env, t⟩, ljtF (λ env t, IH (env, t)) env t) (env, t)

[Mario Carneiro]

the monads really don't play well together though