Książki na temat semantyki języka programowania

31

Czytałem „ Semantykę z aplikacjami ” Nielsona i Nielsona i bardzo podoba mi się ten temat. Chciałbym mieć jeszcze jedną książkę na temat semantyki języka programowania - ale naprawdę mogę dostać tylko jedną.

Rzuciłem okiem na książkę Turbak / Gifford , ale jest ona zbyt długa; Myślałem, że Winskel będzie w porządku, ale nie mam do niego dostępu (nie ma go w naszej bibliotece uniwersyteckiej i brakuje mi pieniędzy) i nawet nie jestem pewien, czy nie jest datowany. Slonneger wydaje się OK, ale część praktyczna sprawia, że ​​jest on trochę za długi, a jego styl nie jest dla mnie zbyt wygodny.

Więc moje pytanie brzmi - czy Winskel to dobra książka? I czy to jest datowane?

Czy są też inne zwięzłe książki na ten temat?

reference-request pl.programming-languages semantics denotational-semantics books Sójka
źródło
5
dodano linki do stron wydawcy dla wszystkich książek. mogą być przydatne dla osób poszukujących przeglądania.
Suresh Venkat,
2
Jaką semantyką jesteś zainteresowany? Denotacyjny? Operacyjny? Przegląd?
Ohad Kammar,
@Ohad Kammar: Interesuje mnie jedno i drugie.
Jay

Odpowiedzi:

31

Wszystko zależy od tego, jak głęboko chcesz zejść i ile już wiesz. Dla początkującego książka Winksel jest naprawdę fajna, ale tak, nie wprowadza cię w stan semantyki, jak napisano około 20 lat temu. Niemniej jednak jest to dobre pierwsze wprowadzenie do tematu. Warto również wskazać, że T. Nipkow sformalizował znaczną część książki Winskela w Isabelle / HOL, patrz tutaj . Jeśli więc chcesz nauczyć się korzystać z interaktywnych asystentów sprawdzających wraz ze zrozumieniem semantyki języków programowania, masz wiele spójnych materiałów do wykorzystania.

Inne bardziej zaawansowane książki to:

  • Gunter, Semantyka języków programowania , bardziej zaawansowana książka skupiająca się na semantyce denotacyjnej, podejściu do semantyki, która nie spełniła oczekiwań. Koncentruje się na czysto funkcjonalnych językach i ignoruje współbieżność. Jest to książka, od której nauczyłem się semantyki jako licencjat, i z perspektywy czasu żałuję, że nie zamiast tego użyłem książki Winksel. Gunter nie jest łatwym do przeczytania dla początkującego.

  • Domeny i rachunek lambda Amadio i Curien. Kolejna książka, napisana bardziej w tradycji teoretycznej, choć omawia rachunek procesowy.

  • Książki Johna Mitchella, które zostały już wspomniane powyżej. Dotyczą one głównie obliczeń sekwencyjnych.

Książki takie jak TAPL Pierce'a są bardzo ładne, ale skupiają się wąsko na jednym aspekcie języków programowania, a mianowicie na typach, tak samo ważnych. Nie polecałbym tego jako pierwszego wprowadzenia do ogólnej dziedziny języków programowania, ale jest to obowiązkowe lektury dla każdego, kto chce dowiedzieć się o typach.

Prawdę mówiąc, myślę, że obecnie nie ma aktualnej książki wprowadzającej na temat semantyki języka, która odzwierciedla znaczny postęp, jaki nastąpił w ostatniej dekadzie, z jej zdecydowanym przejściem od metod denotacyjnych i obliczeń sekwencyjnych do współbieżności (kalkulacja procesów i semantyka gry) , semantyka aksjomatyczna i zastosowanie interaktywnych asystentów dowodowych w weryfikacji.

Aktualizacja 22. kwietnia 2014 r .: Tobias Nipkow i Gerwin Klein opublikowali nową książkę

co można uznać za „Winskel in Isabelle / HOL”. Jest to wprowadzenie do semantyki języków programowania (przede wszystkim operacyjnej i aksjomatycznej), ale w przeciwieństwie do wcześniejszych podejść opartych na pisaniu i pisaniu, ta książka wyraża całą swoją matematykę w Isabelle / HOL. Innymi słowy, jest to jednocześnie książka o dowodzeniu twierdzeń.

Książka jest zupełnie nowa, więc nie korzystałem z niej do nauczania, ale wydaje się ona naprawdę odpowiednia jako wstęp, który jest na niższym poziomie niż Software Foundations autorstwa Pierce i in.

Martin Berger
źródło
2
Czy odchodzi się od metod denotacyjnych? Wydaje mi się bardziej podobny do ludzi, którzy wcześniej używali ręcznych falowań, obecnie oczekuje się, że przedstawią formalne dowody. Ponieważ metody denotacyjne wciąż nie są w stanie łatwo modelować wszystkiego, co robimy, i wymagają o wiele więcej warunków wstępnych, badacze stosują bardziej przystępne metody, takie jak gry, kalkulacje procesów, asystenci dowodzenia. Nie jestem pewien, czy nastąpił spadek metod denotacyjnych.
Ohad Kammar,
4
Proszę nie mylić semantyki denotacyjnej z teorią domen . Semantyka gry może być i zazwyczaj jest całkowicie denotacyjna, tzn. Znaczenie programu jest funkcją znaczeń jego części.
Andrej Bauer,
2
Otworzyłem nowy wątek dotyczący tego komentarza. Ale nawet jeśli nie jestem pewien, czy zgadzam się z twoją definicją, semantyka gry ma charakter denotacyjny. Myślę, że powinienem zastąpić „gry” „semantyką operacyjną” w moim komentarzu i uwzględnić semantykę gier jako prawdopodobnie inną formę badań semantyki denotacyjnej. cstheory.stackexchange.com/questions/3577/…
Ohad Kammar
1
Nie jestem przekonany, że nastąpiła zmiana. Zobacz mój pierwszy komentarz w świetle komentarza Andreja.
Ohad Kammar,
1
Czy jest zmiana? Ciekawe pytanie. Jak możemy zmierzyć zmianę? Jest tak wiele kryteriów, które moglibyśmy zastosować, od względnie konkretnych, takich jak kwota dotacji na ponowne pozyskiwanie środków dla różnych podejść, po niejasne pomysły, takie jak dzielenie umysłu. Biorąc pod uwagę zaangażowanie, jako badaczy, pracowników i osób ubiegających się o dotacje, w wyniku takiego pytania, jest mało prawdopodobne, abyśmy uzgodnili odpowiedź.
Martin Berger,
20

Oto losowa próbka materiałów dostępnych bezpłatnie online:

  • Winskel, Formalna semantyka języków programowania , podgląd Książek Google . Nic nie wiem o tej książce. Jest na liście, ponieważ pytanie dotyczy konkretnie treści, która jest głównie online.
  • Morgan, Programowanie ze specyfikacji , lista plików ps . Przedmiotem jest udoskonalenie, czyli proces rozpoczynania od opisów niewykonywalnych na wysokim poziomie i systematycznego przekształcania się w coś wykonywalnego. Oczywiście, każdy krok dopracowania musi zachować semantykę, więc omawia także pewien typ semantyki (oparty głównie na predykatach treansformerów).
  • Harper, Praktyczne podstawy języków programowania , pdf projektu . Zobacz komentarz Dave'a Clarke'a poniżej.
  • Remy, korzystanie, rozumienie i odkrywanie języka OCaml , pdf . Jest to książka, z której dowiedziałem się programowania funkcyjnego (OCaml, dokładniej) i podobało mi się to dużo . Bardzo ładnie prezentuje semantykę podstawowych cech języka, a przy tym prezentuje rachunek lambda i teorię typów na zasadzie „musi wiedzieć”.
  • Peyton Jones, Implementation of Functional Programming Languages , djvu . Pierwsze rozdziały opisują rachunek lambda (i jego „semantykę operacyjną”) oraz opisują funkcje języka wyższego poziomu w rachunku lambda. W tym sensie praca przedstawia semantykę operacyjną języków funkcjonalnych.
  • Pierce (ed), Zaawansowane tematy w typach i językach programowania , podgląd Książek Google .
  • Slonneger, Składnia i semantyka języków programowania , lista plików pdf . Spojrzałem na to krótko dawno temu i nie podobało mi się to zbytnio. Jest na liście, ponieważ jest wymieniony w pytaniu.
  • Brookes, A Semantics for Concurrent Separation Logic , pdf . To duży artykuł (80 stron), a nie książka. Zawarłem go, ponieważ jest to dość niedawny rozwój, który uważam za interesujący.
Radu GRIGore
źródło
1
to dużo linków :)
Suresh Venkat
3
Byłoby to bardziej przydatne, gdyby został przedstawiony jako lista. W każdym razie poleciłbym książkę Harpera: kliknij „może”.
Dave Clarke,
Zgadzam się. Radu, czy mógłbyś wymienić książki, więc wiemy, co klikamy? byłby to doskonały zasób.
Suresh Venkat,
To jest teraz lista. (Pierwsza wersja została opublikowana około 2 rano, po spaniu około 5 godzin poprzedniej nocy.: P)
Radu GRIGore,
16

Książki na temat semantyki programowania dzieliłem na dwie klasy: te, które koncentrują się na modelowaniu pojęć języka programowania i te, które koncentrują się na podstawowych aspektach semantyki. Nie ma powodu, dla którego książka nie może robić obu tych rzeczy. Ale zazwyczaj jest tylko tyle rzeczy, które można umieścić w książce, a autorzy mają również własne predyspozycje do tego, co jest ważne.

Książka Winskela, o której już wspomniano, zawiera trochę obu aspektów. Jest to dobra książka dla początkujących. Równie dobrą, może nawet lepszą książką jest ta, którą zacząłem: Denotacyjny opis języków programowania Gordona . To była moja pierwsza książka na temat semantyki, którą przeczytałam wkrótce po ukończeniu pracy licencjackiej. Muszę powiedzieć, że dało mi to solidne podstawy w semantyce i nigdy nie musiałem się zastanawiać, jak semantyka denotacyjna różni się od semantyki operacyjnej czy semantyki aksomatycznej itp. Ta książka pozostanie moją ulubioną semantyką denotacyjną.

Inne książki, które koncentrują się na aspektach modelowania, a nie na aspektach podstawowych, są następujące:

  • Tennent's Semantyka języków programowania , która jest mniej więcej aktualną książką na temat semantyki imperatywnych języków programowania. Jest łatwy do odczytania. Jednak w późniejszych częściach książki wydaje się to abstrakcyjne i być może będziesz musiał się starać, aby zrozumieć, dlaczego rzeczy są robione w określony sposób.

  • Teorie języków programowania Reynoldsa . Każdy, kto specjalizuje się w semantyce, powinien zdecydowanie przeczytać tę książkę. W końcu jest to Reynolds. (David Schmidt zauważył kiedyś: „nawet jeśli Reynolds czyta ci poranną gazetę, chcesz słuchać uważnie, ponieważ możesz nauczyć się czegoś ważnego”!). Ma dobre omówienie zarówno aspektów modelowania, jak i aspektów fundamentalnych.

Najlepsze książki o fundamentalnych aspektach to Gunter (który uważam za podręcznik dla absolwentów) i Mitchell (który jest dobrym podręcznikiem na półce, ponieważ jest dość obszerny).

Uday Reddy
źródło
Bardzo miło cię tu mieć, Uday!
Radu GRIGore
Cieszę się, że tu też jestem. To bardzo fajny zasób!
Uday Reddy,
Co powiesz na: Przejścia i drzewa: wprowadzenie do strukturalnej semantyki operacyjnej od Hansa Hüttel 2010. Wydaje się, że miał dobre recenzje, ale nikt o tym nie wspomina.
Arturo Hernandez
1
@Uday: Dzięki za odpowiedź. Co oznaczają „koncepcje modelowania języka programowania” i „podstawowe aspekty semantyki”? Jakie są ich różnice i relacje?
Tim
1
@Tim: Aby nadać semantykę języka programowania, musisz stworzyć pewne struktury matematyczne, np. Zestawy w najprostszym przypadku, ale wyrafinowane struktury, takie jak domeny, kategorie, węgielne itp. Dla problemów, których zestawy nie mogą sobie poradzić. Przez „podstawowe aspekty” rozumiem teorię tych bardziej wyrafinowanych struktur. W pierwszym przypadku nacisk kładziony jest na języki programowania, a w drugim przypadku na podstawy matematyczne.
Uday Reddy,
8

Bardzo podobało mi się czytanie Winskel, gdy brałem udział w kursie semantycznym. Nie wiem jednak, czy jest to datowane, ponieważ nie prowadzę badań w tej dziedzinie. Zaletą Winskel jest to, że można go przetłumaczyć na inne języki niż angielski.

Do dalszej lektury, bardziej na poziomie magisterskim, sugerowałbym książki Johna Mitchella Podstawy programowania języków i pojęcia w językach programowania . Jeśli czytasz tylko pierwsze rozdziały, myślę, że spełniają one również twoje wymagania dotyczące zwięzłości.

Nie znajdziesz darmowych wersji tych książek, więc jeśli masz ograniczony budżet, wybierz „moc” w odpowiedzi Radu.

Alessandro Cosentino
źródło
6

Cóż, nie jestem ekspertem w tej dziedzinie, ale mogę udzielić kilku ogólnych rad.

Po pierwsze, są ludzie, którzy już przeczytali książkę i przedstawili recenzje na jej temat. Na przykład w książce Winskel The Formal Semantics of Programming Languages (patrz [1] i [2] ) znalazłem recenzje na Amazon.

Część jednej recenzji brzmi:

Ta książka od początku myli składnię i semantykę, jak oddzielanie literałów od ich wartości. Do ich rozróżnienia nie użyto żadnych specjalnych oznaczeń. Jest to kluczowa kwestia, którą autor powinien poruszyć w takim temacie. Ponadto niektóre inne notacje, które wykorzystał, są dość mylące, na przykład pokazanie przesłanek i wniosków.

Autor zdawał się zakładać, że masz WSZYSTKIE niezbędne warunki wstępne, ponieważ wyjaśnił materiały tła w kilku pierwszych rozdziałach (tj. Teorię zbiorów, semantykę operacyjną, indukcje, definicje indukcyjne) bardzo krótko. Styl, którego autor użył we wstępie, polega na umieszczeniu dwóch lub trzech akapitów tekstów, dodaniu formuł i wykonaniu ćwiczeń. Co jest dla mnie dość frustrujące ...

18/20 osób uważa tę recenzję za przydatną. Możesz poszukać Amazon (lub innych źródeł), aby zobaczyć więcej recenzji.

Po drugie, Amazon oferuje typy i języki programowania oraz podstawową teorię kategorii dla informatyków wraz z niniejszą książką. Na inny temat Dave Clarke oferuje te książki jako doskonałe na temat „Typów systemów i semantyki języka programowania”. Znowu nie jestem ekspertem, ale mogą ci się przydać.

MS Dousti
źródło
TaPL idzie trochę za wolno jak na mój gust. Jest to dobra książka, ale wspomniałem o tym, ponieważ osoba pytająca wydaje się martwić książkami o „długich wątkach”.
Radu GRIGore,
@Radu: Z pewnością TAPL działa wolno, ale jest to raczej dobre wprowadzenie. Książka Harpera, o której wspomniałeś w swoich linkach, idzie znacznie szybciej i obejmuje o wiele więcej, choć nie została jeszcze ukończona.
Dave Clarke,
4
Weź tę recenzję Amazonka książki Winskela ze szczyptą soli. Jest często używany jako zalecany tekst na studiach licencjackich z zakresu semantyki i prawdopodobnie przyciąga niezadowolonych studentów. Przeczytałem książkę i uznałem wstępne rozdziały za wystarczające. Jego notacja wydawała się również całkowicie standardowa.
Dominic Mulligan,