Alfa (particle traces)

[In English]

Alfa är en efterföljare till beviseditorn ALF, dvs en editor för direktmanipulering av bevisobjekt i ett logiskt ramverk baserat på Per Martin-Löfs typteori. Med Alfa kan man, interaktivt och inkrementellt, definiera teorier (axiom och härledningsregler), formulera satser och konstruera bevis av satser. Alla steg i beviskonstruktionen kontrolleras direkt av systemet, så det är omöjligt att konstruera felaktiga bevis.

Man kan också se Alfa som ett syntaxorienterad redigeringsprogram för ett litet, rent funktionellt programmeringsspråk med ett typsystem som har beroende typer. Det funktionella språket är i själva verket mycket likt språket Cayenne av Lennart Augustsson.

Alfa utvecklas av några av medlemmarna i Programmeringslogikgruppen vid Chalmers. Alfa utnyttjar ett beviskontrollprogram som ursprungligen skrevs av Thierry Coquand (V3) och sedan vidareutvecklades av Catarina Coquand (Agda). De senaste förbättringarna av Agda har gjorts av Makoto Takeyama. Han har lagt till idata-konstruktionen, för att få tillbaka en del av den uttryckskraft som fanns i de induktiva datadefintionerna i det gamla ALF-systemet.

Alfa har också visst stöd för att arbeta med översättningar av bevis till naturligt språk, genom att koppla ihop Alfa med Aarne Rantas Grammatiska Ramverk, GF.

Det grafiska användargränssnittet och infrastrukturen som kopplar samman alltihop implementeras av Thomas Hallgren. Alla programdelar skrivs i språket Haskell.

Vill du ladda ner Alfa, se nedan.


Alfa-dokumentation

Resten av dokumentationen är på engelska.

Länkar


Ladda ner Alfa

(Inga binärdistributioner finns att ladda ner längre, pga omorganisation. Tack för det, Chalmers.)

Alfa har testats och fungerar på bland annat följande system (oktober 2000):

Uppdatering 2017-08-26: några uppdatering för att koden ska gå att kompilera med den nuvarande versionen av GHC har gjorts. Källkod (ett Cabal-paket) and ett binärt installationspaket för macOS finns nu att ladda ner.

Uppdatering 2020-10-26: uppdaterade källkodpaket för Fudgets och Alfa är nu tillgängliga, för att göra det lättare att kompilera Alfa med de senaste versionerna av GHC. Det binära installationspaketet för macOS som nämns ovan finns också kvar.


Länkar