Self-referential let

Stream: new members

[Serena]

Is there a way to do a self-referential let? I want to write this code, but it is complaining that arr is not defined inside the anonymous function.

let arr := Array.ofFn
    fun (n' : Fin (n + 1)) =>
      Thunk.mk fun _ => match n' with
      | 0 => some []
      | n' => shortest? <| coins.filterMap
        fun (c : PNat) =>
          if let some changeThunk := arr[n' - c.val]? >>= Thunk.get then
            some <| c :: changeThunk
          else none

[Eric Wieser]

let rec?

[Serena]

Eric Wieser said:

let rec?

If this is wrong please correct me -- I thought that let rec would create recursive definitions, in this case I only want 1 definition (self-referential), not recursive? Setting let rec gives an error because it can't show that it terminates.

[Aaron Liu]

what do you mean "self-referential"

[Aaron Liu]

I think I see what you want to do here

[Aaron Liu]

I'm not sure about all those thunks though

[Anthony Wang]

(deleted)

[Eric Wieser]

Can you make this a #mwe?

[Aaron Liu]

oh it's not possible to prove it terminates because it doesn't terminate

[Aaron Liu]

especially if one of the coins is zero

[Anthony Wang]

It seems like the coins have type PNat which rules out the possibility that one of the coins is 0.

[Aaron Liu]

oh I see

[Aaron Liu]

yeah but it still doesn't "terminate" in the sense that the termination checker wants you to prove

[Serena]

This is all of the code

def shortest? : List (List α) → Option (List α)
  | []    => none
  | a::as => some <| as.foldl (
    fun (a : List α) (b : List α) => if a.length < b.length then a else b
  ) a

abbrev PNat := { n : Nat // n > 0 }

def findChange (coins : List PNat) : Nat -> Option (List PNat)
  | 0 => some []
  | n => shortest? <| coins.filterMap
    fun (c : PNat) =>
      if n >= c then
        if let some change := findChange coins (n - c) then
          some <| c :: change
        else none
      else none

def findChangeMemo (coins : List PNat) (n : Nat) : Option (List PNat) :=
  let arr := Array.ofFn
    fun (n' : Fin (n + 1)) =>
      Thunk.mk fun _ => match n' with
      | 0 => some []
      | n' => shortest? <| coins.filterMap
        fun (c : PNat) =>
          if let some changeThunk := arr[n' - c.val]? >>= Thunk.get then
            some <| c :: changeThunk
          else none
  arr[n].get

Regular version works fine, memo version does not

[Aaron Liu]

what happens if I swap out Array.ofFn for my Array.ofFn'? Does it still "terminate"?

def Array.ofFn' : type_of% @Array.ofFn :=
  fun f => (Array.ofFn fun n => f n.rev).reverse

[Anthony Wang]

Since you're doing memoization, it might be easier to use a local imperatively function rather than thunks:

def shortest? : List (List α) → Option (List α)
  | []    => none
  | a::as => some <| as.foldl (
    fun (a : List α) (b : List α) => if a.length < b.length then a else b
  ) a

abbrev PNat := { n : Nat // n > 0 }

def findChange (coins : List PNat) : Nat -> Option (List PNat)
  | 0 => some []
  | n => shortest? <| coins.filterMap
    fun (c : PNat) =>
      if n >= c then
        if let some change := findChange coins (n - c) then
          some <| c :: change
        else none
      else none

def findChangeMemo (coins : List PNat) (n : Nat) : Option (List PNat) := Id.run do
  let mut arr := Vector.replicate (n + 1) none
  arr := arr.set 0 <| some []
  for h : i in [1:n + 1] do
    arr := arr.set i <| shortest? <| coins.filterMap
      fun c =>
        if c.val ≤ i then
          have : i < n + 1 := Membership.get_elem_helper h rfl
          arr[i - c.val].map (c :: ·)
        else
          none
  arr[n]

#eval findChange [⟨3, show 3 > 0 by grind⟩, ⟨5, show 5 > 0 by grind⟩, ⟨14, show 14 > 0 by grind⟩] 69

#eval findChangeMemo [⟨3, show 3 > 0 by grind⟩, ⟨5, show 5 > 0 by grind⟩, ⟨14, show 14 > 0 by grind⟩] 69

[Serena]

@Anthony Wang thanks, I was thinking about using do-notation but was still trying to figure it out. (I was thinking that thunks might be better to avoid mutability). Can I ask why you use Vector instead of Array? Vector isn't in the FPIL book afaik (or I missed it)

[Anthony Wang]

A vector has fixed length, so it makes the bounds check proofs go through.

[Vlad Tsyrklevich]

Serena said:

Vector isn't in the FPIL book afaik (or I missed it)

It is equivalent to Vect from Chapter 7