Logika liniowa - Linear logic

Logika liniowa jest logiką substrukturalną zaproponowaną przez Jean-Yvesa Girarda jako udoskonalenie logiki klasycznej i intuicjonistycznej , łączącą dwoistość pierwszej z wieloma konstruktywnymi właściwościami tej drugiej. Chociaż logika była również badana dla niej samej, szerzej, idee z logiki liniowej miały wpływ na takie dziedziny, jak języki programowania , semantyka gier i fizyka kwantowa (ponieważ logikę liniową można postrzegać jako logikę teorii informacji kwantowej ). , a także językoznawstwo , szczególnie ze względu na nacisk na ograniczenie zasobów, dualizm i interakcję.

Logika liniowa nadaje się do wielu różnych prezentacji, wyjaśnień i intuicji. Dowód teoretycznie wywodzi się z analizy klasycznego rachunku sekwencyjnego, w którym użycie ( reguł strukturalnych ) kontrakcji i osłabienia jest dokładnie kontrolowane. Z operacyjnego punktu widzenia oznacza to, że dedukcja logiczna nie dotyczy już tylko stale powiększającego się zbioru trwałych „prawd”, ale także sposobu manipulowania zasobami, które nie zawsze mogą być powielane lub wyrzucane do woli. Jeśli chodzi o prostych modeli denotational logika liniowy może być postrzegane jako rafinacji interpretację intuicjonistycznej logiki zastępując kartezjański (zamknięte) kategorię przez symetryczny monoidal (zamknięte) kategorii lub interpretację logiki klasycznej zastępując logicznych algebr przez C * -algebras .

Połączenia, dwoistość i biegunowość

Składnia

Język klasycznej logiki liniowej (CLL) jest definiowany indukcyjnie przez notację BNF

A	::=	p | p ⊥
	|	A ⊗ A ∣ A ⊕ A
	|	A i A ∣ A ⅋ A
	|	1 ∣ 0 ∣ ⊤ ∣ ⊥
	|	! |? A

Tutaj p i p ^{rozchodzą się} po atomach logicznych . Ze względów być wyjaśnione poniżej, spójniki ⊗, ⅋, 1 i ⊥ są nazywane multiplicatives , z spójników &, ⊕, ⊤ i 0 nazywane są dodatki , a spójniki! oraz ? nazywane są wykładnikami . Możemy dalej posługiwać się następującą terminologią:

Symbol	Nazwa
⊗	spójnik multiplikatywny	czasy	napinacz
⊕	alternatywa addytywna	plus
&	addytywne połączenie	z
⅋	alternatywa multiplikatywna	par
!	oczywiście	huk
?	Dlaczego nie

Spójniki binarne ⊗, ⊕, & i ⅋ są asocjacyjne i przemienne; 1 to jednostka dla ⊗, 0 to jednostka dla ⊕, ⊥ to jednostka dla ⅋, a ⊤ to jednostka dla &.

Każde zdanie A w CLL ma podwójne A ^⊥ , zdefiniowane w następujący sposób:

( p ) ⊥ = p ⊥			( p ⊥ ) ⊥ = p
( A ⊗ B ) ⊥ = A ⊥ ⅋ B ⊥			( A ⅋ B ) ⊥ = A ⊥ ⊗ B ⊥
( A ⊕ B ) ⊥ = A ⊥ & B ⊥			( A & B ) ⊥ = A ⊥ ⊕ B ⊥
(1) ⊥ = ⊥			(⊥) ⊥ = 1
(0) ⊥ = ⊤			(⊤) ⊥ = 0
(! A ) ⊥ = ?( A ⊥ )			(? A ) ⊥ = !( A ⊥ )

Klasyfikacja spójników

	Dodaj	muł	do potęgi
pozycja	0	1	!
neg	&	⅋ ⊥	?

Zauważ, że (-) ^⊥ jest inwolucją , tzn. A ^⊥⊥ = A dla wszystkich zdań. ^⊥ jest również nazywany liniowy negację z A .

Kolumny tabeli sugerują inny sposób klasyfikowania spójników logiki liniowej, nazwany biegunowością : spójniki zanegowane w lewej kolumnie (⊗, ⊕, 1, 0, !) nazywane są dodatnimi , natomiast ich dualne po prawej (⅋, &, ⊥, ⊤, ?) nazywamy ujemnymi ; por. stół po prawej stronie.

Implikacja liniowa nie jest zawarta w gramatyce spójników , ale można ją zdefiniować w CLL za pomocą negacji liniowej i alternatywy multiplikatywnej, przez A ⊸ B  := A ^⊥ ⅋ B . Łącznik ⊸ jest czasami wymawiany jako „ lizak ”, ze względu na swój kształt.

Sekwencyjna prezentacja rachunku różniczkowego

Jednym ze sposobów definiowania logiki liniowej jest rachunek sekwencyjny . Używamy liter Γ i Δ do poruszania się po liście zdań A ₁ , ..., A _n , zwanych także kontekstami . SEQUENT umieszcza kontekst na lewo i na prawo od kołowrotu , pisemnej Tt Æ${\displaystyle \vdash}$ . Intuicyjnie sekwencja twierdzi, że koniunkcja Γ pociąga za sobą alternatywę Δ (chociaż mamy na myśli „multiplikatywną” koniunkcję i alternatywę, jak wyjaśniono poniżej). Girard opisuje klasyczną logikę liniową używając tylko jednostronnych sekwencji (gdzie kontekst po lewej stronie jest pusty), a my kierujemy się tutaj bardziej ekonomiczną prezentacją. Jest to możliwe, ponieważ każdy lokal na lewo od kołowrotu można zawsze przesunąć na drugą stronę i podwoić.

Podajemy teraz reguły wnioskowania opisujące, jak budować dowody sekwencji.

Po pierwsze, aby sformalizować fakt, że nie obchodzi nas kolejność zdań w kontekście, dodajemy strukturalną zasadę wymiany :

${\displaystyle \vdash}$Γ, A 1 , A 2 , Δ

${\displaystyle \vdash}$Γ, A 2 , A 1 , Δ

Zwróć uwagę, że nie dodajemy strukturalnych reguł osłabienia i skrócenia, ponieważ zależy nam na braku zdań w sekwencji i liczbie obecnych egzemplarzy.

Następnie dodajemy początkowe sekwencje i cięcia :

${\displaystyle \vdash}$ , ⊥

${\displaystyle \vdash}$, A       ${\displaystyle \vdash}$ ⊥ , Δ ${\displaystyle \vdash}$ ,

Reguła cięcia może być postrzegana jako sposób komponowania dowodów, a początkowe sekwencje służą jako jednostki kompozycji. W pewnym sensie reguły te są zbędne: wprowadzając poniżej dodatkowe reguły budowania dowodów, zachowamy własność, że dowolne ciągi początkowe można wyprowadzić z atomowych ciągów początkowych i że ilekroć sekwencja jest dowodliwa, można mu nadać cięcie. bezpłatny dowód. Ostatecznie ta właściwość formy kanonicznej (którą można podzielić na zupełność atomowych ciągów początkowych i twierdzenie o eliminacji cięcia , wywołujące pojęcie dowodu analitycznego ) leży za zastosowaniami logiki liniowej w informatyce, ponieważ pozwala na używany w wyszukiwaniu dowodów i jako zasobowy rachunek lambda .

Teraz wyjaśnimy spójniki, podając reguły logiczne . Zazwyczaj w rachunku sekwencyjnym podaje się zarówno „prawo-reguły”, jak i „lewo-reguły” dla każdego spójnika, zasadniczo opisując dwa sposoby rozumowania o zdaniach dotyczących tego spójnika (np. weryfikacja i falsyfikacja). W prezentacji jednostronnej zamiast tego używa się negacji: prawe reguły dla spójnika (powiedzmy ⅋) skutecznie pełnią rolę lewych reguł dla jego dualu (⊗). Powinniśmy więc oczekiwać pewnej „harmonii” między regułą (regułami) dla spójnika a regułą (regułami) dla jego duala.

Mnożniki

Zasady koniunkcji multiplikatywnej (⊗) i alternatywy (⅋):

${\displaystyle \vdash}$, A       ${\displaystyle \vdash}$, B ${\displaystyle \vdash}$Γ, Δ, A ⊗ B

${\displaystyle \vdash}$Γ, A , B ${\displaystyle \vdash}$, A ⅋ B

oraz dla ich jednostek:

${\displaystyle \vdash}$ 1

${\displaystyle \vdash}$ Γ ${\displaystyle \vdash}$ ,

Zauważ, że reguły dla koniunkcji i alternatywy multiplikatywnej są dopuszczalne dla koniunkcji i alternatywy w interpretacji klasycznej (tj. są to reguły dopuszczalne w LK ).

Dodatki

Reguły addytywnej koniunkcji (&) i alternatywy (⊕) :

${\displaystyle \vdash}$, A       ${\displaystyle \vdash}$, B ${\displaystyle \vdash}$, A i B

${\displaystyle \vdash}$, A ${\displaystyle \vdash}$, A ⊕ B

${\displaystyle \vdash}$, B ${\displaystyle \vdash}$, A ⊕ B

oraz dla ich jednostek:

${\displaystyle \vdash}$ ,

(brak reguły dla 0 )

Zauważ, że reguły addytywnej koniunkcji i alternatywy są ponownie dopuszczalne w klasycznej interpretacji. Ale teraz możemy wyjaśnić podstawę rozróżnienia multiplikatywno-dodatkowego w regułach dla dwóch różnych wersji koniunkcji: dla spójnika multiplikatywnego (⊗) kontekst wniosku ( Γ, Δ ) jest podzielony między przesłanki, podczas gdy dla przypadku addytywnego spójnik (&) kontekst wniosku ( Γ ) jest przenoszony w całości do obu przesłanek.

Wykładniczy

Wykładnicze są używane do zapewnienia kontrolowanego dostępu do osłabienia i skurczu. W szczególności dodajemy strukturalne reguły osłabiania i skracania dla zdań ?'d:

${\displaystyle \vdash}$ Γ ${\displaystyle \vdash}$, ? A

${\displaystyle \vdash}$, ? ,? A ${\displaystyle \vdash}$, ? A

i zastosuj następujące reguły logiczne:

${\displaystyle \vdash}$?Γ, A ${\displaystyle \vdash}$?Γ, ! A

${\displaystyle \vdash}$, A ${\displaystyle \vdash}$, ? A

Można zauważyć, że reguły dla wykładników mają inny wzór niż reguły dla pozostałych spójników, przypominając reguły wnioskowania rządzące modalnościami w kolejnych formalizacjach rachunku różniczkowego normalnej logiki modalnej S4 i że nie ma już tak wyraźnej symetrii między podwójne ! oraz ?. Sytuacji tej zaradzają alternatywne prezentacje CLL (np. prezentacja LU ).

Niezwykłe formuły

Oprócz opisanych powyżej dualności De Morgana , niektóre ważne równoważności w logice liniowej obejmują:

Dystrybucja

A ( B ⊕ C ) ≣ ( A ⊗ B ) ⊕ ( A ⊗ C )

( A ⊕ B ) ⊗ C ≣ ( A ⊗ C ) ⊕ ( B ⊗ C )

A ( B i C ) ≣ ( A ⅋ B ) i ( A ⅋ C )

( A & B ) ⅋ C ≣ ( A ⅋ C ) i ( B ⅋ C )

Z definicji A ⊸ B jako A ^⊥ ⅋ B , ostatnie dwa prawa dystrybucyjności również dają:

A ( B i C ) ≣ ( A ⊸ B ) i ( A ⊸ C )

( A ⊕ B ) ⊸ C ≣ ( A ⊸ C ) i ( B ⊸ C )

(Tutaj A ≣ B to ( A ⊸ B ) & ( B ⊸ A ) .)

Izomorfizm wykładniczy

! ( A i B ) ≣ ! ⊗! b

?( A ⊕ B ) ≣ ? ⅋? b

Rozkłady liniowe

Mapa, która nie jest izomorfizmem, ale odgrywa kluczową rolę w logice liniowej, to:

( A ⊗ ( B ⅋ C )) ⊸ (( A ⊗ B ) ⅋ C )

Rozkłady liniowe mają fundamentalne znaczenie w teorii dowodu logiki liniowej. Konsekwencje tej mapy zostały po raz pierwszy zbadane i nazwane „słabym rozkładem”. W kolejnych pracach zmieniono jego nazwę na „rozkład liniowy”, aby odzwierciedlić fundamentalny związek z logiką liniową.

Inne implikacje

Poniższe wzory na dystrybucję nie są na ogół równoważne, a jedynie implikacją:

! ⊗! B ⊸ ! ( A ⊗ B )

! ⊕! B ⊸ ! ( A ⊕ B )

?( A ⅋ B ) ⊸ ? ⅋? b

?( A i B ) ⊸ ? A i ? b

( A & B ) ⊗ C ⊸ ( A ⊗ C ) i ( B ⊗ C )

( A & B ) ⊕ C ⊸ ( A ⊕ C ) i ( B ⊕ C )

( A ⅋ C ) ⊕ ( B ⅋ C ) ⊸ ( A ⊕ B ) ⅋ C

( A & C ) ⊕ ( B & C ) ⊸ ( A ⊕ B ) & C

Kodowanie logiki klasycznej/intuicjonistycznej w logice liniowej

Zarówno implikacja intuicjonistyczna, jak i klasyczna może być odzyskana z implikacji liniowej przez wstawienie wykładników: implikacja intuicjonistyczna jest zakodowana jako ! A ⊸ B , natomiast implikację klasyczną można zakodować jako !? ⊸? B lub ! ⊸? B (lub różne alternatywne możliwe tłumaczenia). Chodzi o to, że wykładniki pozwalają nam używać formuły tyle razy, ile potrzebujemy, co jest zawsze możliwe w logice klasycznej i intuicjonistycznej.

Formalnie istnieje tłumaczenie formuł logiki intuicjonistycznej na formuły logiki liniowej w sposób gwarantujący, że oryginalna formuła jest dowodliwa w logice intuicjonistycznej wtedy i tylko wtedy, gdy przetłumaczona formuła jest dowodliwa w logice linearnej. Korzystając z przekładu negatywnego Gödla-Gentzena , możemy zatem osadzić klasyczną logikę pierwszego rzędu w liniową logikę pierwszego rzędu.

Interpretacja zasobów

Lafont (1993) po raz pierwszy pokazał, jak intuicjonistyczną logikę liniową można wyjaśnić jako logikę zasobów, zapewniając językowi logicznemu dostęp do formalizmów, których można użyć do wnioskowania o zasobach w samej logice, a nie, jak w logice klasycznej, przez środki nielogicznych predykatów i relacji. Klasyczny przykład automatu vendingowego Tony'ego Hoare'a (1985) może posłużyć do zilustrowania tego pomysłu.

Załóżmy, że posiadanie batonika reprezentujemy za pomocą propozycji atomowej cukierek , a posiadanie dolara za pomocą $1 . Aby stwierdzić, że za dolara można kupić jeden batonik, możemy napisać implikację $1 ⇒ cukierek . Ale w zwykłej (klasycznej lub intuicjonistycznej) logice z A i A ⇒ B można wnioskować A ∧ B . Tak więc zwykła logika prowadzi nas do przekonania, że ​​możemy kupić batonika i zatrzymać dolara! Oczywiście możemy uniknąć tego problemu, używając bardziej wyrafinowanych kodowań, chociaż zazwyczaj takie kodowania cierpią z powodu problemu z ramkami . Jednak odrzucenie osłabienia i kontrakcji pozwala logice liniowej uniknąć tego rodzaju fałszywego rozumowania, nawet przy „naiwnej” regule. Raczej niż $ 1 ⇒ cukierków , wyrażamy własność automatu jako liniowego implikację $ 1 ⊸ cukierków . Z 1 dolara i tego faktu możemy wywnioskować cukierki , ale nie 1 ⊗ cukierka . Ogólnie rzecz biorąc, możemy użyć propozycji logiki liniowej A ⊸ B, aby wyrazić słuszność przekształcenia zasobu A w zasób B .

Na przykładzie automatu sprzedającego rozważ „interpretacje zasobów” innych spójników multiplikatywnych i addytywnych. (Wykładniki zapewniają środki do połączenia tej interpretacji zasobów ze zwykłym pojęciem trwałej prawdy logicznej ).

Spójnik multiplikatywny ( A ⊗ B ) oznacza jednoczesne występowanie zasobów, które mają być używane zgodnie z poleceniami konsumenta. Na przykład, jeśli kupujesz gumę do żucia i butelkę napoju bezalkoholowego, prosisz o wypicie gumy ⊗ . Stała 1 oznacza brak jakiegokolwiek zasobu i dlatego działa jako jednostka ⊗.

Koniunkcja addytywna ( A & B ) reprezentuje alternatywne występowanie zasobów, których wybór kontroluje konsument. Jeśli w automacie znajduje się paczka chipsów, batonik i puszka napoju bezalkoholowego, każdy w cenie jednego dolara, to za tę cenę można kupić dokładnie jeden z tych produktów. Tak więc piszemy $ 1 ⊸ ( cukierki i chipsy i napój ) . Mamy nie napisać $ 1 ⊸ ( cukierek ⊗ Chips ⊗ napój ) , co oznaczałoby, że wystarczy jeden dolar za zakup wszystkich trzech produktów razem. Jednak z 1 $ ⊸ ( cukierek & frytki & napój ) możemy poprawnie wyliczyć 3 $ ⊸ ( cukierek ⊗ frytki ⊗ napój ) , gdzie 3 $  := $1 ⊗ $1 ⊗ $1 . Jednostka ⊤ addytywnej koniunkcji może być postrzegana jako kosz na śmieci na niepotrzebne zasoby. Na przykład możemy napisać 3 dolary ⊸ ( cukierek ⊗ ⊤), aby wyrazić, że za trzy dolary można dostać batonika i inne rzeczy, bez bardziej szczegółowych (na przykład frytki i napój lub 2 dolary lub 1 dolar z frytkami itp.).

Addytywna alternatywa ( A ⊕ B ) reprezentuje alternatywne występowanie zasobów, których wybór kontroluje maszyna. Załóżmy na przykład, że automat pozwala na hazard: włóż dolara, a automat może wydać batonik, paczkę chipsów lub napój bezalkoholowy. Możemy wyrazić tę sytuację jako 1 ⊸ ( słodycze ⊕ frytki ⊕ napój ) . Stała 0 reprezentuje produkt, którego nie można wytworzyć, a zatem służy jako jednostka ⊕ (maszyna, która może wyprodukować A lub 0, jest tak dobra, jak maszyna, która zawsze wytwarza A, ponieważ nigdy nie uda jej się wyprodukować 0). Więc w przeciwieństwie do powyższego, nie możemy z tego wywnioskować 3 $ ⊸ ( cukierki ⊗ frytki ⊗ napój ) .

Dysjunkcja multiplikatywna ( A ⅋ B ) jest trudniejsza do wyjaśnienia pod względem interpretacji zasobów, chociaż możemy zakodować z powrotem w implikację liniową, jako A ^⊥ ⊸ B lub B ^⊥ ⊸ A .

Inne systemy dowodowe

Siatki dowodowe

Wprowadzone przez Jeana-Yvesa Girarda sieci dowodowe zostały stworzone, aby uniknąć biurokracji , czyli wszystkich rzeczy, które różnią dwa wyprowadzenia z logicznego punktu widzenia, ale nie z „moralnego” punktu widzenia.

Przykładowo, te dwa dowody są "moralnie" identyczne:

${\displaystyle \vdash}$ A , B , C , D ${\displaystyle \vdash}$ ⅋ B , C , D ${\displaystyle \vdash}$ ⅋ B , C ⅋ D

${\displaystyle \vdash}$ A , B , C , D ${\displaystyle \vdash}$ A , B , C ⅋ D ${\displaystyle \vdash}$ ⅋ B , C ⅋ D

Celem sieci dowodowych jest ich utożsamienie poprzez stworzenie ich graficznej reprezentacji.

Semantyka

Semantyka algebraiczna

Rozstrzygalność/złożoność wnioskowania

Entailment relacja w pełni CLL jest nierozstrzygalny . Rozważając fragmenty CLL, problem decyzyjny ma różną złożoność:

• Multiplikatywna logika liniowa (MLL): tylko spójniki multiplikatywne. Wyciąganie MLL jest NP-zupełne , nawet ograniczając się do klauzul Horna w czysto implikacyjnym fragmencie lub do wzorów bezatomowych.
• Logika liniowa multiplikatywno-addytywna (MALL): tylko multiplikatywy i dodatki (tj. bezwykładnicze). Wyciąganie z MALL jest zgodne z PSPACE .
• Multiplikatywno-wykładnicza logika liniowa (MELL): tylko multiplikatywy i wykładniki. Redukując z problemu osiągalności dla sieci Petriego , pociąganie MELL musi być co najmniej EXPSPACE-trudne , chociaż sama rozstrzygalność ma status otwartego problemu od dawna. W 2015 r. w czasopiśmie TCS opublikowano dowód rozstrzygalności , który później okazał się błędny.
• Afiniczna logika liniowa (czyli logika liniowa z osłabieniem, raczej rozszerzeniem niż fragmentem) okazała się rozstrzygalna w 1995 roku.

Warianty

Wiele odmian logiki liniowej powstaje w wyniku dalszego majstrowania przy regułach strukturalnych:

• Logika afiniczna , która zabrania kontrakcji, ale pozwala na globalne osłabienie (rozstrzygalne rozszerzenie).
• Ścisła logika lub odpowiednia logika , która zabrania osłabienia, ale pozwala na globalne kurczenie się.
• Logika nieprzemienna lub logika uporządkowana, która oprócz ograniczenia osłabienia i kontrakcji usuwa zasadę wymiany. W logice uporządkowanej implikacja liniowa dzieli się dalej na implikację lewostronną i implikację prawostronną.

Rozważano różne intuicjonistyczne warianty logiki liniowej. Gdy opiera się na jednownioskowej, sekwencyjnej prezentacji rachunku różniczkowego, jak w ILL (Intuicjonistyczna Logika Liniowa), spójniki , ⊥ i ? są nieobecne, a implikacja liniowa jest traktowana jako prymitywny spójnik. W FILL (Full Intuitionistic Linear Logic) spójniki ⅋, ⊥ i ? są obecne, implikacja liniowa jest spójnikiem pierwotnym i, podobnie jak w logice intuicjonistycznej, wszystkie spójniki (poza negacją liniową) są niezależne. Istnieją również rozszerzenia pierwszego i wyższego rzędu logiki liniowej, których rozwój formalny jest nieco standardowy (patrz logika pierwszego rzędu i logika wyższego rzędu ).

Zobacz też

• System typu liniowego , o substructural System typ
• Logika jedności (LU)
• Siatki dowodowe
• Geometria interakcji
• Semantyka gry
• Logika intuicjonistyczna
• Logika obliczalności
• Ludyka
• spacje Chu
• Typ wyjątkowości
• Programowanie w logice liniowej

Bibliografia

Dalsza lektura

• Girard, Jean-Yves. Logika liniowa , Informatyka teoretyczna, t. 50, nr 1, s. 1-102, 1987.
• Girard, Jean-Yves, Lafont, Yves i Taylor, Paul. Dowody i typy . Cambridge Press, 1989.
• Hoare, CAR, 1985. Komunikowanie procesów sekwencyjnych . Prentice-Hall International. ISBN  0-13-153271-5
• Lafont, Yves, 1993. Wprowadzenie do logiki liniowej . Notatki z wykładów z letniej szkoły TEMPUS na temat metod algebraicznych i kategorycznych w informatyce , Brno, Czechy.
• Troelstra, AS Wykłady z logiki liniowej . CSLI (Centrum Studiów Języka i Informacji) Notatki do wykładu nr 29. Stanford, 1992.
• AS Troelstra , H. Schwichtenberg (1996). Podstawowa teoria dowodu . W serii Cambridge Tracts in Theoretical Computer Science , Cambridge University Press, ISBN  0-521-77911-1 .
• Di Cosmo, Roberto i Danos, Vincent. Elementarz logiki liniowej .
• Wprowadzenie do logiki liniowej (postscript) autorstwa Patricka Lincolna
• Wprowadzenie do logiki liniowej autorstwa Torbena Braunera
• Smak logiki liniowej Philipa Wadlera
• Logika liniowa autorstwa Roberto Di Cosmo i Dale'a Millera . The Stanford Encyclopedia of Philosophy (wydanie jesienne 2006), Edward N. Zalta (red.).
• Przegląd programowania w logice liniowej autorstwa Dale'a Millera . In Linear Logic in Computer Science , pod redakcją Ehrharda, Girarda, Rueta i Scotta. Wydawnictwo Uniwersytetu Cambridge. London Mathematical Society Lecture Notes, tom 316, 2004.
• Wiki o logice liniowej

Linki zewnętrzne

• Multimedia związane z logiką liniową w Wikimedia Commons
• Linear Logic Prover (llprover) , dostępny do użytku online, od: Naoyuki Tamura / Dept of CS / Kobe University / Japonia