Filozofija Informatike

2023 Autor: Noah Black | [email protected]. Zadnja promjena: 2023-08-25 04:38

To je spis u arhivu filozofske enciklopedije Stanford. Autor i podaci o citiranju | Prijatelji PDF pregled | InPho pretraživanje | PhilPapers Bibliografija

Filozofija informatike

Prvo objavljeno u petak, 12. prosinca 2008

Filozofija informatike (PCS)) bavi se filozofskim pitanjima koja proizlaze iz razmišljanja o prirodi i praksi akademske discipline informatike. Ali što je ovo posljednje? To sigurno nije samo programiranje. Uostalom, mnogi ljudi koji pišu programe nisu računalni znanstvenici. Na primjer, fizičari, računovođe i kemičari. Zaista bi se računalna znanost bolje opisala kao da se bavi meta-aktivnošću koja je povezana s programiranjem. Općenitije, i točnije, okupiran je dizajnom, razvojem i istraživanjem koncepata i metodologija koji olakšavaju i pomažu u specificiranju, razvoju, primjeni i analizi računskih sustava. Primjeri ove aktivnosti mogu uključivati dizajn i analizu programskih jezika, specifikacija i arhitektonskih opisa jezika;konstrukcija i optimizacija prevodilaca, tumača, dokaza i teoremskih sustava; izum logičkih okvira i dizajn ugrađenih sustava i još mnogo toga. Mnoga središnja filozofska pitanja informatike okružuju i podupiru te aktivnosti, a mnoga od njih usredotočuju se na logička, ontološka i epistemološka pitanja koja ih se tiču. Međutim, na kraju je računalna znanost ono što rade računalni znanstvenici, a nijedna točna formulacijska definicija ne može poslužiti kao vodilja raspravi koja slijedi. Doista, nada je tomeMnoga središnja filozofska pitanja informatike okružuju i podupiru te aktivnosti, a mnoga od njih usredotočuju se na logička, ontološka i epistemološka pitanja koja ih se tiču. Međutim, na kraju je računalna znanost ono što rade računalni znanstvenici, a nijedna točna formulacijska definicija ne može poslužiti kao vodilja raspravi koja slijedi. Doista, nada je tomeMnoga središnja filozofska pitanja informatike okružuju i podupiru te aktivnosti, a mnoga od njih usredotočuju se na logička, ontološka i epistemološka pitanja koja ih se tiču. Međutim, na kraju je računalna znanost ono što rade računalni znanstvenici, a nijedna točna formulacijska definicija ne može poslužiti kao vodilja raspravi koja slijedi. Doista, nada je tome PCS će s vremenom doprinijeti dubljem razumijevanju prirode informatike.

Ali mapiranje filozofskog krajolika informatike nije lak zadatak. Srećom, tradicionalne grane filozofije mogu pružiti intelektualne i strukturalne smjernice. Na primjer, u filozofiji matematike i fizike, centralna su pitanja koja se tiču prirode predmeta koji se obrađuju, što tvori znanje i načina za stjecanje tog znanja. Filozofija jezika postavlja pitanja o sadržaju i obliku semantičke teorije prirodnog jezika. On dovodi u prvi plan temeljne ontološke i epistemološke pretpostavke semantičkog pothvata. Ontologija označava vrste stvari koje postoje, kako ih individualizirati i njihovu ulogu u oblikovanju naših konceptualnih shema. Filozofija logike daje prikaz i analizu različitih vrsta logičkih sustava i njihove uloge u svakodnevnom i specijaliziranom diskursu. Analogije i sličnosti iz ove i drugih grana filozofije trebale bi biti korisne u identificiranju i rasvjetljavanju nekih središnjih filozofskih pitanja računalne znanosti. Postojeći utjecaj tih disciplina na PCS će se pojaviti dok nastavimo. Posebno će drugi, treći i četvrti odjeljak odražavati utjecaj ontologije i filozofije jezika i matematike.

• 1. Neka središnja pitanja

• 2. Postojanje i identitet

  • 2.1 Dvostruka priroda programa
  • 2.2. Programi i algoritmi
  • 2.3 Programi i specifikacije

• 3. Semantika

  • 3.1 Denotacijska i operativna semantika
  • 3.2 Provedba i semantička interpretacija
  • 3.3 Semantika, jednakost i identitet

• 4. Dokazi i programi

  • 4.1 Dokazi iz informatike
  • 4.2 Dokazi iz matematike
  • 4.3. Fizička i apstraktna ispravnost

• 5. Računalnost

  5.1 Teza crkve-Turing

• 6. Jezici programiranja i programiranja

  • 6.1 Apstrakcija
  • 6.2 Vrste i ontologija

• 7. Pravna i etička pitanja

  • 7.1 Autorska prava, patenti i identitet
  • 7.2 Ispravnost i odgovornost
• 8. Novi zavoji ili nova izdanja?
• Bibliografija
• Ostali internetski resursi
• Povezani unosi

1. Neka središnja pitanja

Za početak ćemo nabrojati ono što smo smatrali nekim od središnjih pitanja i pitanja. Ovo će čitatelju pružiti brzi pregled predmeta koji će nadopuniti detaljniju raspravu. Iako se mnogi od njih nisu izravno bavili u literaturi i potrebno im je neko pojašnjenje, ova pitanja ilustriraju vrste problema zbog kojih mi smatramo PCS.

1. Kakve su stvari programi? Jesu li apstraktni ili konkretni? (Moor 1978; Colburn 2004)
2. Koje su razlike između programa i algoritama? (Rapaport 2005a)
3. Što je specifikacija? I što se određuje? (Smith 1985; Turner 2005)
4. Jesu li specifikacije bitno različite od programa? (Smith 1985)
5. Što je provedba? (Rapaport 2005b)
6. Što razlikuje hardver od softvera? Postoje li programi u fizičkom i simboličkom obliku? (Moor 1978; Colburn 2004)
7. Koje su vrste digitalni objekti? Trebamo li novu ontološku kategoriju da bismo ih smjestili? (Allison i sur. 2005.)
8. Koji su ciljevi različitih semantičkih teorija programskih jezika? (Bijela 2004; Turner 2007)
9. Kako se pitanja iz filozofije programskih jezika odnose na paralelna u filozofiji jezika? (Bijela 2004)
10. Odnosi li se princip modularnosti (npr. Dijkstra 1968) na konceptualna pitanja cjelovite apstrakcije i kompozicijnosti?
11. Koje su temeljne konceptualne razlike između sljedećih programskih paradigmi: strukturirano, funkcionalno, logičko i objektno orijentirano programiranje?
12. Koje su uloge tipova u računalnoj znanosti? (Barandregt 1992; Pierce 2002)
13. Koja je razlika između operativne i denotacijske semantike? (Turner 2007)
14. Što za program znači da je točan? Kakav je epistemološki status dokaza ispravnosti? Da li se oni bitno razlikuju od dokaza iz matematike? (DeMillo i sur. 1979; Smith 1985)
15. Što utvrđuju dokazi o ispravnosti? (Fetzer 1988; Fetzer 1999; Colburn 2004)
16. Što je apstrakcija u računalnoj znanosti? Kako je to povezano sa apstrakcijom u matematici? (Colburn & Shute 2007; Fine 2008; Hale & Wright 2001)
17. Koje su formalne metode? Što je formalno kod formalnih metoda? Koja je razlika između formalne metode i neformalne? (Bowen & Hinchey 2005; Bowen & Hinchey 1995)
18. Kakva je disciplina informatika? Koje su uloge matematičkog modeliranja i eksperimentiranja? (Minsky 1970; Denning 1980; Denning 1981; Denning i dr. 1989; Denning 1985; Denning 1980b; Hartmanis 1994; Hartmanis1993; Hartmanis 1981; Colburn 2004; Eden 2007)
19. Treba li programe smatrati znanstvenim teorijama? (Rapaport 2005a)
20. Kako se matematika koristi u računarskoj znanosti? Koriste li se matematički modeli na opisni ili normativni način? (Bijela 2004; Turner 2007)
21. Da li teza Church-Turing obuhvaća matematički pojam učinkovite ili mehaničke metode iz logike i matematike? Da li obuhvaća proračune koje čovjek može izvesti? Primjenjuje li se njegov opseg na fizičke strojeve? (Copeland 2004; Copeland 2007; Hodges 2006)
22. Može li pojam računalnog mišljenja odoljeti filozofskom ispitivanju? (Krilo 2006)
23. Koja je odgovarajuća logika za razmišljanje o ispravnosti i prekidu programa? (Hoare 1969; Feferman 1992) Kako logika ovisi o temeljnom programskom jeziku?
24. Što su informacije? (Floridi 2004; Floridi 2005) Da li ovaj pojam baca svjetlo na neka od ovdje navedenih pitanja?
25. Zašto postoji toliko programskih jezika i programskih paradigmi? (Krishnamurthi 2003)
26. Imaju li programski jezici (i paradigme) prirodu znanstvenih teorija? Što uzrokuje pomak paradigme programiranja? (Kuhn 1970)
27. Postavlja li softverski inženjering bilo kakva filozofska pitanja? (Eden 2007)

U nastavku ćemo staviti malo mesa na nekoliko ovih pitanja.

2. Postojanje i identitet

Kako kategoriziramo i individualiziramo cjeline i pojmove informatike? Kakve su stvari i što im određuje identitet? Na primjer, neki su jasno konkretni fizički objekti (npr. Čipovi, usmjerivači, prijenosna računala, grafičke kartice), a neki nisu (npr. Formalne gramatike, apstraktni strojevi, dokazi teorema, logički okviri, procesne algebre, apstraktni tipovi podataka). No karakterizacija nekih središnjih pojmova poput programa i podataka bila je problematičnija. Posebno je utvrđeno da ontološki status programa nije posve jasan, niti ima pitanje njihovih kriterija identiteta.

2.1 Dvostruka priroda programa

Mnogi autori (Moor 1978; Rapaport 2005b; Colburn 2004) raspravljaju o takozvanoj dualnoj prirodi programa. S druge strane, program ima tekstualni i mehanički ili procesni oblik. Kao tekst, program se može uređivati. No čini se da njegova manifestacija na strojno čitljivom disku ima sasvim drugačija svojstva. Posebno se može izvesti na fizičkom stroju. Dakle, prema načelu neizrecivosti identiteta (§ 3.3), dvije vrste ne mogu biti isti entitet. Naravno, svatko tko je uvjeren u ovu dvojnost dužan je reći nešto o odnosu između ta dva prividna oblika postojanja.

Jedan neposredni prijedlog je da je jedna manifestacija programa provedba druge, tj. Da je fizička manifestacija implementacija tekstualne. Međutim, ni u ograničenjima informatike nije odmah jasno da se riječ implementacija odnosi samo na jedan pojam. Često se koristi za upućivanje na rezultat postupka kompilacije gdje se program na jeziku visoke razine (izvorni kod) pretvara u strojni jezik (objektni kod). Ali podjednako se često koristi za označavanje procesa u kojem se izvorni kod nekako izravno realizira u hardveru (npr. Konkretna implementacija u poluvodiče). I pretpostavlja se da je to mjerodavan pojam. Ali bez detaljnije filozofske analize samog pojma provedbe (§3.2) (Rapaport 2005b),nejasno je na koji način to napreduje u raspravi; čini se da smo samo imenovali odnos dvaju prividnih oblika postojanja. Na sličan je način drugi opisao odnos programa-teksta i programskog procesa kao sličan onome između plana i njegove manifestacije kao niza fizičkih akcija. No čini se da to nije sasvim analogno uparivanju programskog procesa: nismo u iskušenju da plan i fizički proces označavamo kao različite manifestacije iste stvari. Na primjer, da li smo u iskušenju razmišljati o planu za šetnju i stvarnom hodu kao o različitim aspektima iste stvari?drugi su odnos programa-teksta i procesa-programa opisali kao sličan odnosu između plana i njegove manifestacije kao niz fizičkih radnji. No čini se da to nije sasvim analogno uparivanju programskog procesa: nismo u iskušenju da plan i fizički proces označavamo kao različite manifestacije iste stvari. Na primjer, da li smo u iskušenju razmišljati o planu za šetnju i stvarnom hodu kao o različitim aspektima iste stvari?drugi su odnos programa-teksta i procesa-programa opisali kao sličan odnosu između plana i njegove manifestacije kao niz fizičkih radnji. No čini se da to nije sasvim analogno uparivanju programskog procesa: nismo u iskušenju da plan i fizički proces označavamo kao različite manifestacije iste stvari. Na primjer, da li smo u iskušenju razmišljati o planu za šetnju i stvarnom hodu kao o različitim aspektima iste stvari?da li smo u iskušenju razmišljati o planu za šetnju i stvarnom hodu kao o različitim aspektima iste stvari?da li smo u iskušenju razmišljati o planu za šetnju i stvarnom hodu kao o različitim aspektima iste stvari?

Možda su stvari najbolje opisane riječima da programi kao tekstualni objekti uzrokuju mehaničke procese? Čini se da je ideja da tekstualni objekt nekako fizički izaziva mehanički proces. No, čini se da bi to zahtijevalo prilično pažljivu analizu prirode takvog uzročno-posljedičnog odnosa. Colburn (2004) negira da simbolički tekst ima kauzalni učinak; njegova fizička manifestacija (stvar na disku) ima takav učinak. Softver je konkretna apstrakcija koja ima medij opisa (tekst, apstrakcija) i medij izvedbe (npr. Konkretnu implementaciju u poluvodičima).

Nešto drugačija perspektiva ovih pitanja polazi od pitanja identiteta programa. Kada se dva programa uzimaju kao jednaka? Takva se pitanja javljaju, na primjer, pri pokušajima utvrđivanja pravnog identiteta dijela softvera. Ako program identificiramo s njegovom tekstualnom manifestacijom, tada je identitet programa osjetljiv na promjene u njegovom izgledu (npr. Na promjenu fonta). Očigledno da nam tekst nije samo filozofski zanimljiv pojam programskog identiteta. Umjesto toga, da bismo dostigli informirani kriterij identiteta, moramo više voditi računa o semantičnosti i implementaciji. Vratit ćemo se ovoj temi u §3 i §6.

2.2. Programi i algoritmi

Bez obzira na to o kojem programu gledamo, razlikovanje algoritam i program također je potrebno za dodatna konceptualna pojašnjenja. Algoritmi se često smatraju matematičkim objektima. Ako je to istina, onda mnoga filozofska pitanja koja se njih tiču pripadaju i filozofiji matematike. Međutim, algoritmi su vjerovatno u središtu informatike nego matematike i zaslužuju više filozofske pažnje nego što im se poklanja. Iako je došlo do značajnog matematičkog proučavanja algoritama u teorijskoj računalnoj znanosti i matematičkoj logici (npr. Moschovakis 1997; Blass i Gurevich 2003), nije bilo puno filozofske rasprave koja je usredotočena na prirodu algoritama i razlike između algoritmi i programi.

Je li to da su algoritmi apstraktni objekti, u smislu koji nudi Rosen (2001), dok su programi konkretni? Preciznije, jesu li algoritmi apstraktni matematički kolega tekstualnog objekta koji je program? Ova se slika prirodno podnosi obliku ontološkog platonizma (Shapiro 1997), gdje algoritmi imaju ontološki prioritet, a programi daju jezične načine da se na njih dokopaju. Prema ovom mišljenju, mogu se uzeti algoritmi za pružanje semantike (§3) programskih jezika. Naravno, ova slika nasljeđuje sve prednosti i probleme s takvom platonskom perspektivom (Shapiro 1997).

Manje platonski prikaz smatra da algoritmi sadrže ideje izražene u programu. U zakonu je to shvaćeno kao razlog što algoritmi, za razliku od programa, ne mogu biti zaštićeni autorskim pravima (§7.1). Naravno, pojam ideja zahtijeva daljnju filozofsku analizu. Doista, može se tvrditi da je ogoljeni pojam algoritma potrebno mnogo manje pojašnjenja od standardnog prikaza ideja i pridruženih ideja apstrakcije (Rosen 2001).

Konačno, gotovo je folklorno stajalište da nam Turingovi strojevi pružaju formalnu analizu našeg pojma algoritma. No, odgovara li onom suvremenom pojmu koji je korišten u modernoj računalnoj znanosti sa svojim sofisticiranim pojmovima reprezentacije i kontrole? Moschovakis (1997) nudi analizu koja ide nešto bolje.

2.3 Programi i specifikacije

Još jedno popularno razlikovanje koje bi trebalo biti tema kritičke analize javlja se u odnosu na programe i specifikacije. Što su specifikacije i kako se razlikuju od programa? Iako je u filozofskoj literaturi malo izravne rasprave o ovom pitanju (ali vidi Smith 1985), priroda specifikacija temeljno je pitanje za konceptualne temelje informatike.

Jedno gledište, koje se u formalnim specifikacijama nalazi u udžbenicima, je da programi sadrže detaljne strojne upute dok (funkcionalne) specifikacije samo opisuju odnos ulaza i izlaza. Jedan očigledan način da se ovo raspakira je u pogledu imperativnog / opisnog razlikovanja: programi su imperativ i opisuju kako postići cilj opisan specifikacijom. Dakako, čini se da u imperativnoj programskoj paradigmi to čini značajnu razliku. Ali to nije prikladno za sve. Na primjer, logički, funkcionalni i objektno orijentirani programski jezici očito ne upravljaju: uzeti po nominalnoj vrijednosti, programi kodirani u takvim jezicima sastoje se od niza definicija, a ne 'upute'. Osim toga,nefunkcionalne specifikacije ne mogu se artikulirati kao izjave o odnosu ulaza i izlaza, jer nameću zahtjeve dizajnu i vrsti upute koje mogu biti uključene u bilo koji program.

Drugo gledište inzistira na tome da se razlika između specifikacija i programa mora nalaziti u smislu pojma provedbe, tj. Može li se sastaviti i izvršiti? Ali što se pod tim misli? Da li to znači u smislu postojanja postojećeg prevoditelja? Ova je interpretacija prilično plitka jer ne nudi konceptualni kriterij razlikovanja, već kontingentni. Na primjer, tijekom prvih pet generacija programskih jezika (2. polovica 20. stoljeća) rekurzivne, modularne, funkcionalne i objektno orijentirane specifikacije jedne generacije postale su artikulirane kao programi u sljedećoj, tj. Današnjim jezicima specifikacija često postaju sutrašnji programski jezici.

Drugo gledište sugerira da su programski jezici oni jezici koji imaju načelnu implementaciju, dok su specifikacijski jezici oni koji to ne mogu. I vjerojatno je razlog da to ne mogu biti u tome što jezici specifikacija dopuštaju izražavanje pojmova koji nisu Turingovi izračunavi. To je razlikovanje u skladu s mnogim postojećim jezicima specifikacija koji se temelje na teoriji skupova Zermelo-Fraenkel i logici višeg reda. Međutim, čini se čudnim da ono što treba da karakterizira jezik specifikacije je činjenica da može iskazivati svojstva i odnose koji se ne mogu izračunati. Je li neki od tih neračunalih zahtjeva zaista potreban u praksi (Jones & Hayes 1990; Fuchs 1994)?

Raznolikost ovih stajališta sugerira da je tradicionalna, binarna podjela između specifikacija i programa primjer problema u PCS-u koji zaslužuje više pažnje, ne samo zbog konceptualnog pojašnjenja, već i zbog toga što bi moglo imati implikacija na dizajn budućih programa i jezika specifikacija.,

3. Semantika

Gramatika programskog jezika određuje samo ono što je sintaktički legitimno; ne obavještava nas o namjeravanom značenju njegovih konstrukata. Stoga gramatika programskog jezika sama po sebi ne određuje ono što ljudi programiraju. Umjesto toga, gramatika obogaćena semantičkim obračunom (formalnim ili neformalnim) uzima se za to. Semantika je namijenjena informiranju programera, pisca sastavljača i teoretičara zainteresiranog za istraživanje svojstava jezika. Doista, često se tvrdi da su za ispunjavanje različitih zahtjeva programera i sastavljača potrebni različiti semantički računi, na različitim razinama apstrakcije. A posao teoretičara je istražiti njihov odnos.

Ovo je standardna slika koja se pojavljuje u semantičkoj literaturi. No mnogo toga treba konceptualna pojašnjenja. U ovom odjeljku razmatramo samo nekoliko pitanja koja proizlaze iz ove aktivnosti.

3.1 Denotacijska i operativna semantika

Jedno od najvažnijih razlikovanja semantike programskih jezika usredotočuje se na razliku između operativne i denotacijske semantike. Operativna semantika (Landin 1964; Plotkin 1981) pruža tumačenje programskog jezika u smislu nekih apstraktnih strojeva. Točnije, prijevod izraza u programskom jeziku u upute ili programe apstraktnog stroja. Na primjer, program 1 raspakirao bi se u redoslijed apstraktnih strojnih operacija, poput "a ← 0" i push. Operativna semantika može se zamisliti i kao algoritmička semantika, posebno kada je stroj namijenjen karakterizaciji samog pojma algoritma (npr. Moschovakis 1997).

Suprotno tome, denotacijska semantika (Milne & Strachey 1977) daje interpretaciju matematičkih struktura poput skupova ili kategorija. Na primjer, u klasičnom pristupu, matematički okvir pružaju matematički okvir u obliku cjelovitih rešetki i kontinuiranih funkcija na njima.

Ali postoji li neka značajna konceptualna razlika između njih? Je li to što je denotacijska semantika eksplicitno utemeljena na matematičkim strukturama poput skupova matematička, dok operativna semantika nije? Turner (2007) ne tvrdi: svi oni daju matematičke interpretacije.

Ili je operativna semantika više slična stroju, u smislu stvaranja apstraktnog stroja, dok kod denotacijske semantike, koja je dana teoretski skupa, nema nagovještaja o apstraktnom stroju? Takve se razlike, međutim, nisu pokazale konceptualno značajnima jer se denotacijski semantički računi mogu promatrati kao strukture koje čine apstraktni stroj sa stanjem i operacijama koje djeluju na njima. Niti su operativni računi bliži implementaciji: denotacijski pristupi (Milne i Strachey 1977) također su vrlo fleksibilni i sposobni su odražavati različite razine detalja o provedbi.

Druga moguća razlika odnosi se na kompozicijsku (ili na neki drugi način) prirodu semantike. Zamišljeno je da se semantika smatra kompozicijskom (Szabó 2007) ako je semantička vrijednost složenog izraza funkcija semantičke vrijednosti njegovih dijelova. Skladateljstvo se smatra ključnim kriterijem semantike, jer se čini da je potrebno objasniti produktivnost našeg jezičnog razumijevanja: kaže se da objašnjava kako razumijemo i konstruiramo složene programe. Ali pruža li nam klin da razdvojimo operativnu i denotacijsku semantiku? Nažalost, čini se da to nije tako: iako su denotacijske definicije oblikovane kao kompozicijske, to sigurno nije slučaj da sva operativna semantika nije kompozicijska.

Konačno, neke semantičke verzije razlikuju se u pogledu postojanja rekurzivnog modela, tj. Interpretacije u Turingovim strojevima ili Gandijevim strojevima (§5.1). Međutim, čak ni to se ne podudara s tradicionalnom operativnom / denotacijskom podjelom. Neke denotacijske definicije imaju rekurzivni model, a neke ne.

Čini se da je to teško teško ukloniti. S druge strane, ne postoji oštra konceptualna razlika između operativne i denotacijske semantike.

3.2 Provedba i semantička interpretacija

Koja je razlika između semantičke interpretacije i implementacije? Na primjer, koja je konceptualna razlika između sastavljanja programa u strojni kod i davanja denotacijske semantike? Prema Rapaport (2005b), implementacija se najbolje promatra kao semantička interpretacija, gdje se potonja karakterizira preslikavanjem između dviju domena: sintaktičke i semantičke. I oba su određena pravilima nekog opisa. Na primjer, sastavljeni kod (u kombinaciji s pravilima koja reguliraju njegovu semantiku) je semantički prikaz izvornog koda.

U uobičajenom razumijevanju termina "implementacija", semantičku domenu daje fizički stroj. Drugim riječima, sam fizički stroj ('implementacija') određuje što program znači. Na primjer, u programskim jezicima to je ekvivalent tvrdnji da semantiku za programski jezik C ++ određuje Bjarneovo računalo na kojem radi njegov C ++ prevodilac. Ali ovo je objašnjenje očito neprimjereno: ako pretpostavimo da Bjarneov stroj određuje značenje programa C ++, tada ne postoji pojava neispravnosti ili pogrešne interpretacije: što god Bjarneov kompjuter radi, ipso facto, značenje programa. Ali zasigurno, oluja može uzrokovati da se stroj pokvari. Ali što bismo mogli značiti ako idemo krivo? Pretpostavlja se da (neispravni) stroj ne utječe na predviđeno značenje. Ali,zauzvrat, čini nam se da samo možemo shvatiti ovu frazu na temelju neke strojno neovisne karakterizacije značenja. A na nekoj razini to se mora dati kroz neovisni semantički opis. Ovo sugeriše da pojam gole implementacije ne nudi adekvatan pojam semantike. (Usporedi s: Kripke 1982; Wittgenstein 1953).

3.3 Semantika, jednakost i identitet

Zaključili smo raspravu o programskoj jednakosti (§2.1) obećanjem da ćemo semantiku unijeti u sliku. Svaki semantički prikaz programskog jezika određuje pojam jednakosti programa, naime, dva se programa uzimaju jednaka ako imaju istu semantičku vrijednost, tj.

P = Q iff || P || = || Q ||

gdje || P || je semantička vrijednost programa P. U tom smislu svaki semantički račun određuje kriterij jednakosti. Na primjer, jedna inačica denotacijske semantike apstrahirala bi se od svih računskih koraka i izjednačila programe koji u određenom smislu računaju istu matematičku funkciju. Na primjer, sljedeća dva programa prema ovom se kriteriju smatraju jednakim:

funkcija Faktor (n: cijeli broj): cijeli broj započinje ako je n = 0, a Faktor: = 1; drugo Činjenica: = (n) * Faktororska (n -1); kraj;

1. program

funkcija Faktor (n: cijeli broj): cijeli broj var x, y: cijeli broj; započnite y: = 1; x: = 0; dok x <n započinje x: = x +1; y: = y * x; kraj Faktorski: = y; kraj;

2. program

S druge strane, operativniji prikaz koji upućuje na korake izračuna ne bi smatrao da su Program 1 i Program 2 jednaki. Doista, u svjetlu § 3.1., Možemo osmisliti semantičke račune koji odražavaju bilo koju razinu detalja o provedbi. Različiti semantički računi određuju različite pojmove jednakosti koji mogu poslužiti različitim konceptualnim i praktičnim ciljevima. Ali što onda treba poduzeti za određivanje jezika? Srećom, postoje neki desiderati koji se mogu primijeniti; možemo smanjiti mogućnosti: neki semantički računi pružaju nam logično zadovoljavajući pojam identiteta, a neki ne.

Indiscernibility od identicals je princip ugrađen u običnom predikat logika. Kaže da ako su dva objekta jednaka, tada dijele sva svojstva. Nasuprot principu, identitetu neupadljivogkaže da ako, za svako svojstvo F, objekt x ima F ako i samo ako objekt y ima F, tada je x identičan y. Identitet neupitnih podrazumijeva da ako su x i y različiti, onda postoji barem jedno svojstvo koje x ima, a y ne. Ponekad je spajanje oba principa poznato kao Leibnizov zakon (Forrest 2006). Za Leibnizov zakon često se smatra da je bitan za bilo koji pojam jednakosti. Ti su zakoni obično formulirani u logičkim teorijama, poput logike drugog reda. Ali najviše će nas zanimati njihova sposobnost razlikovanja različitih vrsta semantike programskog jezika. Zapravo je Leibnizov zakon jedan od središnjih pojmova moderne semantičke teorije. Kriterij identiteta izrađuje se u smislu promatračke ekvivalentnosti.

Dva programa M i N definirani su kao promatrački ekvivalentniako i samo ako je u svim kontekstima C […] gdje je C [M] valjani program, slučaj je da je C [N] također valjani program s istom semantičkom vrijednošću. Na primjer, kažemo da su Oracle i DB2 (programi koji manipuliraju relacijskim bazama podataka) promatrački ekvivalentni prema nekom semantičkom računu operacija na relacijskim bazama podataka ako i samo ako ih izvršavaju u „istom“kontekstu (operativni sustav, arhitektura stroja, unos itd.).) dobiva "istu" bazu podataka. Naravno, izraz promatrački ekvivalent potrebno je uzimati sa prstohvatom soli. Jasno ne možemo promatrati ponašanje programa u svim kontekstima. Međutim, promatračka ekvivalentnost odražava temeljni konceptualni zahtjev koji proizlazi iz načela neuništivosti identiteta i identiteta neupitnih.

U semantika, ako svi vidljivo različiti programi imaju različite semantičke vrijednosti, semantika se kaže zvukom. Prema tome, zvučna semantika zadovoljava sljedeći princip:

|| P || = || Q || podrazumijeva da za sve kontekste C, || C [P] || = || C [Q] ||

Treba biti jasno da pojam identiteta potaknut zvučnom semantikom zadovoljava neupitnost identiteta.

Kaže se da je semantika potpuna ako su bilo koja dva programa s izrazitim semantičkim vrijednostima vidljivo različita. Preciznije, kompletna semantika zadovoljava sljedeće:

Za sve kontekste C, || C [P] || = || C [Q] || podrazumijeva || P || = || Q ||

Opet, treba biti očito da cjelovita semantika zadovoljava načelo identiteta neupadljivog.

Konačno, za semantiku se kaže da je potpuno apstraktna ako je zvučna i cjelovita. Prema tome, potpuno apstraktna semantika zadovoljava Leibnizov zakon.

Ova logička pozadina pruža filozofsko opravdanje za razvoj potpuno apstraktne semantike. Tako nam nudi način izbora semantičkih računa koji pružaju filozofski prihvatljive pojmove jednakosti. To, naravno, ne određuje nijedan pojedinačni pojam. On pruža samo alat za odbacivanje onih koji ne mogu pružiti konceptualno prihvatljiv. Mnoge takozvane denotacijske semantike nisu u potpunosti apstraktne, dok su mnoge operativne. Doista, jedna od središnjih tema u novijoj povijesti semantike uključivala je potragu za potpuno apstraktnim definicijama koje se daju unutar klase semantičkih definicijskih tehnika koje su uzete za pružanje denotacijske semantike.

Semantika igra normativnu ili definirajuću ulogu u računarskoj znanosti. Bez semantičkih definicija, jezici i strukture nemaju sadržaje koji su iznad i sintaksičkih opisa. A ovo posljednje teško je dovoljno za praktične ili filozofske svrhe. Iako smo započeli s analizom središnjih pitanja, samo smo ogrebali površinu.

4. Dokazi i programi

Specifikacije (§2.3) potiču određeni pojam ispravnosti. Prema apstraktnom tumačenju ovog pojma, program se smatra ispravnim u odnosu na (funkcionalnu) specifikaciju ako odnos koji se nalazi između ulaza i izlaza zadovoljava onaj koji je utvrđen specifikacijom. Preciznije, ako je p program, tada ispunjava specifikaciju R, što se smatra odnosom prema ulaznom tipu I i izlaznom tipu O, ako vrijedi sljedeće:

Za sve ulaze, i tipa I, par (i, p (i)) zadovoljava odnos R

gdje je p (i) rezultat pokretanja programa p na ulazu i. Ovdje je R izražen u nekom jeziku specifikacije, a p u nekom programskom jeziku. Prva je obično neka varijanta (tipizirane) predikatne logike, a dokazi o ispravnosti (tj. Da je tvrdnja (1) pridržana) provode se u dokaznom sustavu logike. Na primjer, često se koristi Hoareova logika (Hoare 1969), u kojoj su dokazi o ispravnosti u obliku zaključaka između trojki, zapisanih

B {P} A

gdje je P program, a B i A su tvrdnje (stanja 'prije' i 'nakon' programa) izražene u nekoj verziji predikata logike sa značajkama koje olakšavaju izražavanje vrijednosti prikačenih programskim varijablama.

Jedna filozofska polemika koja okružuje pitanje ispravnosti usredotočuje se na prirodu takvih dokaza; drugi je izazov što pružaju takvi dokazi.

4.1 Dokazi iz informatike

Jesu li dokazi o ispravnosti programa stvarni matematički dokazi, odnosno, jesu li takvi dokazi usporedivi sa standardnim matematičkim? DeMillo i sur. (1979) tvrde da su dokazi o ispravnosti dugi i matematički plitki za razliku od dokaza iz matematike koji su konceptualno zanimljivi, uvjerljivi i privlače pažnju drugih matematičara koji ih žele proučavati i nadograditi. Primjerice, dokaz u Hoareovoj logici do te mjere da Program 2 izračunava faktorsku funkciju sadržavao bi detalje o temeljnom pojmu stanja, koristio bi induktivnu argumentaciju i uključivao razmišljanje o invaziji na petlju.

Ali takvi bi dokazi bili puno duži od samog programa. Nadalje, razina na kojoj je obrazloženje kodirano u Hoareovoj logici zahtijevala bi izražavanje i predstavljanje mnogih detalja koji bi obično ostali implicitni. Bilo bi to zamorno i, u slučaju većine programa, konceptualno trivijalno.

Ovaj argument paralelno je i s argumentima shvatljivosti iz filozofije matematike (npr. Tymoczko 1979; Burge 1988). U njegovom srcu su epistemološke brige: dokazi koji su predugi, nezgrapni i nezanimljivi ne mogu biti nositelji vrste sigurnosti koja se pripisuje standardnim matematičkim dokazima. Za prirodu znanja dobivenog dokazima o ispravnosti tvrdi se da se razlikuje od znanja koje se može dobiti iz dokaza iz matematike ^[1].

Također se mora razlikovati ta suštinski sociološka perspektiva dokaza o onom dokazu od one koja tvrdi da su dokazi ispravni ili pogrešni na način koji je neovisan o takvim epistemološkim prosudbama. Moguće je zadržati se realističnijeg stava prema kojem je svaki dati dokaz točan ili netočan bez odustajanja od zahtjeva koji dokazi trebaju biti razumljivi.

Moglo bi se pokušati steći osnova zalaganjem da dokaze o ispravnosti treba provjeriti računalo, a ne čovjek. Ali naravno provjerniku treba i sama provjera. Arkoudas i Bringsjord (2007) tvrde da ako postoji samo jedan dokaz ispravnosti koji treba provjeriti, naime onaj kod samog provjerenika dokaza, tada se mogućnost grešaka značajno smanjuje.

4.2 Dokazi iz matematike

Matematički dokazi poput dokaza Gödelove teoreme o nepotpunosti su također dugi i složeni. Ali ono što ih matematičkoj zajednici čini transparentnim, zanimljivim i razumljivim, jest upotreba tehnika modularnosti (npr. Lema) i upotreba apstrakcije u činu matematičkog stvaranja. Uvođenje novih pojmova omogućava da se dokaz konstruira postupno, što čini dokaze razumljivijim. Matematika napreduje izumom novih matematičkih koncepata koji omogućuju izgradnju više razine i općenitijih dokaza koji bi bili puno složeniji, pa čak i nemogući bez njih. Primjerice, notacija eksponenta omogućuje provođenje računanja izvan složenosti množenja i raspravljati se o rezultatima. S druge krajnosti,izum teorije kategorija olakšao je tvrdnju i dokaz vrlo općih rezultata o algebarskim strukturama koje se automatski primjenjuju na čitav niz takvih. Matematika se ne odnosi samo na dokaz; ona također uključuje apstrakciju i stvaranje novih koncepata i notacija. S obzirom na to, formalni dokazi o ispravnosti općenito ne koriste stvaranje novih koncepata niti se uključuju u proces matematičke apstrakcije. Suprotno tome, apstrakcija iz informatike (§ 6.1) koncentrirana je u pojmovima potrebnim za oblikovanje programa. Ali kako su ta dva pojma apstrakcije povezana? O tome ćemo malo više reći kasnije.ona također uključuje apstrakciju i stvaranje novih koncepata i notacija. S obzirom na to, formalni dokazi o ispravnosti općenito ne koriste stvaranje novih koncepata niti se uključuju u proces matematičke apstrakcije. Suprotno tome, apstrakcija iz informatike (§ 6.1) koncentrirana je u pojmovima potrebnim za oblikovanje programa. Ali kako su ta dva pojma apstrakcije povezana? O tome ćemo malo više reći kasnije.ona također uključuje apstrakciju i stvaranje novih koncepata i notacija. S obzirom na to, formalni dokazi o ispravnosti općenito ne koriste stvaranje novih koncepata niti se uključuju u proces matematičke apstrakcije. Suprotno tome, apstrakcija iz informatike (§ 6.1) koncentrirana je u pojmovima potrebnim za oblikovanje programa. Ali kako su ta dva pojma apstrakcije povezana? O tome ćemo malo više reći kasnije.

4.3. Fizička i apstraktna ispravnost

Čak i ako ostavimo po strani ove epistemološke brige, druga i naoko razorna kritika dokaza korektnosti dovodi u pitanje što ih je zapravo utvrdilo. Naizgled, dokaz ispravnosti pruža točnost samo do tekstualne reprezentacije programa. Nikakva količina formalnog rada ne može nas prijeći apstraktnu / fizičku barijeru: nikada ne možemo garantirati da će bilo kakva posebna izvedba programa na fizičkom stroju zapravo proći onako kako se očekuje (Fetzer 1988; Fetzer 1999; Colburn 2004).

Ali što znači da je program p točan? Pretpostavimo da imamo specifikaciju programa i da on može biti formalni ili neformalni. Zatim, pretpostavimo da provedemo niz pokusnih programa kako bismo provjerili da program ispunjava svoje specifikacije. Ako im uspije, imamo empirijske dokaze da je fizička slika tekstualnog programa doista ispravna jer djeluje prema specifikaciji. Prema ovom mišljenju, fizička se suprotnost ispitivala; a ne tekstualni program.

Ova analiza sugerira postojanje dualnosti u pojmu ispravnosti programa. U skladu s dualnom prirodom programa, mogli bismo reći da je tekstualni program podložan matematičkoj ispravnosti, dok je njegov fizički kolega podvrgnut empirijskoj provjeri.

5. Računalnost

Računarstvo je jedna od najstarijih tema koja se može označiti kao PCS. Međutim, tema je nekoliko unosa SEP-a (npr. Barker-Plummer 2004), pa ćemo spomenuti samo nekoliko tema i njihovih veza s ostatkom ovog unosa.

5.1 Teza crkve-Turing

Jedno od središnjih pitanja jest teza crkve-Turing. I ovdje postoje dva spora, jedan povijesni i jedan empirijski. Usredotočuju se na sljedeća dva moguća tumačenja teze:

1. Turingovi strojevi mogu učiniti sve što bi se moglo opisati kao "pravilo palca" ili "čisto mehaničko".
2. Turing što sve može izračunati stroj (rad na konačnim podacima u skladu s konačnim programom upute) je Turingovo strojno izračunato.

Tumačenje I ima za cilj da obuhvati pojam učinkovite ili mehaničke metode iz logike i matematike. Zamišljeno je da odražava neformalni pojam algoritma koji se podrazumijeva u matematici i koji je Hilbertov program izveo u prvi plan. Interpretacija II namijenjena je upravljanju fizičkim strojevima. Doista, (Gandy 1980) može se promatrati kao daljnje raspakiranje II. Gandy predlaže četiri načela koja su namijenjena karakterizaciji računanja pomoću fizičkog stroja. On pokazuje da se takvi strojevi točno slažu s Turingovom karakterizacijom (Gandijeva teorema). U vezi s našom raspravom o različitim semantičkim paradigmama, jasno je da se mnogi strojevi koji su u osnovi denotacijske semantike (§3.1) ne kvalificiraju kao Gandijevi strojevi. Najčešće djeluju s ekstenzijskim prostorom višeg reda,i to se ne može smatrati konačnim podacima i ne zadovoljavaju Gandijeve uvjete.

Neki tvrde (Copeland 2004; Copeland 2008) da se teza koju su predložili Church i Turing odnosi samo na interpretaciju I i da ne postavlja ograničenje za strojeve uopće. Hodges (2007) se ne slaže. Tvrdi da Church i Turing nisu razlikovali dvije interpretacije. Ovo je povijesni spor.

Fizički spor odnosi se na sposobnosti stvarnih strojeva (interpretacija II.) Mnogi shvaćaju zdravo za gotovo da teza Church-Turing karakterizira i propisuje stvarno fizičko računanje. Na primjer, čini se da je to implicitna pretpostavka u redovnoj računalnoj znanosti. Sigurno je da je svaki program napisan u postojećem implementiranom programskom jeziku Turingovim računalnim i obrnuto, da su svi programski jezici opće namjene cjeloviti, tj. Da sadrže sve upravljačke konstrukcije potrebne za simulaciju univerzalnog Turingovog stroja.

Copeland (2007) tvrdi da je Gandijeva karakterizacija diskretnog determiniranog mehaničkog uređaja preuska, te stoga postoje primjeri mogućih fizičkih strojeva čije mogućnosti nadilaze klasu računalnih funkcija Turinga. Mnogi od njih zahtijevaju beskonačno ubrzanje, pri čemu se može beskonačno mnogo računanja fizički obaviti u ograničenom vremenu. Kvantno računanje navodi se kao mogući primjer za takve strojeve, ali to je sporno (Hodges 2007; Hagar 2007).

Hodges se također bavi primjenom standardne matematičke argumentacije u fizici na onim slučajevima u kojima je uključena beskonačna preciznost. To sugerira da ovaj spor nije jednostavan empirijski. Doista, postoje oni koji se pitaju je li fizički moguće u beskonačnom vremenu izvršiti beskonačan broj zadataka. Dummett (2006) postavlja pitanje je li sam pojam beskonačnog zadatka koji se treba izvesti u fizičkom području nije samo fizička nemogućnost, već i konceptualna. Dakle, spor nije samo empirijski, već ide u središte našeg razumijevanja odnosa između naših matematičkih modela i fizičke stvarnosti.

6. Jezici programiranja i programiranja

Dizajn programa i programskih jezika jedna je od tradicionalnih aktivnosti informatike. Oko njih je okružen niz konceptualnih pitanja (§1), od kojih mnoga nisu dobila filozofsku pozornost. Ovdje ćemo ukratko razmotriti dva od ovih problema.

6.1 Apstrakcija

Apstrakcija je jedan od konceptualnih temelja informatike. Sastavni je dio dizajna i konstrukcije programa i čini jezgru metodologije za dizajn programskih jezika. Doista, to pokreće stvaranje novih programskih paradigmi. U osnovi je izum pojmova kao što su proceduralna i funkcionalna apstrakcija, polimorfizam, apstrakcija podataka, objekti i klase, obrasci dizajna, arhitektonski stilovi, podpisivanje i nasljeđivanje. Mnoge grane softverskog inženjerstva (npr. Modeliranje softvera, razumijevanje programa, vizualizacija programa, obrnuto i ponovno inženjering) primarno se bave istraživanjem odgovarajućih mehanizama za apstrakciju programa. Veliki dio napretka softverskog inženjeringa postignut je uvođenjem novih mehanizama apstrakcije.

Ali kakva je priroda apstrakcije u računarskoj znanosti? Koje je temeljno filozofsko objašnjenje? Nažalost, općenito, sama ideja apstrakcije filozofski je problematična. Prema tradicionalnom mišljenju, koje ima svoje podrijetlo u filozofskoj psihologiji, apstrakcija je mentalni proces u kojem se nove koncepcije formiraju razmatranjem nekoliko predmeta ili ideja i izostavljanjem obilježja koja ih razlikuju. (Rosen 2001). No, ovaj pristup ima malo, ako ih ima, suvremenih filozofskih zagovornika.

Logičniji pristup analizi apstrakcije koji ima snažno zagovaranje (Wright 1983; Hale 1987). Ali nejasno je jesu li te ideje, razvijene za matematičku apstrakciju, primjenjive na računalnu znanost. Jasno, neki pojmovi apstrakcije iz računarskih znanosti bili su ili nadahnuti ili su istraženi pomoću matematičkih apstrakcija. Kakav je konceptualni odnos između apstrakcije u tim disciplinama? Jesu li oni bitno različiti? Nažalost, iako postoji značajna literatura o filozofskim osnovama matematičke apstrakcije (vidi Wright 1983; Hale 1987; Fine 2002), konceptualno istraživanje apstrakcije u računalnoj znanosti tek je u povojima. Colburn (2007) sugerira da razlika između apstrakcije u matematici i apstrakcije u računarskoj znanosti leži u činjenici da je u matematici apstrakcija zanemarivanje informacija, dok se u računarskoj znanosti skriva informacija. Odnosno, matematičke apstrakcije zanemaruju ono što se ocjenjuje nevažnim (npr. Boja sličnih trokuta). Suprotno tome, u računalnoj znanosti, bilo koji od nižih razina (npr. Virtualna) ne smije zanemariti bilo koje detalje koji se zanemaruju na jednoj razini apstrakcije (npr. Java programeri ne moraju brinuti o točnom mjestu u memoriji povezanoj s određenom varijablom). stroj obrađuje sve dodjele memorije).apstrakcije u matematici zanemaruju ono što se smatra nebitnim (npr. boja sličnih trokuta). Suprotno tome, u računalnoj znanosti, bilo koji od nižih razina (npr. Virtualna) ne smije zanemariti bilo koje detalje koji se zanemaruju na jednoj razini apstrakcije (npr. Java programeri ne moraju brinuti o točnom mjestu u memoriji povezanoj s određenom varijablom). stroj obrađuje sve dodjele memorije).apstrakcije iz matematike zanemaruju ono što se ocjenjuje nevažnim (npr. boja sličnih trokuta). Suprotno tome, u računalnoj znanosti, bilo koji od nižih razina (npr. Virtualna) ne smije zanemariti bilo koje detalje koji se zanemaruju na jednoj razini apstrakcije (npr. Java programeri ne moraju brinuti o točnom mjestu u memoriji povezanoj s određenom varijablom). stroj obrađuje sve dodjele memorije).

No, je li to zasnovano na previše pojednostavljenom pojmu apstrakcije u matematici? Postoji li samo jedna vrsta pojma? Na primjer, podaci koji se kriju u Bishopovoj analizi (Bishop 1970) prilično su različiti od Wrightove pojma apstrakcije - doista, vrlo su slični računalnoj znanosti.

6.2 Vrste i ontologija

Programirani jezici su uglavnom tipkani jezici, pri čemu suvremeni pojam tipa potječe iz Fregea i Russella, a osobito iz Russell-ove jednostavne teorije tipova (Irvine 2003). Naravno, Russell je bio motiviran logičkim i semantičkim paradoksima i ta značajka nije središnja u primjeni vrsta u računalnoj znanosti. S druge strane, za Russelove vrste crta se svemir diskursa na načine koji imaju gramatički i semantički značaj. I ta se ideja prenijela na informatiku. Doista, teorije tipa nadahnute su i obogaćene računalnim znanostima. Na primjer, Russell-ova teorija tipova, premda matematički moćna, pomalo osiromašuje svoju ekspresivnu snagu u usporedbi s teorijama tipa modernih računalnih jezika (Coquand 2006; Pierce 2002). Osim niza osnovnih tipova kao što su brojevi i bulovi, programski jezici sadrže i zbirku konstruktora tipa (načini za izgradnju novih tipova od starih). Na primjer, one uključuju mogućnost stvaranja kartezijanskog proizvoda i konačnih skupova. U mnogim objektno programskim jezicima vrste (klase) mogu uvoziti (i nadjačati) operacije iz drugih vrsta i ponuditi sofisticiranije konstruktore koji podržavaju stvaranje apstraktnih tipova podataka i različitih oblika polimorfizma.vrste (klase) mogu uvoziti (i nadjačati) operacije iz drugih vrsta i ponuditi sofisticiranije konstruktore koji podržavaju stvaranje apstraktnih tipova podataka i različitih oblika polimorfizma.vrste (klase) mogu uvoziti (i nadjačati) operacije iz drugih vrsta i ponuditi sofisticiranije konstruktore koji podržavaju stvaranje apstraktnih tipova podataka i različitih oblika polimorfizma.

U računarskoj znanosti tipovi igraju ulogu koja je na pola puta između sintakse i semantike. Prvo, oni proširuju naše normalno poimanje gramatike bez konteksta. Neke jezične značajke, posebno one koje omogućuju fiksiranje vrste varijable kontekstom (tj. Deklaracije na jeziku), zahtijevaju gramatički oblik koji je fleksibilniji od standardnog. Takozvane gramatike na dvije razine, iako tehnički odgovarajuće, ne odražavaju način na koji se varijablama dodjeljuju njihove vrste u modernim jezicima. I vrlo su nespretni za korištenje. Ni oni se ne mogu lako prilagoditi sustavima polimorfnog tipa mnogih jezika. Moderni sustavi tipa rade bolje: varijablama se deklaracijama dodjeljuju njihove vrste, npr. X: Boolean. Nakon toga, prevoditelj može provjeriti program, npr.može osigurati pojavljivanje varijable u sljedećim izjavama (npr. x

Ali vrste igraju i ulogu ispravnosti koja se obično ne bi opisala sintaktičkim terminima. To se postiže proširivanjem tradicionalnog fizičkog pojma dimenzionalne analize na mnogo bogatiji sustav tipova. Dobijanje strukture odgovarajućeg tipa za program na neki način osigurava njegovu ispravnost. A to je određeno strukturom koju tipovi nameću jeziku. Vrste popravljaju sve vrste stvari u programskom jeziku. Tako, na primjer, svaki programski jezik koji priznaje brojeve, proizvode i klase i ništa drugo, programeru nameće konceptualni okvir unutar kojeg on mora raditi. Problemi se moraju artikulirati i rješenja se mogu naći u sredstvima reprezentacije koju pruža tip tipki. Nakon što je postavljena struktura tipa programskog jezika, popravljen je veći dio njegove ontološke postavke.

Ili ima? Možda se trebamo odmaknuti i prvo se pitati kako se određuju ontološke opredjeljenosti nekog jezika. Je li semantika ta koja određuje stvari (Turner i Eden 2007)? To bi sugerirala duga tradicija koja proizlazi iz Fregea (Dummett 1991). Ako pretpostavimo da je analogija s prirodnim jezicima legitimna, ontologiju jezika određuju strukture potrebne za pružanje njegovih semantičkih domena. Ali koju bi semantičku teoriju trebali usvojiti? Iako svaka semantika mora uzeti u obzir vrste, semantički određena ontologija nadišla bi ih izvan i odražavala uključene semantičke domene, a one bi odražavale detalje implementacije koji su uključeni u semantiku. Kao i kod jednakosti, različita semantička tumačenja određuju različite ontologije. Iz toga slijedi da nije smisleno govoriti o ontologiji programskog jezika, već o više ontologija koje ovise o razini apstrakcije uključene u semantiku. Na primjer, ontologija se također može djelomično odrediti paradigmom programiranja.

7. Pravna i etička pitanja

Neki problemi računalne etike pripadaju PCS- u jer aktivnost izgradnje i korištenja softvera postavlja etička pitanja. Međutim, mnogi nisu specifični za informatiku u užem smislu ovog unosa; oni utječu na cjelinu informacijskih tehnologija i računalnih aplikacija (Bynum 2001). Slijedom toga spomenut ćemo samo dva koja se čine središnjim za računalnu znanost.

7.1 Autorska prava, patenti i identitet

Autorska prava pružaju određenu zaštitu softveru, ali nisu u stanju zaštititi njegovu semantičku jezgru. I pretpostavljamo da ovo potonje treba odrediti semantičkim računom (§3) programskog jezika na kojem je program napisan. Vjerojatno se suština ovog pitanja tiče problema identiteta programa (§3.3). Ali ako postoji mnogo mogućih semantičkih pojmova identiteta, koji je prikladan za pravnu primjenu?

Jedan neformalni semantički račun koji se često navodi u zakonu identificira program s idejama koje su u njemu izražene, a najčešće se uzimaju kao temeljni algoritam. Ali ne samo da je često teško točno odrediti što je ovaj algoritam, već i to, kao što je slučaj s matematičkim teoremima, algoritmi ne mogu biti zaštićeni autorskim pravima. A ista takva sudbina čeka bilo koji formalni semantički račun, jer bi svaki takav bio određen nekim matematičkim pojmom, bilo da je riječ o algoritmima ili nekom pojmu djelovanja ili matematičke funkcije.

Ali čak i ako bismo uspjeli pronaći semantički račun koji bi bio usklađen sa zakonima o autorskim pravima, pravna slika ne bi bila potpuna. Povreda autorskih prava često ne ovisi samo o nekom identitetu, već io tome je li vjerojatno pretpostaviti da će netko pristupiti istom programu. Tako da namjerna razmatranja ulaze u okvir. Drugim riječima, čak i ako se dva programa smatraju jednakim prema našem semantičkom kriteriju, ako bi se moglo smatrati vjerojatnim da su izgrađeni neovisno, ne bi bilo kršenja autorskih prava.

Patenti (posebno korisni patenti) ne idu ništa bolje. Još je teže dobiti softver jer se ne mogu patentirati mentalni procesi, apstraktne ideje i algoritmi. A nove ideje često sadrže algoritmi a ne izvorni kod. Ali još jednom, upravo je pitanje identifikacije i identiteta središnje filozofsko pitanje. A to uključuje i semantička i namjerna razmatranja.

7.2 Ispravnost i odgovornost

Je li ispravno da se softver prodaje s malo jamstva prikladnosti za namjenu? (Coleman 2008) posvećen je ovom pitanju. Ovo je posebno važno pitanje za sigurnosno kritične sustave, npr. Sustave koji prate medicinske uvjete, upravljaju nuklearnim elektranama i komuniciraju s svemirskim šatlovima. Ovdje bi se činilo nužnim provođenje strožijih testiranja i dokaza ispravnosti. Ali etički gledano, je li slučaj programera koji ne analizira i testira svoj program različito od onog građevinskog inženjera koji ne izvrši traženo matematičko modeliranje i ispitivanja građevinskih konstrukcija? Moralne obveze izgledaju slično.

Jedan od načina na koji bi oni mogli biti različiti odnosi se na složenost softvera (Brooks 1987) koja prema stupnju veličine premašuje složenost bilo koje druge ljudske artefakte. Mnogi bi tvrdili da nije izvedivo jamstvo ispravnosti (DeMillo i sur. 1979); softver je toliko složen da je postupak rigoroznih matematičkih dokaza i testiranja softvera neizvediv. I, pretpostavljamo, čovjek može imati samo (moralnu ili pravnu) obvezu da provede izvedivi postupak.

No kako se uravnotežuju aspekti dokazivanja i testiranja razvoja softvera prema namjeravanoj upotrebi softvera? Bi li softver razvijen za zabavu trebao biti podvrgnut jednakom strogom dokazu i testiranju kao softver koji je kritičan za sigurnost? Vjerojatno ne, ali možda ćemo se i dalje zapitati jesu li to novi etički problemi ili nam oni samo pružaju daljnje studije slučaja postojećih etičkih dilema? Na primjer, čak i problemi u sigurnosti softvera koji se koristi u industriji zabave mogu financirati novčane kazne.

8. Novi zavoji ili nova izdanja?

Čak i ovaj prilično kratak pregled PCS-atrebali bi uvjeriti čitatelja da računalna znanost postavlja zanimljiva i zahtjevna filozofska pitanja. Zapravo, jedan od najvažnijih dojmova jest da ima značajne veze s većinom tradicionalnih grana filozofije. Postoje jasne veze s ontologijom, etikom, epistemologijom i filozofijama matematike, fizike i jezika. Zapravo, naš početni popis pitanja otvara mnogo više tema koje se povezuju s drugim područjima filozofije. Konkretno, postoji značajna literatura o primjenama informatike. Umjetna inteligencija i kognitivna znanost daju filozofska pitanja koja pripadaju filozofiji uma (McLaughlin 2004). Naravno, mnogo toga proizlazi iz Turinga (1950). Ostale primjene informatike u tradicionalnim područjima znanosti, tzv. Računarstvo,stvaraju pitanja za filozofiju znanosti: koji je epistemološki utjecaj računalnih simulacija, osobito tamo gdje su to jedini održivi oblik eksperimentiranja? Računalni zaokret u ontologiji donosi nove tehnike koje se odnose na strukturu bilo koje vrste konceptualne ontologije. Filozofija logike obogaćena je mnoštvom materijala: nastao je veliki broj novih logičkih sustava u svrhu reprezentacije i razmišljanja o računalnim sustavima.nastao je veliki broj novih logičkih sustava u svrhu reprezentacije i razmišljanja o računalnim sustavima.nastao je veliki broj novih logičkih sustava u svrhu reprezentacije i razmišljanja o računalnim sustavima.

Iako je jasno da računalna znanost izaziva mnoge značajne zaplete tradicionalnim filozofskim problemima, ono što je manje jasno je da li stvara bilo kakve istinski nove filozofske zabrinutosti: postoje li pitanja u PCS-u koja nemaju paralele u bilo kojoj drugoj grani filozofije?

Bibliografija

• Allison, A., Currall, J., Moss, M. i Stuart, S., 2005, "Pitanja digitalnog identiteta", Journal of American Society Information Science and Technology 56 (4): 364–372.
• Arkoudas, K. i Bringsjord, S., 2007, "Računala, opravdanje i matematičko znanje", Minds and Machines 17 (2): 185–202.
• Barendregt, HP, 1993, “Lambda izračunava s tipovima”, u: Priručnik logike u računalnoj znanosti, Vol. 2, New York, NY: Oxford University Press Inc.
• Barker-Plummer, D., 2008, "Turing Machines", Stanfordska enciklopedija filozofije (jesenje izdanje 2008), Edward N. Zalta (ur.), URL = ,
• Bishop, Errett, 1977., Temelji konstruktivne analize, McGraw-Hill.
• Blass, Andreas i Gurevich, Yuri, 2003., "Algoritmi: potraga za apsolutnim definicijama", Bilten Europskog udruženja za teorijske računalne znanosti (EATCS) br. 181: 195-225.
• Bowen, JP i Hinchey, MG, 1995, "Deset zapovijedi formalnih metoda", IEEE Computer 28 (4): 56–63.
• Bowen, JP i Hinchey, MG, 2005, "Deset zapovijedi formalnih metoda: deset godina kasnije", IEEE Computer 39 (1): 40–48.
• Brooks, FP, 1987, „Nema srebrnog metka: Suštine i nesreće softverskog inženjerstva“, IEEE Computer 20 (4): 10-19.
• Burge, T., 1998, „Računalni dokaz, priori znanje i drugi umovi“, Filozofske perspektive 12: 1–37.
• Bynum, T., 2001, "Računarna etika: osnovni pojmovi i povijesni pregled", Stanfordska enciklopedija filozofije (zima 2001. Izdanje), Edward N. Zalta (ur.), URL =
• Colburn, T., 2004., „Metodologija računarskih znanosti“, Blackwell vodič za filozofiju računarstva i informacija, Luciano Floridi (ur.), Malden: Blackwell, str. 318–326.
• Colburn, T., i Shute, G., 2007, “Apstrakcija u računarskim znanostima”, Minds and Machines 17 (2): 169-184.
• Coleman, KG, 2008, „Računarstvo i moralna odgovornost“, Stanfordska enciklopedija filozofije (jesenje izdanje 2008), Edward N. Zalta (ur.), URL = ,
• Copeland, B. Jack, 2008, "Teza o Turing Church-u", The Stanford Encyclopedia of Philosophy (Jesenje izdanje 2008), Edward N. Zalta (ur.), URL = ,
• Copeland, B. Jack, 2004, „Računanje“, Vodič za filozofiju računarstva i informacija u Blackwellu, Luciano Floridi (ur.), Malden: Blackwell, str. 3–17.
• Coquand, Thierry, 2006, "Teorija tipa", Stanfordska enciklopedija filozofije (zima 2006, izdanje), Edward N. Zalta (ur.), URL = ,
• DeMillo, RA, Lipton, RJ i Perlis, AJ, 1979, „Društveni procesi i dokazi teorema i programa“, Komunikacije ACM 22 (5): 271-280.
• Denning, PJ, 1980, "O narodnim teoremama i narodnim mitovima", Komunikacije ACM 23 (9): 493–494.
• Denning, PJ, 1980b, "Što je eksperimentalna informatika?" Komunikacije ACM 23 (10): 534–544.
• Denning, PJ, 1981., „Analiza performansi: Eksperimentalna informatika kao najbolja“, Komunikacije ACM 24 (11): 725–727.
• Denning, PJ, 1985., "Nauka o računarstvu: što je računalna znanost?" Američki znanstvenik 73 (1): 16-19.
• Denning, PJ (ur.), Et al., 1989, „Računanje kao disciplina“, Komunikacije ACM-a 32 (1): 9–23.
• Dijkstra, E., 1968., "Smatra se da je izjava štetna", priopćenja ACM 11 (3): 147–148.
• Dummett, M., 1991, "Logičke osnove metafizike", Harvard University Press.
• Dummett, M., 2006, "Misao i stvarnost", Oxford University Press.
• Eden, Amnon, 2007, "Tri paradigme u računalnoj znanosti", Minds and Machines 17 (2): 135-167.
• Feferman, S., 1992, „Logika ukidanja i ispravnosti funkcionalnih programa“, Logic for Computer Science: 95–127, MSRI Pubs. vol. 21, New York, NY: Springer-Verlag.
• Fetzer, JH, 1988., "Provjera programa: sama ideja", komunikacije ACM-a 31 (9): 1048–1063.
• Fetzer, JH, 1999, "Uloga modela u računarskoj znanosti", Monist 82 (1): 20–36.
• Fine, K., 2008, "Granice apstrakcije". Oxford: Oxford University Press.
• Floridi, Luciano, 2004. „Informacije“, Blackwell vodič za filozofiju računarstva i informacija, Luciano Floridi (ur.), Malden: Blackwell, str. 40–62.
• Floridi, Luciano 2007, "Semantički pojmovi informacija", Stanfordska enciklopedija filozofije (proljetno izdanje 2007), Edward N. Zalta (ur.), URL = ,
• Forrest, P., 2006, "Identitet neprimjetljivih", Stanfordska enciklopedija filozofije (jesenje izdanje 2008), Edward N. Zalta (ur.), Idući URL =. >.
• Fuchs, NE, 1992., „Specifikacije su (po mogućnosti) izvršljive“. Časopis za softverski inženjering 7 (5): 323–334.
• Gandy, R., 1980, "Crkvena teza i načela za mehanizme", The Kleene simpozij, Barwise, J., Keisler, HJ i Kunen, K. (ur.), Amsterdam: North-Holland.
• Hagar, Amit, 2007, „Kvantni algoritmi: filozofske lekcije“, uma i strojeva 17 (2): 233–247.
• Hale, B. i Wright, C., 2001, „Ispravna studija razuma: eseji o neo-fregeanskoj filozofiji matematike“, Oxford Scholarships on Line, Oxford: Oxford University Press.
• Hartmanis, J., 1993, „Neka zapažanja o prirodi računarskih znanosti“, Bilješke predavanja iz informatike 761, Shyamasundar, RK (ur.): 1–12.
• Hartmanis, J., 1994, „Turingovo nagradu za predavanje: O složenosti računara i prirodi računarskih znanosti“, Komunikacije ACM 37 (10): 37–43.
• Hoare, CAR, 1969, „Aksiomatska osnova za računalno programiranje“. Komunikacije ACM 12 (10): 576–585. [Ponovno tiskanje dostupno na mreži]
• Hodges, A., 2006, "Jesu li Crkva i Turing imali tezu o strojevima?", Crkvena teza nakon 70 godina Olszewski, Adam (ur.)
• Hodges, A., 2007, "Može li kvantno računanje riješiti klasično nerešive probleme?"
• Horsten, L., 2008, „Filozofija matematike“, Stanfordska enciklopedija filozofije (jesenje izdanje 2008), Edward N. Zalta (ur.), URL = ,
• Immerman, N., 2006, „Računalnost i složenost“, Stanfordska enciklopedija filozofije (jesenje izdanje 2006), Edward N. Zalta (ur.), URL = ,
• Irvine, AD, 2003., „Russell's Paradox“, Stanfordska enciklopedija filozofije (jesenje izdanje 2006), Edward N. Zalta (ur.), URL =
• Jones, CB i Hayes, IJ, 1990., „Specifikacije nisu (nužno) štetne“, Software Engineering Journal 4 (6): 330–339.
• Krishnamurthi, S., 2003. Programski jezici: primjena i tumačenje,
• Kreisel, G., Gandy, RO, 1975, „Neki razlozi za generaliziranje teorije rekurzije“. Časopis Simbolička logika 40 (2): 230–232.
• Kripke, S., 1982, Wittgenstein o pravilima i privatnom jeziku. Harvard University Press.
• Kuhn, TS, 1970, Struktura znanstvenih revolucija, 2. ed., Chicago: Univ. Chicago Pressa.
• Landin, PJ, 1964, "Mehanička procjena izraza", Computer Journal 6 (4): 308–320.
• Milne, R. i Strachey, C., 1977, A Theory of Programming Language Semantics, New York, NY: Halsted Press.
• McLaughlin, B., 2004, „Računanje, konekcionizam i filozofija uma“, Blackwell vodič za filozofiju računarstva i informacija, Floridi, Luciano (ur.) Malden: Blackwell, str. 135–152.
• Minsky, M., 1970, „predavanje o ACM-u Turing: Oblik i sadržaj u računarskoj znanosti“, časopis Asocijacije za računarske strojeve 17 (2): 197–215.
• Moor, JH, 1978., "Three Myths of Computer Science", Britanski časopis za filozofiju znanosti 29 (3): 213–222.
• Moschovakis, YN, 1998, „O utemeljenju teorije algoritama“, Istina u matematici Dales, Harold G. i Oliveri, Gianluigi (ur.), Oxford: Oxford University Press.
• Pierce, Benjamin C., 2002, Vrste i programski jezici, Cambridge, MA: MIT Press.
• Plotkin, GD, 1981., "Strukturalni pristup operativnoj semantika", Teh. Izaslanik DAIMI FN-19, odjel za računalne znanosti, Sveučilište Aarhus, Aarhus, Danska.
• Rapaport, WJ, 2005a, „Filozofija informatike: uvodni tečaj“, Podučavanje filozofije 28 (4): 319–341.
• Rapaport, WJ, 2005b, "Provedba je semantička interpretacija: daljnje misli." Časopis za eksperimentalnu i teorijsku umjetnu inteligenciju 17 (4): 385–417.
• Rosen, Gideon, 2001. „Abstraktni objekti“, Stanfordska enciklopedija filozofije (jesensko izdanje 2001), Edward N. Zalta (ur.), URL = ,
• Shapiro, S., 1997, Filozofija matematike: struktura i ontologija, Oxford: Oxford University Press.
• Sieg, Wilfried, 2008, „Crkva bez dogme: Aksiomi za računarstvo“, Nove računske paradigme, Lowe, B., Sorbi, A. i Cooper, B. (ur.), Springer-Verlag, 139–152.
• Smith, BC, 1996, "Granice ispravnosti u računalima", Informatizacija i kontroverza, Kling, R. (ur.), Morgan Kaufman, str. 810–825.
• Szabó, ZG, 2007, „Kompozicionizam“, Stanfordska enciklopedija filozofije (proljetno izdanje 2007), Edward N. Zalta (ur.), URL = ,
• Thomason, R., 2005., "Logika i umjetna inteligencija", Stanfordska enciklopedija filozofije (ljeto 2005), Edward N. Zalta (ur.), URL = ,
• Turner, Raymond i Eden, Amnon H., 2007, „Prema programskoj jezičnoj ontologiji“, računanje, informacije, kognicija - Nexus i zločinac, Dodig-Crnković, Gordana i Stuart, Susan (ur.), Cambridge, Velika Britanija: Cambridge Stipendisti Press, str. 147–159.
• Turner, Raymond, 2005, “Temelji specifikacije”, časopis za logično računanje 15: 623–662.
• Turner, Raymond, 2007, „Razumijevanje programskih jezika“. Um i strojevi 17 (2): 129-133
• Tymoczko, T., 1979, "Problem u četiri boje i njegov filozofski značaj", časopis za filozofiju 76 (2): 57–83.
• White, G., 2004, "Filozofija računalnih jezika", Blackwell vodič za filozofiju računarstva i informacija, Floridi, Luciano (ur.), Malden: Blackwell, str. 318–326.
• Wing, JM, 2006., "Računalno mišljenje", Komunikacije ACM-a, 49 (3): 33–35.
• Wittgenstein, L., 1953. Filozofska istraživanja. Blackwell Publishing.
• Wright, Crispin, 1983., Fregeova koncepcija brojeva kao objekata, Aberdeen University Press.

Ostali internetski resursi

• Filozofija računalnih znanosti na Sveučilištu Essex
• Međunarodno udruženje za računarstvo i filozofiju