[nem-pl] projekty

[Lukasz Kaiser]

Oczywiscie pomylilem zalacznik.

- lk

-----------------------------------
-------------- next part --------------
Proponowane projekty (dokladniejszy opis)

Chcemy zrobic formalna semantyke Nemerle w stylu funkcjonalnym zeby:
 1) moc robic automatyczne testy,
 2) jak ktos chce mogl sie bawic w dowody formalne.
Dyskusje o tym, czy ludzie robiacy formalne dowody sa szaleni ani jak robic dowody 
automatycznie _nie_ zaliczaja sie do tych projektow. Zeby robic automatyczne testy
to trzeba miec pewne zalozenia - asercje wzgledem ktorych testujemy. Jezykiem do ich
wpisywania zajmie sie Grzesiek. Glownym problemem w tych projektach jest zakodowanie
imperatywnych konstrukcji Nemerle na prosty jezyk funkcjonalny (przepisywanie termow).
Trzeba to polaczyc z IDE i zrobic tak, zeby uzytkownik chcacy zrbic testy czy nawet ktos
chcacy robic dowod formalny nie musial sie uczyc tego kodowania.

1. Przepisywanie Termow

Trzeba sie nauczyc co to sa termy i jak to jest, ze reguly przepisywania termow to wlasciwie
programy funkcjonalne, np.
- append( nil, x ) -> list( x, nil )
- append( list( x, y ), z ) -> list( x, append( y, z ) )
definiuja funkcje dodajaca el. do listy.
Nie bede sie nad tym rozpisywal, mam nadzieje ze ToMasz to ladnie wytlumaczy i poda lepsze przyklady.

Trzeba jeszcze dodac kilka szczegolow technicznych. Termy beda przepisywane gorliwie, tzn. najpierw 
bedzie przepisywany ten redex w termie pod ktorym nie ma juz innych redexow. 
Jesli jest kilka takich redexow to moga byc  przepisywane rownolegle, np. w osobnych watkach.
Do tego jesli po lewej i prawej stronie wystepuje ta sama zmienna to nalezy kopiowac wskaznik a nie
cala zmienna jako term. Przy wykonywaniu rownoleglym trzeba sie przygotowac na skopiowanie kodu
programu ze wzgledu na sposob kodowania (nizej) i dlatego przy tlumaczeniu z jezyka wyzszego
poziomu powinna byc opcja - czy tlumaczyc na przepisanie po kolei czy rownolegle z kopiowaniem kodu.

2. Zakodowane Przepisywanie Termow

Jest jedna drobna wada prostego przepisywania termow - osobno sa reguly i osobno funkcje, wiec nie
jest zdefiniowane np. jak to zrobic zeby funkcja dodala nowe reguly przepisywania. 
Zeby moc robic takie rzeczy zakodujemy reguly przepisywania razem z termem ktory bedzie przepisywany
i bedziemy je podawac jako argument kazdej funkcji, tzn. zamiast
- append ( x, y ) 
bedzie
- append ( x, y, reguly przepisywania )
czyli zamiast
- append( list( x, y ), z ) -> list( x, append( y, z ) )
mamy
- append( list( x, y ), z, r ) -> list( x, append( y, z, r ) ).
Przy takim kodowaniu zarowno reguly przepisywania czyli kod programu jak i dane do przepisania
sa w jednym termie, ktory jest przepisywany gorliwie tak dlugo jak sie da.

Jest jeszcze jeden problem gdy dodajemy nowe funkcje maja one zwykle nowe nazwy, ktore sa etykietami
w termie i naleza do jakiegos ustalonego wczesniej zbioru mozliwych etykiet. Poniewaz my chcemy moc
dodawac nowe etykiety, to bedziemy kodowac tak, ze zamiast
- append( x, y, r )
bedzie
- fun( "append", x, y, r ), przy czym "append" to string zakodowany jako term.
Podobnie zrobimy z typami, tzn. zamiast
- list( 1, nil )
bedzie
- tycons( "list", tycons( "1" ), tycons( "nil" ) ).

Wazne jest, zeby to kodowanie bylo w miare niewidoczne, tzn. w skladni jezyka do wpisywania takich termow \
nie bedzie tego "tycons" ani "fun" ani tych dodatkowych zmiennych, bedzie jednak specjalna zmienna "system" 
pozwalajaca operowac na tej dodatkowej zmiennej i specjalne zmienne ktorych bedzie mozna uzywac w glowie 
termu, co bedzie tlumaczone do tycons( x, ... ).

Formalnie proponuje taka sygnature dla termow:
stale:  0, 1, nil, list, char
funkcyjne: fun o arnosci 4 oraz 10 symboli tyconsN dla N=0,1,2,...,8,32 do reprezentowania typow
o arnosci N+1 (wszystko mozna zakodowac binarnie, ale bardziej plaskie lepiej widac i mozna
cos wtedy zrozumiec i sie nie mylic co chwile).

3. Typy

Zwykle statyczne polimorficzne typowanie kazdy zna z OCamla czy MLa.
Do tego dochodza dwie rzeczy: interface'y i funkcje dynamiczne.
Nie planujemy zadnej rekonstrukcji typow na tym poziomie, dlatego musza byc one podawane
przy zmiennych i przy funkcjach.

Interface to prosta rzecz, po prostu lista funkcji. Potem mozna napisac, ze zbior zmiennych typowych
spelnia interface. Tak samo jak w calym Nemerle, mam nadzieje ze Michal to wytlumaczy.

Funkcje dynamiczne przy statycznym typowaniu moga sie wydawac problematyczne, ale wlasnie od tego jest dobre 
kodowanie. Wprowadzamy do jezyka symbol specjalny ?, ktory pozwala brac za zmienne etykiety w termach,
tzn. ?x( y ) dopasuje sie do np. list( nil ) i wtedy x = "list" a y = nil. Tlumaczenie jest jasne,
?x(y) = tycons( x, y ). Oczywiscie wyrazenie ?x(...) jest typu 'a. Jakis przyklad:

Zalozmy, ze chcemy funkcje eq : ( 'a, 'b ) -> bool ktora dla kazdych dwoch termow sprawdza,
czy sa rowne. Piszemy
- eq( 0, x ) -> if x = 0 then true else false //zapis skrotowy
- ... dla innych stalych, czyli w sumie 5 wersji
- eq( ?x( l ), ?y( m ) ) -> and2( eq( x, y ), eq( l, m ) )
- eq( ?x( l1, l2  ), ?y( m1, m2 ) ) -> and3( eq( x, y ), eq( l1, m1 ), eq( l2, m2 ) )
... dla roznych arnosci tycons, czyli 10 wersji.
Bez takiego rozszerzenia systemu typow takiej funkcji nie da sie napisac, a ona jest przydatna.

4. Skladnia

Jakas skladnie trzeba miec bo nie mozna pisac termow z palca jak tam sa takie rzeczy jak ten tycons
i do tego jeszcze reguly przepisywania razem z funkcjami.
Dlatego niech bedzie tak, ze piszemy dowolne termy, tylko z malej litery, bo z duzej sa zmienne, czyli
term := smallID "(" {term ","}+ ")" | largeID ":" type

Do tego potrzeba wpisywac reguly przepisywania, asercje, typy i interface'y, wiec podam prosta
gramatyke, ktora moze trzeba troche zmienic. {x}* znaczy 0 lub wiecej wystapien x, terminale sa
w cudzyslowiach, poza ID. Sa ID typow (tID), zmiennych (vID), funkcji (fID), konstruktorow (cID)
i interface'ow (iID).

vars := "(" {vID ","}* ")"
type := tID "(" { {vID | type} "," }* ")" | type "->" type

tydecl := "type" tID vars "=" { "|" cID "of" {type "*"}* }*
ifacedecl := "interface" iID vars "=" {fID ":" type }*
assertdecl := term "=" term
fundecl := "fun" fID ":" type {", where" vars "implements" iID }* "=" { term "->" term "," }*

expr := tydecl | ifacedecl | assertdecl | fundecl

Do tego potrzebne jest jeszcze naturalne kodowanie liczb, znakow, stringow, krotek i list, oraz termow bez 
tycons, tylko z dodatkowym znakiem ? o ktorym juz pisalem i dodatkowa mozliwoscia wywolania kazdej
funkcji z 3 dodatkowymi argumentami - nazwa funkcji, jej numerem i calym programem.

Jeszcze kilka uwag:
- przy uzyciu arnosci innej niz 0-8+32 powinien byc jakis warning,
- jesli chodzi o symbole stale, to zakladam, ze one nie sa tlumaczone, tzn. nil = nil a nie tycons( "nil" )
  a np. char( 'c' ) = tycons( char, 'c' ) a nie tycons( "char", 'c' ) co by prowadzilo do zakrecenia,
- mozna przeciazac nazwy jesli maja inna arnosc ale nie wystarczy inny typ, prawdziwe przeciazanie bedzie
  robione gdzies na wyzszym poziomie,
- zmienne w termach moga byc 3 rodzajow: zwykle (argumenty), wejscie (leniwie podstawiane, tylko
  jedna zmienna ale mozliwy rozny numer portu wejscia) i egzystencjalne w asercjach; proponuje tak
  to zakodowac: IN_n - wejscie z portu n, Ex_nazwa - zmienna egzystencjalna, reszta to zwykle
- przy kazdym typie moga byc jeszcze jakies atrybuty potrzebna np. przy kodowaniu pol prywatnych, zeby
  zachowywac takie informacje chociaz my z nich nie korzystamy, czyli raczej
type := tID "(" { {vID | type} "," }* ")" 
     | tID "attr" string "(" { {vID | type} "," }* ")" 
     | type "->" type.

5. Kodowanie

Kazdy umie sobie zakodowac liczby, stringi i w koncu typy i reguly przepisywania w termach, ale
zeby nie robil tego kazdy po swojemu to ja podam typy. Te typy sa podobne do napisanej powyzej
gramatyki bo wlasnie ja koduja, wiec wlasciwie sa jej przepisaniem.

Podstawowe:

type list a' = nil | list of 'a * list 'a // tzn. term list( 3, nil ) ma typ list int
type digit = 0 | 1
type int = list of digit
type sint = plus of int | minus of int 
type fp = fp of sint * sint // floating point = 0.x * 10^y
type char = char of digit^8 // nieformalnie, tzn. 8-bitowy char
type string = list of char
type desc = 0 | 1 | nil | char | list | string

Kodowanie zmiennych w termach wraz z typami:

type var = var of string * type )
type exvar = exvar of string * type
type invar = in of int // numer portu

Kodowanie typow i interface'ow:

dla czytelnosci:
type tyvar = tyvar of string
type iface = iface of string
type funname = funname of string

type type = tyvar | type of desc * list of type | funtype of type * type
type tagtype = tagtype of type * string * string // typ z atrybutem i nazwa
type tydecl = tdecl of string * list of ( string * list of tagtype )
type ifacedecl = ifacedecl of iface * list of tyvar * list of ( funname * type )


Kodowanie funkcji:

zwykle wywolania:
type data = tycons of desc * list of data
type funcall = fun of funname * data

lewa strona regul przepisywania:
type datapattern = var | invar |  tycons of  desc * list of datapattern
type funcallpattern = funpattern of funname * datapattern

prawa strona regul przepisywania:
type funpattern = var 
     | invar 
     | tycons of desc * list of funpattern 
     | fun of funname * funpattern
     | out of int * string // wypisz string na port numer int

regula przepisywania:
type rrule = rr of funcallpattern * funpattern

definicja funkcji:
type fundef = fundecl of funname * type * list of ( list of tyvar * iface ) * list of rrule

Asercje:

type funexpattern = var 
     | invar
     | exvar 
     | tycons of desc * list of funpattern 
     | fun of funname * funpattern
     | out of int * string // wypisz string na port numer int

type assert = eq of funexpattern * funexpattern

Tutaj kazda zmienna invar jest interpretowana jako zwykla zmienna a out nic nie znaczy, tzn. przepisuje
sie do pustego stringu.

Trzeba jeszcze zdefiniowac interface calego systemu, czyli zbioru funkcji, typow, interface'ow i  asercji
oraz byc moze jeszcze innych danych. Zrobimy to najpierw tak:

type system = sys of list of tydecl * list of ifacedecl * list of fundef * list of assert * list of data

Ale chcemy miec przynajmniej namiastke sensownej wydajnosci, wiec nie mozemy funkcji lub asercji trzymac
w listach. Dlatego zrobmy tak:

type array 'a = leaf of 'a | array of (array of 'a)^32

To sa tablice, ktore moga byc dosc plaskie (32^4 =~ milion). Teraz mozemy zamiast list zrobic tablice,
ale trzeba do kazdego wywolania funkcji dopisac numer tej funkcji w tablicy i dopisac to odpowiednio do 
typow napisanych wczesniej.

Jesli chodzi o typy, interface'y, asercje i dane, to mozna nie okreslac dokladnie w jaki sposob sa 
trzymane bo one sa dla innych programow, nie jest konieczne konkretne okreslenie typu w ktorym sa trzymane.
Wystarczy napisac interface i zaimplementowac jakikolwiek typ spelniajacy ten interface.
Przyklady interface'ow sa np. na stronie http://www.go-mono.org/docs/, np. IDictionary.

6. Co trzeba zrobic na poczatek.

Trzeba zrobic prosty programik w Nemerle, ktory:
- wczytuje kod programu i jeden term do wykonania zgodnie z podana w punkcie 4. gramatyka,
- zamienia ten kod na odpowiedni term S typu system dodajac np. numery funkcji w tablicy,
- z wczytanego termu i termu S tworzy jeden term zgodny z sygnatura opisana w 2. zamieniajac
  we wlasciwy sposob wszystkie ? i dodajac funkcjom nowe argumenty,
- robi zwykle gorliwe przepisywanie tego termu,
- wypisuje to co zostalo zgodnie z podana w punkcie 4. gramatyka (da sie o ile program byl poprawnie
  otypowany).

Potem trzeba napisac (juz w tym jezyku) program sprawdzajacy typy.
Do tego przydaloby sie zrobic ladna dokumentacje i ladnie to wszystko powyjasniac.

7. Testowanie i dowodzenie na poziomie termow

Na poziomie przepisywania termow wszystko co da sie udowodnic mozna udowodnic wykorzystujac tylko
dwie rzeczy:
- rozbicie przez indukcje pewnej zmiennej,
- udowodnienie innej rownosci jako lematu i jej wykorzystanie.
My mamy jeszcze zmienne egzystencjalne (zakladamy, ze konstruktywne), czyli kazda z tych zmiennych jest
jakims termem i mozna cos pod nia podstawic.
Trzeba to zaimplementowac tak, zeby te kroki byly robione na termach ale tylko gdy sa zgodne z typami
i zeby byly widoczne w jak wykonywane na jezyku termowym a nie na samych termach ze wszystkimi tycons itd.

Przy testowaniu mamy asercje rownosciowa bez zmiennych egzystencjalnych i mamy ja przetestowac, tzn.
sprobowac znalezc podstawienie pod zmienne ktore obala ta asercje. Widac, ze jest to dokladnie
odwrotny przypadek do dowodzenia. Trzeba generowac rozne losowe dane odpowiedniego typu i podstawiac.
Przy generowaniu tych danych trzeba brac pod uwage strukture asercji i funkcji w niej wystepujacych,
tzn. jesli mamy wstawic dane typu t to mozemy wypisac wszystkie mozliwe termy typu t do pewnej glebokosci
a potem pare wzorcow, sprawdzic asercje dla tych niskich termow a potem zrobic nowe asercje dla
wzorcow i sprawdzac je dalej razem z jakims occur checkiem. Mozna to tez ew. mieszac z dowodzeniem i
trzeba jeszcze dokladnie to ustalic.

Pewna idee jak to mogloby probowac dzialac mozna zobaczyc na takim trywialnym przykladzie:
asercja: x+256 < x+n
jak juz beda do tego jakies heurystyki, to mozna od razu zgadnac n = 256+m i dla x=m=1 koniec, ale mozna
rozbic po strukturze liczb (kodowanych binarnie), czyli
asercja 1: x+256 < x+0 // szybko sie dowodzi jakimis wiezami arytm., ze jest prawdziwe i dalej pomijamy
asercja 2: x+256 < x+1 // szybko sie dowodzi, ze jest prawdziwe i dalej pomijamy
asercja 3: x+256 < x+2n - rozbijamy dalej log. ilosc krokow i znajdujemy kontrprzyklad
asercja 4: x+256 < x+2n+1

Na poczatek jednak to nie musi byc zbyt zaawansowane, wazne zeby generowalo sensowne losowe dane
dowolnego typu przechodzace przez wszystkie rozgalezienia wywolania danej funkcji do zadanego
poziomu glebokosci i dawalo mozliwosc wygodnego zapisywania gdzies danych testowych od uzytkownika.


8. Podniesienie sie z abstrakcji

Trzeba zrobic jezyk abstract Nemerle z takimi samymi typami co nasz jezyk termow, ale dodatkowo z:
- wskaznikami,
- zmiennymi i wywolywaniem sekwencyjnym,
- wyjatkami.
To wszystko mozna dosc latwo zakodowac w termach, ale trzeba sprobowac na ile sie da zachowac czytelnosc
testowania i dowodzenia.
Potem trzeba pojsc jeszcze wyzej, czyli przetlumaczyc samo Nemerle na abstract Nemerle.

Oczywiscie potem pozostaje integracja z IDE i innymi projektami, dokumentacja, tutariale i testy.

- lk