[nem-pl] [rfc] poster

[Lukasz Kaiser]

Hej.
 
> Pod http://nemerle.org/~malekith/budapest.pdf jest nowa wersja:
>   - przyk³ady s± okomentowane
>   - drzewa RB s± na koniec bez komentarza
>   - doda³em sekcjê o TRS i testach, ale co¶ tu trzeba bêdzie jeszcze
>     dodaæ
>   - takie tam drobne poprawki
> 
> Razem 12 stron, my¶lê, ¿e po 4 w rzêdzie.

12 stron jest chyba OK. Mam pytanie co do tego SQL, czy to to lname nie
powinno byc jakos poprzedzone np. jakims "as" albo czyms, bo to nie jest
konstrukcja sql tylko dodatek tego rozszerzenia a ile dobrze rozumiem, ale
w zasadzie to nie rozumiem tego przykladu do konca.

Jesli chodzi o sekcje o TRS i testach to proponuje inny tytul, bo ludzie
lepiej rozumieja "formal semantics" niz "TRS", szczegolnie w tytule.
Mysle, ze mozesz napisac po pierwszym punkcie ktory jest OK cos w stylu
* using term rewriting semantics it will be possible to prove program
  properties using existing equational theorem provers (Isabelle, VeriFun)

Male wyjasnienie dlaczego obok znanego wszystkimn Isabelle jest malo znany
i slabszy (ale jaki ladny ;)) VeriFun
(http://www.inferenzsysteme.informatik.tu-darmstadt.de/verifun/).
Problem z Isabelle polega na tym, ze trzeba podawany jej kod zrobic tak,
zeby byla jasno widoczna terminacja kazdej funkcji, wiec czasem nie bedzie
sie dalo wepchnac jej bezposrednio tlumaczenia z Nemerle. VeriFun tez
potrzebuje terminacji, ale pozwala sobie wepchnac kod funkcjonalny i
potem osobno udowodnic terminacje. Pewnie z Isabelle tez sie jakos tak da,
ale przez ta jej HOU (unifikacje l-termow) to wszystko jest mniej
zrozumiale, przynajmniej dla mnie i ja na razie nie wiem jak to zrobic.
Jesli potrzebujesz to moge jeszcze innych poszukac, chyba nadawalaby sie
tez INKA (dosc znane i duze), ale do tego musialbym zainstalowac Allegro
Common Lisp'a zeby to sprobowac uruchomic i niezbyt mi sie chce.

To jesli chodzi o dowodzenie, o testy popytaj Pawla.

Niezaleznie od plakatu - co sie dzieje z Andrzejem i z dokumentacja kodu ?

- lk