Apakah `sort` diketik pada logika affine dasar?

Istilah λ berikut, di sini dalam bentuk normal:

sort = (λabc.(a(λdefg.(f(d(λhij.(j(λkl.(k(λmn.(mhi))l))
       (h(λkl.l)i)))(λhi.(i(λjk.(bd(jhk)))(bd(h(λjk.(j
       (λlm.m)k))c)))))e))(λde.e)(λde.(d(λfg.g)e))c))

Menerapkan algoritma pengurutan untuk daftar yang dikodekan oleh gereja. Yaitu, hasil dari:

sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n))))

Demikian pula,

sort_below = λabcd.a(λef.f(λghi.g(λj.h(λkl.kj(ikl)))(hi))e(λgh.h))
            (λe.d)(λe.b(λf.e(f(λghi.hg)(λgh.cfh))))

Juga mengimplementasikan penyortiran untuk daftar yang sama seperti di atas, kecuali Anda harus memberikan argumen tambahan dengan batas untuk nomor yang akan dipertimbangkan:

sort_below 4 [5,1,3,2,4] → [1,2,3]

Saya mencoba untuk menentukan apakah istilah-istilah tersebut dapat diketik pada logika affine dasar. Karena saya tidak tahu jenis pemeriksa EAL yang tersedia untuk umum, ini membuktikan tugas yang lebih sulit dari yang saya harapkan. Apakah ada tipe untuk sortlogika affine dasar?

lo.logic lambda-calculus type-systems Viktor Maia
sumber

Apakah ini memiliki tipe "biasa"? Apa yang terjadi jika Anda mencolokkannya ke Haskell?

Andrej Bauer

Saya setuju dengan Andrej, syaratnya tidak bisa dibaca. Algoritma apa yang mereka terapkan? Beberapa penyortiran bilangan bulat tidak didasarkan pada perbandingan ? Sistem mengetik berbasis EAL apa yang Anda pertimbangkan? Yang naif (tanpa pengurangan subjek) atau yang oleh Coppola, Dal Lago dan Ronchi ? Apakah mereka dapat diketik dalam Sistem F, mis , di mana ? Jika tidak, maka tidak ada harapan mereka dapat diketik dalam sistem berbasis EAL.

s o r t : N a t L i s t \to N a t L i s t

$sort:\mathsf{NatList}\to\mathsf{NatList}$

N a t L i s t := \forall X . (N a t \to X \to X) \to X \to X

$\mathsf{NatList}:=\forall X.(\mathsf{Nat}\to X\to X)\to X\to X$

Damiano Mazza

Ya, ini karena ada functor yang pelupa dari EAL ke System F (atau ke tipe sederhana, jika Anda tidak menggunakan polimorfisme) sehingga jika dalam EAL, maka dalam Sistem F. Fakta bahwa evaluator Anda yang disederhanakan bekerja tidak konsisten dengan ini: apa yang membuat algoritma Lamping bekerja tanpa tanda kurung dan croissant adalah properti stratifikasi istilah, yang murni struktural dan tidak tergantung jenis: ada istilah yang tidak dapat diketik (dalam Sistem F, EAL, Haskell atau apa pun) yang bertingkat. Saya kira istilah Anda harus jatuh dalam kelas ini.

(\cdot)^{-}

$(\cdot)^-$

t : A

$t:A$

t^{-} : A^{-}

$t^-:A^-$

Damiano Mazza

Mungkin komentar ini bisa dijadikan jawaban?

Andrej Bauer

Saat membaca pertanyaan. :-)

Tayfun Bayar

Jawaban:

Saya pikir sort, seperti yang disajikan di sana, tidak dapat diketik pada EAL. Saya tidak bisa membuktikannya, tetapi itu tidak bekerja pada Algoritma Abstrak Lamping tanpa oracle. Selain itu, sementara istilahnya agak pintar dan singkat, ia menggunakan strategi yang sangat aneh yang tidak ramah-EAL.

Tetapi di balik pertanyaan ini ada yang lebih menarik: "dapatkah fungsi penyortiran nat diterapkan di EAL" ? Itu adalah pertanyaan yang sangat sulit pada waktu itu, tetapi sekarang itu terlihat sangat sepele. Ya tentu saja. Ada banyak cara sederhana untuk melakukannya. Sebagai contoh, seseorang dapat mengisi kode Scott yang dikodekan NatSetdengan kode Gereja Nat, dan kemudian mengonversinya menjadi daftar. Berikut ini adalah demonstrasi lengkap:

-- sort_example.mel
-- Sorting a list of Church-encoded numbers on the untyped lambda calculus
-- with terms that can be executed by Lamping's Abstract Algorithm without
-- using the Oracle. Test by calling `mel sort_example.mel`, using Caramel,
-- from https://github.com/maiavictor/caramel

-- Constructors for Church-encoded Lists 
-- Haskell: `data List = Cons a (List a) | Nil`
Cons head tail = (cons nil -> (cons head (tail cons nil)))
Nil            = (cons nil -> nil)

-- Constructors for Church-encoded Nats
-- Haskell: `data Nat = Succ Nat | Zero`
Succ pred = (succ zero -> (succ (pred succ zero)))
Zero      = (succ zero -> zero)

---- Constructors for Scott-encoded NatMaps
---- Those work like lists, where `Yep` constructors mean
---- there is a number on that index, `Nah` constructors
---- mean there isn't, and `End` ends the list.
---- Haskell: `data NatMap = Yep NatMap | Nah NatMap | End`
Yep natMap = (yep nah end -> (yep natMap))
Nah natMap = (yep nah end -> (nah natMap))
End        = (yep nah end -> end)

---- insert :: Nat (Church) -> NatMap (Scott) -> NatMap (Scott)
---- Inserts a Church-encoded Nat into a Scott-encoded NatMap.
insert nat natMap    = (nat succ zero natMap)
    succ pred natMap = (natMap yep? nah? end?)
        yep? natMap  = (Yep (pred natMap))
        nah? natMap  = (Nah (pred natMap))
        end?         = (Nah (pred natMap))
    zero natMap      = (natMap Yep Yep (Yep End))

---- toList :: NatMap (Scott) -> List Nat (Church)
---- Converts a Scott-Encoded NatMap to a Church-encoded List
toList natMap        = (go go natMap 0)
    go go natMap nat = (natMap yep? nah? end?)
        yep? natMap  = (Cons nat (go go natMap (Succ nat)))
        nah? natMap  = (go go natMap (Succ nat))
        end?         = Nil

---- sort :: List Nat (Church) -> List Nat (Church)
---- Sorts a Church-encoded list of Nats in ascending order.
sort nats = (toList (nats insert End))

-- Test
main = (sort [1,4,5,2,3])

Berikut adalah bentuk normal bruijn yang diindeks dari versi yang sedikit diubah di sortatas, yang harus diterima (x -> (x x))sebagai argumen pertama agar dapat berfungsi (jika tidak, ia tidak memiliki bentuk normal):

λλ(((1 λλλ(((1 λλλ((1 3) (((((5 5) 2) λλ(1 ((5 1) 0))) 1) 0))) 
λ(((3 3) 0) λλ(1 ((3 1) 0)))) λλ0)) ((0 λλ(((1 λλ(((0 λλλλ(2 (
5 3))) λλλλ(1 (5 3))) λλλ(1 (4 3)))) λ(((0 λλλλ(2 3)) λλλλ(2 3
)) λλλ(2 λλλ0))) 0)) λλλ0)) λλ0)

Cukup sederhana dalam retrospeksi.

Viktor Maia
sumber