Czy `sort 'można pisać na elementarnej logice afinicznej?

Następujący termin λ, tutaj w formie normalnej:

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))

Implementuje algorytm sortowania dla list zakodowanych w kościele. Oznacza to, że wynik:

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

Podobnie,

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))))

Implementuje również sortowanie dla tych samych list jak powyżej, z tym wyjątkiem, że musisz podać dodatkowy argument z ograniczeniem liczby, które będzie rozważał:

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

Próbuję ustalić, czy te terminy można pisać na elementarnej logice afinicznej. Ponieważ nie znam publicznie dostępnego sprawdzania typu EAL, jest to trudniejsze zadanie, niż się spodziewałem. Czy istnieje typ sortelementarnej logiki afinicznej?

lo.logic lambda-calculus type-systems

— MaiaVictor
źródło

Czy ma typ „zwykły”? Co się stanie, jeśli podłączysz go do Haskell?

— Andrej Bauer,

Zgadzam się z Andrejem, warunki są jako takie nieczytelne. Jakie algorytmy implementują? Jakieś sortowanie liczb całkowitych nie w oparciu o porównanie ? Jaki system pisania na klawiaturze EAL rozważasz? Naiwny (bez redukcji przedmiotu) czy Coppola, Dal Lago i Ronchi ? Czy można je wpisywać w systemie F, np. , gdzie ? Jeśli nie, to nie ma nadziei, że można je pisać w dowolnym systemie opartym na 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

Tak, ponieważ istnieje zapomniany funktor od EAL do Systemu F (lub do prostych typów, jeśli nie używasz polimorfizmu) tak, że jeśli w EAL, to w Systemie F. Fakt, że Twój uproszczony ewaluator działa, nie jest niespójny z tym: to, co sprawia, że algorytm Lampinga działa bez nawiasów i rogalików, jest rozwarstwieniem właściwości terminów, które są czysto strukturalne i niezależne od typów: istnieją terminy nietypowe (w Systemie F, EAL, Haskell lub cokolwiek innego), które są rozwarstwione. Myślę, że twój termin musi należeć do tej klasy.

(\cdot)^{-}

$(\cdot)^-$

t : A

$t:A$

t^{-} : A^{-}

$t^-:A^-$

— Damiano Mazza

Może te komentarze można zamienić w odpowiedź?

— Andrej Bauer,

Podczas czytania pytań. :-)

— Tayfun Zapłać

Wydaje mi się, że sorttak, jak tam przedstawiono, nie można pisać na EAL. Nie mogę tego udowodnić, ale nie działa on na abstrakcyjnym algorytmie Lampinga bez wyroczni. Co więcej, chociaż termin ten jest dość sprytny i krótki, wykorzystuje bardzo zwariowane strategie, które nie są przyjazne dla EAL.

Ale za tym pytaniem kryje się bardziej interesujące pytanie: „czy w EAL można zaimplementować funkcję sortowania nat” ? To było wtedy bardzo trudne pytanie, ale teraz wygląda dość trywialnie. Tak oczywiście. Istnieje wiele prostszych sposobów, aby to zrobić. Na przykład, można po prostu wypełnić kodowany przez Scott NatSetkodek Nats, a następnie przekonwertować go na listę. Oto pełna demonstracja:

-- 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])

Oto indeksowana przez bruijn normalna wersja nieco zmienionej wersji sortpowyższej, którą należy otrzymać (x -> (x x))jako pierwszy argument, aby zadziałał (w przeciwnym razie nie ma normalnej postaci):

λλ(((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)

Całkiem proste z perspektywy czasu.

— MaiaVictor
źródło