Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Новости HNC

Попилил сегодня экстрактор в Lean. Допилил до состояния, когда это
hnMain = {
        natr ff l = {
                g x total = sum total (ff x)
                natrec g 0 l
        }
        poww a = {
                f zz prod = mod (mul prod a) 1000000000
                natrec f 1 (sub a 1)
        }
        print (mod (sub (natr poww 1000) 1) 1000000000)
}
Экстрактится в это (но без отступов):
definition hnMain : IO void := 
  let natr (ff : num -> num) (l : num) : num := 
    let g (x : num) (total : num) : num := sum total (ff x) 
    in (natrec num) g 0 l 
  in 
    let poww (a : num) : num := 
      let f (t9 : Type) (zz : t9) (prod : num) : num := mod (mul prod a) 1000000000 
      in (natrec num) (f num) 1 (sub a 1) 
    in (print num) (mod (sub (natr poww 1000) 1) 1000000000)
Идея из двух частей:

- можно будет доказывать на Lean свойства программ на HN0
- можно будет ехать в обратную сторону: стирать термы Lean до Хиндли-Милнера и компилить в кресты.
Tags: functional programming, hn0
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments