Filosofin För Datavetenskap

Innehållsförteckning:

Filosofin För Datavetenskap
Filosofin För Datavetenskap

Video: Filosofin För Datavetenskap

Video: Filosofin För Datavetenskap
Video: Björn Johansson, Filosofiska fakulteten - Adjungerad professor i kognitionsvetenskap 2024, Mars
Anonim

Detta är en fil i arkiven för Stanford Encyclopedia of Philosophy. Författare & citatinformation | Vänner PDF-förhandsvisning | InPho Sök | PhilPapers bibliografi

Filosofin för datavetenskap

Först publicerad fredag 12 december 2008

Filosofin för datavetenskap (PCS)) är bekymrad över filosofiska frågor som uppstår genom reflektion över arten och praktiken inom datavetenskapens akademiska disciplin. Men vad är det senare? Det är verkligen inte bara programmering. När allt kommer omkring är många som skriver program inte datavetare. Till exempel gör fysiker, revisorer och kemister. I själva verket skulle datavetenskap beskrivas bättre som att det handlar om metaaktiviteten som är associerad med programmering. Mer generellt, och mer exakt, är det upptaget med utformning, utveckling och utredning av koncept och metoder som underlättar och hjälper till att specificera, utveckla, implementera och analysera beräkningssystem. Exempel på denna aktivitet kan inkludera design och analys av programmeringsspråk, specifikationer och arkitektoniska beskrivningsspråk;konstruktion och optimering av kompilatorer, tolkar, teoremprovrar och typinferenssystem; uppfinningen av logiska ramverk och utformningen av inbäddade system, och mycket mer. Många av de centrala filosofiska frågorna inom datavetenskap omger och underbygger dessa aktiviteter, och många av dem är inriktade på de logiska, ontologiska och epistemologiska frågor som berör den. Men i slutändan är datavetenskap vad datavetare gör, och ingen exakt formel definition kan fungera som mer än en guide till diskussionen som följer. Hoppet är verkligen detMånga av de centrala filosofiska frågorna inom datavetenskap omger och underbygger dessa aktiviteter, och många av dem är inriktade på de logiska, ontologiska och epistemologiska frågor som berör den. Men i slutändan är datavetenskap vad datavetare gör, och ingen exakt formel definition kan fungera som mer än en guide till diskussionen som följer. Hoppet är verkligen detMånga av de centrala filosofiska frågorna inom datavetenskap omger och underbygger dessa aktiviteter, och många av dem är inriktade på de logiska, ontologiska och epistemologiska frågor som berör den. Men i slutändan är datavetenskap vad datavetare gör, och ingen exakt formel definition kan fungera som mer än en guide till diskussionen som följer. Hoppet är verkligen det PCS kommer så småningom att bidra till en djupare förståelse av datavetenskapens natur.

Men att kartlägga det filosofiska landskapet inom datavetenskap är ingen lätt uppgift. Lyckligtvis kan traditionella filialfilialer ge intellektuell och strukturell vägledning. I filosofierna för matematik och fysik finns det till exempel centrala frågor om arten av de objekt som behandlas, vad som utgör kunskap och sättet att få kunskapen. Språkfilosofin ställer frågor om innehållet och formen av en semantisk teori för naturligt språk. Det ger upphov till de underliggande ontologiska och epistemologiska antagandena från det semantiska företaget. Ontologi indikerar vilka saker det finns, hur man kan individualisera dem och deras roll för att utforma våra konceptuella scheman. Logikfilosofin ger en redogörelse för och analys av olika typer av logiska system och deras roll i vardagliga och specialiserade diskurser. Analogier och likheter från dessa och andra filosofiska grenar bör vara användbara för att identifiera och klargöra några av de centrala filosofiska frågorna inom datavetenskap. Det befintliga inflytandet av dessa discipliner på PCS kommer att dyka upp när vi fortsätter. I synnerhet återspeglar den andra, tredje och fjärde delen effekterna av ontologi och språk och matematikens filosofier.

  • 1. Vissa centrala frågor
  • 2. Existens och identitet

    • 2.1 Programmens dubbla karaktär
    • 2.2 Program och algoritmer
    • 2.3 Program och specifikationer
  • 3. Semantik

    • 3.1 Denotations- och operationell semantik
    • 3.2 Implementering och semantisk tolkning
    • 3.3 Semantik, jämställdhet och identitet
  • 4. Bevis och program

    • 4.1 Bevis inom datavetenskap
    • 4.2 Bevis i matematik
    • 4.3 Fysisk och abstrakt korrekthet
  • 5. Beräknbarhet

    5.1 The Church-Turing Thesis

  • 6. Programmering och programmeringsspråk

    • 6.1 Abstraktion
    • 6.2 Typer och ontologi
  • 7. Juridiska och etiska frågor

    • 7.1 Upphovsrätt, patent och identitet
    • 7.2 Korrekthet och ansvar
  • 8. Nya vändningar eller nya problem?
  • Bibliografi
  • Andra internetresurser
  • Relaterade poster

1. Vissa centrala frågor

Till att börja med ska vi räkna upp vad vi tar för att vara några av de centrala frågorna och frågorna. Detta ger läsaren en snabb översikt över frågor som kommer att komplettera den mer detaljerade diskussionen som kommer. Även om många av dem inte har behandlats direkt i litteraturen och har behov av en förtydligande, illustrerar dessa frågor de typer av problem som vi tar upp PCS- uppgifterna.

  1. Vilka saker är program? Är de abstrakta eller konkreta? (Moor 1978; Colburn 2004)
  2. Vilka är skillnaderna mellan program och algoritmer? (Rapaport 2005a)
  3. Vad är en specifikation? Och vad anges? (Smith 1985; Turner 2005)
  4. Är specifikationerna väsentligt olika från program? (Smith 1985)
  5. Vad är en implementering? (Rapaport 2005b)
  6. Vad skiljer hårdvara från programvara? Finns program i både fysiska och symboliska former? (Moor 1978; Colburn 2004)
  7. Vilka saker är digitala objekt? Behöver vi en ny ontologisk kategori för att hysa dem? (Allison et al. 2005)
  8. Vilka är målen för de olika semantiska teorierna om programmeringsspråk? (White 2004; Turner 2007)
  9. Hur relaterar frågor i filosofin om programmeringsspråk till parallella frågor i språkfilosofin? (White 2004)
  10. Relaterar principen om modularitet (t.ex. Dijkstra 1968) de konceptuella frågorna om full abstraktion och kompositionitet?
  11. Vilka är de bakomliggande konceptuella skillnaderna mellan följande programmeringsparadigmer: strukturerad, funktionell, logisk och objektorienterad programmering?
  12. Vilka roller har typerna inom datavetenskap? (Barandregt 1992; Pierce 2002)
  13. Vad är skillnaden mellan operationell och denotational semantik? (Turner 2007)
  14. Vad betyder det för ett program att vara korrekt? Vad är den epistemologiska statusen för korrekthetsbevis? Är de i grunden olika från bevis i matematik? (DeMillo et al. 1979; Smith 1985)
  15. Vad uppvisar korrekt bevis? (Fetzer 1988; Fetzer 1999; Colburn 2004)
  16. Vad är abstraktion inom datavetenskap? Hur är det relaterat till abstraktion i matematik? (Colburn & Shute 2007; Fine 2008; Hale & Wright 2001)
  17. Vad är formella metoder? Vad är formellt med formella metoder? Vad är skillnaden mellan en formell och informell metod? (Bowen & Hinchey 2005; Bowen & Hinchey 1995)
  18. Vilken typ av disciplin är datavetenskap? Vilka roller har matematisk modellering och experiment? (Minsky 1970; Denning 1980; Denning 1981; Denning et al. 1989; Denning 1985; Denning 1980b; Hartmanis 1994; Hartmanis1993; Hartmanis 1981; Colburn 2004; Eden 2007)
  19. Bör program betraktas som vetenskapliga teorier? (Rapaport 2005a)
  20. Hur används matematik i datavetenskap? Används matematiska modeller på ett beskrivande eller normativt sätt? (White 2004; Turner 2007)
  21. Fångar Church-Turing-avhandlingen den matematiska uppfattningen om en effektiv eller mekanisk metod i logik och matematik? Fångar det de beräkningar som kan utföras av en människa? Går dess tillämpningsområde för fysiska maskiner? (Copeland 2004; Copeland 2007; Hodges 2006)
  22. Kan begreppet beräkningstänkande motstå filosofisk granskning? (Wing 2006)
  23. Vad är lämplig logik för att resonera om programmets korrekthet och avslutning? (Hoare 1969; Feferman 1992) Hur är logiken beroende av det underliggande programmeringsspråket?
  24. Vad är information? (Floridi 2004; Floridi 2005) Kasta denna uppfattning ljus på några av de frågor som listas här?
  25. Varför finns det så många programmeringsspråk och programmeringsparadigmer? (Krishnamurthi 2003)
  26. Har programmeringsspråk (och paradigmer) karaktären av vetenskapliga teorier? Vad orsakar ett programmeringsparadigmskifte? (Kuhn 1970)
  27. Har programvaruteknik tagit upp några filosofiska problem? (Eden 2007)

I det följande kommer vi att lägga lite kött på några av dessa frågor.

2. Existens och identitet

Hur kategoriserar och individualiserar vi datavetenskapens enheter och begrepp? Vilka saker är de och vad bestämmer deras identitet? Till exempel är vissa tydligt konkreta fysiska föremål (t.ex. chips, routrar, bärbara datorer, grafikkort) och andra inte (t.ex. formella grammatik, abstrakta maskiner, teorem provers, logiska ramar, processalgebraer, abstrakta datatyper). Men karaktäriseringen av några av de centrala uppfattningarna som program och data har varit mer problematisk. I synnerhet har programmenas ontologiska status inte tagits vara helt okomplicerad och inte heller frågan om deras identitetskriterier.

2.1 Programmens dubbla karaktär

Många författare (Moor 1978; Rapaport 2005b; Colburn 2004) diskuterar programmets så kallade dubbla karaktär. På det sättet verkar ett program ha både en textuell och en mekanisk eller processliknande förknippning. Som text kan ett program redigeras. Men dess manifestation på en maskinläsbar disk verkar ha helt olika egenskaper. I synnerhet kan det köras på en fysisk maskin. Så enligt principen om identitetens oskiljbarhet (§3.3), kan de två väskorna inte vara samma enhet. Naturligtvis, alla som övertalas av denna dualitet är skyldiga att säga något om förhållandet mellan dessa två uppenbara former av existens.

Ett omedelbart förslag är att den ena manifestationen av ett program är en implementering av den andra, dvs. den fysiska manifestationen är en implementering av det textuella. Även inom datavetenskapens gränser är det emellertid inte direkt klart att ordimplementeringen bara hänvisar till en idé. Ofta används det för att hänvisa till resultatet av en sammanställningsprocess där ett program på ett högnivåspråk (källkoden) omvandlas till maskinspråk (objektkoden). Men lika ofta används det för att referera till processen där källkoden på något sätt direkt realiseras i hårdvara (t.ex. en konkret implementering i halvledare). Och förmodligen är detta den relevanta uppfattningen. Men utan en mer detaljerad filosofisk analys av själva uppfattningen om genomförande (§3.2) (Rapaport 2005b),det är oklart hur detta främjar diskussionen; vi verkar bara ha namngivit förhållandet mellan de två uppenbara formerna av existens. På liknande sätt har andra beskrivit förhållandet mellan programtexten och programprocessen som liknar den mellan en plan och dess manifestation som en serie fysiska handlingar. Men detta verkar inte vara riktigt analogt med programprocessparningen: vi frestas inte att hänvisa till planen och den fysiska processen som olika manifestationer av samma sak. Till exempel frestas vi att tänka på en plan för att gå en promenad och själva promenad som olika aspekter av samma sak?andra har beskrivit förhållandet mellan programtexten och programprocessen som liknar den mellan en plan och dess manifestation som en serie fysiska handlingar. Men detta verkar inte vara riktigt analogt med programprocessparningen: vi frestas inte att hänvisa till planen och den fysiska processen som olika manifestationer av samma sak. Till exempel frestas vi att tänka på en plan för att gå en promenad och själva promenad som olika aspekter av samma sak?andra har beskrivit förhållandet mellan programtexten och programprocessen som liknar den mellan en plan och dess manifestation som en serie fysiska handlingar. Men detta verkar inte vara riktigt analogt med programprocessparningen: vi frestas inte att hänvisa till planen och den fysiska processen som olika manifestationer av samma sak. Till exempel frestas vi att tänka på en plan att gå en promenad och själva promenad som olika aspekter av samma sak?är vi frestade att tänka på en plan att gå en promenad och den faktiska promenad som olika aspekter av samma sak?är vi frestade att tänka på en plan att gå en promenad och den faktiska promenad som olika aspekter av samma sak?

Kanske beskrivs frågor bäst genom att säga att program, som textobjekt, orsakar mekaniska processer? Tanken verkar vara att textobjektet på något sätt orsakar den mekaniska processen. Men detta verkar kräva någon ganska noggrann analys av arten av en sådan orsakssamband. Colburn (2004) förnekar att den symboliska texten har kausal effekt. det är dess fysiska manifestation (saken på disken) som har en sådan effekt. Programvara är en konkret abstraktion som har ett beskrivningsmedium (texten, abstraktionen) och ett exekveringsmedium (t.ex. en konkret implementering i halvledare).

Ett något annat perspektiv på dessa frågor börjar med frågan om programidentitet. När ska två program vara samma? Sådana problem uppstår till exempel i försök att bestämma den juridiska identiteten för en mjukvara. Om vi identifierar ett program med dess textliga manifestation är programmets identitet känslig för förändringar i dess utseende (t.ex. att ändra teckensnitt). Uppenbarligen är det inte texten ensam som ger oss någon filosofiskt intressant uppfattning om programidentitet. Snarare måste vi ta mer hänsyn till semantik och implementering för att nå ett informerat kriterium om identitet. Vi kommer tillbaka till detta ämne i §3 och §6.

2.2 Program och algoritmer

Oavsett vilken syn vi ser på program, är algoritm-programskillnaden också i behov av ytterligare begreppsförklaring. Algoritmer anses ofta vara matematiska objekt. Om detta är sant tillhör många av de filosofiska frågor som rör dem också till matematikfilosofin. Men algoritmer är utan tvekan mer centrala för datavetenskap än för matematik och förtjänar mer filosofisk uppmärksamhet än de har givits. Även om det har gjorts någon betydande matematisk studie av algoritmer inom teoretisk datavetenskap och matematisk logik (t.ex. Moschovakis 1997; Blass & Gurevich 2003) har det inte varit mycket filosofisk diskussion som är inriktad på algoritmernas karaktär och skillnaderna mellan algoritmer och program.

Är det så att algoritmer är abstrakta objekt i den mening som Rosen (2001) erbjuder, medan program är konkreta? Mer exakt, är algoritmer den abstrakta matematiska motsvarigheten till ett textobjekt som är programmet? Denna bild lämnar sig naturligtvis till en form av ontologisk platonism (Shapiro 1997) där algoritmer har ontologisk prioritering och program ger de språkliga sätten att komma åt dem. I denna vy kan algoritmer tas för att tillhandahålla semantik (§3) för programmeringsspråk. Naturligtvis ärver denna bild alla fördelar och problem med ett sådant platoniskt perspektiv (Shapiro 1997).

En mindre plattonisk uppfattning har att algoritmer innehåller de idéer som uttrycks i ett program. I lag har detta ansetts vara orsaken till att algoritmer, i motsats till program, inte är upphovsrättsskyddiga (§7.1). Naturligtvis kräver begreppet idé ytterligare filosofisk analys. I själva verket kan man hävda att den nakna uppfattningen om algoritm är i mycket mindre behov av förtydligande än standardrapporten för idéer och dess tillhörande uppfattningar om abstraktion (Rosen 2001).

Slutligen är det nästan en folklorisk uppfattning att Turing-maskiner ger oss en formell analys av vår uppfattning om algoritm. Men passar detta den samtida uppfattningen som används i modern datavetenskap med dess sofistikerade föreställningar och kontroll? Moschovakis (1997) erbjuder en analys som gör något bättre.

2.3 Program och specifikationer

En annan populär åtskillnad som borde vara föremål för en viss kritisk analys uppstår med avseende på program och specifikationer. Vad är specifikationer och hur skiljer de sig från program? Det finns lite direkt diskussion om denna fråga i den filosofiska litteraturen (men se Smith 1985), men specifikationerna är en grundläggande fråga för datorvetenskapens begreppsmässiga grund.

En uppfattning, vanligtvis finns i läroböcker om formell specifikation, är att program innehåller detaljerade maskininstruktioner medan (funktionella) specifikationer endast beskriver förhållandet mellan ingång och utgång. Ett uppenbart sätt att packa upp detta är i termer av den nödvändiga / beskrivande distinktionen: program är nödvändiga och beskriver hur man kan uppnå det mål som beskrivs i specifikationen. Visst, i det nödvändiga programmeringsparadigmet verkar detta fånga en väsentlig skillnad. Men det är inte lämpligt för alla. Till exempel styrs logiska, funktionella och objektorienterade programmeringsspråk inte uppenbart av det: tagna till nominellt värde, program som är kodade på sådana språk består av sekvenser av definitioner, inte "instruktioner". Dessutom,icke-funktionella specifikationer kan inte formuleras som uttalanden om förhållandet mellan ingång och utgång eftersom de ställer krav på designen och på vilken typ av instruktioner som kan ingå i något program.

En annan åsikt insisterar på att skillnaden mellan specifikationer och program ska lokaliseras när det gäller begreppet implementering, dvs. kan det sammanställas och köras? Men vad menas med det? Menas det i den meningen att det finns en befintlig kompilator? Denna tolkning är ganska grunt eftersom den inte erbjuder ett begreppsmässigt kriterium för skillnad utan en kontingent. Under de första fem generationerna av programmeringsspråk (andra halvan av 1900-talet) har till exempel rekursiva, modulära, funktionella och objektorienterade specifikationer för en generation kommit att formuleras som program i nästa, dvs. dagens specifikationsspråk blir ofta morgondagens programmeringsspråk.

En annan åsikt antyder att programmeringsspråk är de språk som har en implementering i princip medan specifikationsspråk är de som inte kan. Och förmodligen är anledningen till att de inte kan vara att specifikationsspråk tillåter en att uttrycka föreställningar som inte är Turing beräkningsbara. Denna distinktion överensstämmer med många befintliga specifikationsspråk som är baserade på Zermelo-Fraenkel-uppsättningsteori och högre ordningslogik. Det verkar dock konstigt att det som ska känneteckna ett specifikationsspråk är det faktum att det kan uttrycka icke-beräknbara egenskaper och relationer. Är några av dessa icke beräknbara krav verkligen nödvändiga i praktiken (Jones & Hayes 1990; Fuchs 1994)?

Mångfalden i dessa åsikter antyder att den traditionella, binära skillnaden mellan specifikationer och program är ett exempel på ett problem i PCS som förtjänar mer uppmärksamhet, inte bara för konceptuell förtydligande utan också för att det kan ha konsekvenser för utformningen av framtida programmerings- och specifikationsspråk..

3. Semantik

Grammatiken för ett programmeringsspråk avgör endast vad som är syntaktiskt legitimt; den informerar inte om den avsedda betydelsen av dess konstruktioner. Således bestämmer grammatiken i ett programmeringsspråk inte i sig det som folk programmerar i. I stället är det grammatiken berikad med ett semantiskt konto (formellt eller informellt) som tas för att göra det. Semantiken är tänkt att informera programmeraren, kompilatören och teoretikern som är intresserad av att utforska språkets egenskaper. Det hävdas ofta att för att uppfylla de olika kraven hos programmeraren och kompilatören krävs olika semantiska konton, på olika nivåer av abstraktion. Och teoretikerens uppgift är att utforska deras relation.

Detta är standardbilden som framträder i den semantiska litteraturen. Men mycket av detta är i behov av begreppsmässig förtydligning. I det här avsnittet behandlar vi bara några av de problem som uppstår genom denna aktivitet.

3.1 Denotations- och operationell semantik

En av de viktigaste distinktionerna i programmeringsspråk semantik bygger på skillnaden mellan operationell och denotational semantik. En operationell semantik (Landin 1964; Plotkin 1981) ger en tolkning av ett programmeringsspråk i termer av någon abstrakt maskin. Mer exakt är det en översättning av uttryck på programmeringsspråket till instruktionerna eller programmen på den abstrakta maskinen. Till exempel skulle program 1 packas upp i en sekvens av abstrakta maskindrift som "a ← 0" och tryck. Operativ semantik kan också tolkas som algoritmisk semantik, särskilt när den underliggande maskinen syftar till att karakterisera själva uppfattningen om algoritm (t.ex. Moschovakis 1997).

Däremot ger en denotational semantik (Milne & Strachey 1977) en tolkning i matematiska strukturer såsom uppsättningar eller kategorier. Till exempel, i den klassiska metoden, ger uppsättningar i form av kompletta gitter och kontinuerliga funktioner på dem det matematiska ramverket.

Men finns det någon betydande begreppsmässig skillnad mellan dem? Är det så att denotationssemantik, som uttryckligen bygger på matematiska strukturer som uppsättningar, är matematisk medan operativ semantik inte är det? Turner (2007) hävdar inte: de ger alla matematiska tolkningar.

Eller är det så att operationell semantik är mer maskinliknande, i den meningen att den utgör en abstrakt maskin, medan det med denotationssemantik, som ges i setteoretiska termer, inte finns någon antydan till en abstrakt maskin? Sådana distinktioner har emellertid inte visat sig begreppsmässigt betydelsefulla eftersom denotationella semantiska konton alla kan ses som strukturer som utgör en abstrakt maskin med tillstånd och operationer som verkar på dem. Operativa konton är inte heller närmare implementeringen: denotationsstrategier (Milne & Strachey 1977) är också mycket flexibla och kan återspegla olika implementeringsnivåer.

En annan möjlig åtskillnad avser semantikens sammansättning (eller på annat sätt). Löst sett anses en semantik vara sammansatt (Szabó 2007) om det semantiska värdet för ett komplex uttryck är en funktion av de semantiska värdena för dess delar. Kompositionitet anses vara ett avgörande kriterium för semantik eftersom det verkar krävas för att förklara produktiviteten i vår språkliga förståelse: det sägs förklara hur vi förstår och konstruerar komplexa program. Men ger det oss en kil för att separera operationell och denotational semantik? Tyvärr verkar det inte göra det: medan denotationsdefinitioner är utformade för att vara sammansatta är det verkligen inte så att all operationell semantik inte är sammansatt.

Slutligen skiljer sig vissa versioner av semantik om förekomsten av en rekursiv modell, dvs. en tolkning i Turing-maskiner eller Gandy-maskiner (§5.1). Men även detta stämmer inte exakt med den traditionella klyftan om operationell / denotation. Vissa denotationsdefinitioner har en rekursiv modell och andra inte.

Det verkar mycket svårt att fastställa denna distinktion. I motsats till detta verkar det inte finnas någon skarp konceptuell åtskillnad mellan operationell och denotational semantik.

3.2 Implementering och semantisk tolkning

Vad är skillnaden mellan en semantisk tolkning och en implementering? Till exempel, vad är den begreppsmässiga skillnaden mellan att sammanställa ett program till maskinkod och att ge det en denotational semantik? Enligt Rapaport (2005b) ses en implementering bäst som semantisk tolkning, där den senare kännetecknas av en kartläggning mellan två domäner: en syntaktisk och en semantisk. Och båda bestäms av regler i någon beskrivning. Till exempel är den sammanställda koden (i kombination med reglerna som styr dess semantik) det semantiska kontot för källkoden.

I en gemensam förståelse av termen "implementering" tillhandahålls den semantiska domänen av en fysisk maskin. Med andra ord, den fysiska maskinen själv ("implementeringen") avgör vad programmet betyder. I programmeringsspråk motsvarar det till exempel påståendet att semantiken för programmeringsspråket C ++ bestäms av Bjarnes dator som kör sin C ++ -kompilerare. Men denna förklaring är uppenbarligen otillräcklig: Om vi antar att Bjarnes maskin bestämmer innebörden av C ++ -program så finns det inget begrepp om fel eller tolkning: vad Bjarnes dator gör är, ipso facto, programmets betydelse. Men säkert kan en elektrisk storm orsaka att maskinen går fel. Men vad kan vi mena med att gå fel? Antagligen att den (felaktiga) maskinen inte innehåller den avsedda betydelsen. Men,i sin tur verkar vi bara kunna förstå denna fras utifrån någon maskinoberoende karaktärisering av meningen. Och på någon nivå måste detta ges via någon oberoende semantisk beskrivning. Detta antyder att föreställningen om bara implementering inte erbjuder ett adekvat begrepp av semantik. (Jämför med: Kripke 1982; Wittgenstein 1953).

3.3 Semantik, jämställdhet och identitet

Vi avslutade vår diskussion om programjämlikhet (§2.1) med ett löfte om att få semantik in i bilden. Varje semantisk redogörelse för ett programmeringsspråk bestämmer en uppfattning om jämlikhet för program, nämligen att två program anses vara lika om de har samma semantiska värde, dvs.

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

där || P || är det semantiska värdet för programmet P. Så i denna mening bestämmer varje semantisk berättelse ett kriterium om jämlikhet. Till exempel skulle en version av denotational semantik abstrahera bort från alla beräkningssteg och jämställa program som i någon mening beräknar samma matematiska funktion. Till exempel skulle följande två program anses vara lika med detta kriterium:

funktion Factorial (n: heltal): heltal

börjar

om n = 0

sedan Factorial: = 1;

annat

Factorial: = (n) * Factorial (n -1);

slutet;

Program 1

funktion Factorial (n: heltal): heltal

var

x, y: heltal;

börja

y: = 1;

x: = 0;

medan x <n börjar

x: = x +1;

y: = y * x;

slutet

Faktoriell: = y;

slutet;

Program 2

Å andra sidan skulle en mer operativ vy, som hänvisar till beräkningsstegen, inte göra att program 1 och program 2 skulle vara lika. I ljuset av §3.1 kan vi faktiskt utforma semantiska konton som återspeglar alla detaljer för implementeringen. Olika semantiska beräkningar bestämmer olika begrepp om jämlikhet som kan tjäna olika konceptuella och praktiska syften. Men vilken bör då tas för att bestämma språket? Lyckligtvis finns det några desiderata som kan tillämpas; vi kan skära ner alternativen: vissa semantiska konton ger oss en logiskt tillfredsställande uppfattning om identitet och andra inte.

Den indiscernibility av identicals är en princip som är inbyggd i vanlig predikatlogik. Den säger att om två objekt är lika delar de alla egenskaper. Den omvända principen, identiteten på oskiljaktighetersäger att om för varje egenskap F, objekt x har F om och bara om objekt y har F, så är x identiskt med y. Oskiljaktigheters identitet innebär att om x och y är olika, så finns det åtminstone en egenskap som x har och y inte. Ibland är kopplingen av båda principerna känd som Leibniz's Law (Forrest 2006). Leibnizs lag anses ofta vara väsentlig för varje begrepp om jämlikhet. Dessa lagar formuleras vanligtvis i logiska teorier såsom andra ordningens logik. Men vi ska vara mest intresserade av deras förmåga att skilja mellan olika typer av programmeringsspråk semantik. I själva verket är Leibniz 'lag en av de centrala uppfattningarna i modern semantisk teori. Kriteriet om identitet utarbetas när det gäller observationsekvivalens.

Två program M och N definieras vara observatoriskt likvärdigaom och bara om, i alla sammanhang C […] där C [M] är ett giltigt program, är det så att C [N] också är ett giltigt program med samma semantiska värde. Vi säger till exempel att Oracle och DB2 (program som manipulerar relationella databaser) är observativt likvärdiga enligt en viss semantisk redogörelse för operationer på relationsdatabaser om och bara om de körs i "samma" sammanhang (operativsystem, maskinarkitektur, input etc.) ger "samma" databas. Naturligtvis måste termen observationsekvivalent tas med en nypa salt. Vi kan tydligt inte observera ett programs beteende i alla sammanhang. Observationsekvivalens återspeglar emellertid ett underliggande begreppsmässigt krav som härrör från principerna om oskiljaktighet för identiska och från identiteten hos oskiljbara.

I semantik, om alla observerbart distinkta program har distinkta semantiska värden, sägs semantiken vara sund. Följaktligen uppfyller en sund semantik följande princip:

|| P || = || Q || innebär att för alla sammanhang C, || C [P] || = || C [Q] ||

Det borde vara tydligt att idén om identitet som framkallas av en sund semantik uppfyller identitetens oskiljaktighet.

En semantik sägs vara fullständig om två program med distinkta semantiska värden är påtagligt distinkta. Mer exakt uppfyller en komplett semantik följande:

För alla sammanhang C, || C [P] || = || C [Q] || antyder || P || = || Q ||

Återigen bör det vara uppenbart att en fullständig semantik uppfyller principen om identitet för oskiljaktigheter.

Slutligen sägs semantik vara helt abstrakt om den är sund och fullständig. Följaktligen uppfyller en helt abstrakt semantik Leibnizs lag.

Denna logiska bakgrund ger den filosofiska motiveringen för utvecklingen av helt abstrakt semantik. Det ger oss därför ett sätt att välja semantiska konton som ger filosofiskt godtagbara föreställningar om jämlikhet. Det avgör naturligtvis inte någon enda uppfattning. Den ger bara ett verktyg för att avvisa de som inte kan leverera ett konceptuellt godtagbart. Många så kallade denotationssemantiker är inte helt abstrakta, medan många operativa är. I själva verket har ett av de centrala ämnena i semantikens senaste historia involverat sökandet efter helt abstrakta definitioner som kastas inom klassen av semantiska definitionstekniker som tas för att leverera en denotational semantik.

Semantik spelar en normativ eller avgörande roll inom datavetenskap. Utan semantiska definitioner har språk och strukturer inget innehåll utöver det som tillhandahålls av deras syntaktiska beskrivningar. Och det senare är knappast tillräckligt för praktiska eller filosofiska ändamål. Medan vi har börjat med analysen av de centrala problemen, har vi bara repat ytan.

4. Bevis och program

Specifikationer (§2.3) inducerar en viss uppfattning om korrekthet. Enligt den abstrakta tolkningen av denna uppfattning anses ett program vara korrekt i förhållande till en (funktionell) specifikation om förhållandet det bryter mellan ingång och utgång uppfyller det som anges i specifikationen. Mer exakt, om p är ett program, uppfyller det en specifikation R, som anses vara en relation över ingångstyp I och utgångstyp O, om följande gäller:

För alla ingångar uppfyller jag av typ I, paret (i, p (i)) relationen R

där p (i) är resultatet av att köra programmet p på ingången i. Här uttrycks R i vissa specifikationsspråk och p i något programmeringsspråk. Den förstnämnda är vanligtvis en variant av (typ) predikatlogik och bevis för korrekthet (dvs. att uttalandet (1) rymmer) utförs i logikens bevissystem. Till exempel används Hoare-logik (Hoare 1969) ofta, där bevis för korrekthet har formen av slutsatser mellan tripplar, skrivna

B {P} A

där P är ett program och B och A är påståenden (programmen "före" och "efter") uttryckta i någon version av predikatlogiken med funktioner som underlättar uttrycket för värdena som är kopplade till programvariablerna.

En filosofisk kontrovers som omger frågan om korrekthet bygger på sådana bevis; den andra utmanar vad sådana bevis levererar.

4.1 Bevis inom datavetenskap

Är bevis på programmets korrekthet äkta matematiska bevis, dvs. är sådana bevis i nivå med standardmatematiska? DeMillo et al. (1979) hävdar att eftersom korrekthetsproven är långa och matematiskt grunt är de till skillnad från bevis i matematik som är konceptuellt intressant, övertygande och lockar uppmärksamheten hos andra matematiker som vill studera och bygga på dem. Exempelvis skulle ett bevis i Hoare-logik för att program 2 beräknar factorialfunktionen innehålla detaljer om den underliggande uppfattningen om tillstånd, använda ett induktivt argument och involvera resonemang om loop-invarians.

Men sådana bevis skulle vara mycket längre än själva programmet. Vidare skulle den nivå på vilken resonemanget kodas i Hoare-logik kräva uttryck och representation av många detaljer som normalt skulle vara implicita. Det skulle vara en tråkig och, för de flesta program, konceptuellt trivial.

Detta argument är parallellt med förståelsegrunderna i matematikens filosofi (t.ex. Tymoczko 1979; Burge 1988). I sitt hjärta finns epistemologiska bekymmer: bevis som är för långa, klumpiga och ointressanta kan inte vara bärare av den typ av säkerhet som tillskrivs standard matematiska bevis. Arten av den kunskap som erhållits från korrektionsbevis påstås vara annorlunda än den kunskap som kan hämtas från bevis i matematik [1].

Man måste också skilja detta väsentligen sociologiska perspektiv på bevis från det som hävdar att bevis är rätt eller fel på ett sätt som är oberoende av sådana epistemologiska bedömningar. Det är möjligt att hålla fast vid den mer realistiska ståndpunkt enligt vilken ett visst bevis är antingen korrekt eller felaktigt utan att ge upp kravet om att bevis, för att tas in och valideras, behöver förstås.

Man kan försöka vinna någon mark genom att förespråka att korrekt bevis bör kontrolleras av en dator snarare än en människa. Men självklart behöver provkontrollen själv kontrollera. Arkoudas och Bringsjord (2007) hävdar att om det bara finns ett korrekthetsbevis som måste kontrolleras, nämligen det för själva beviskontrollen, så minskar risken för misstag avsevärt.

4.2 Bevis i matematik

Matematiska bevis som beviset för Gödels ofullständighetsteorem är också långa och komplicerade. Men det som gör dem transparenta, intressanta och begripliga ('enkäterbara') av det matematiska samhället är användningen av modularitetstekniker (t.ex. lemmor) och användningen av abstraktion i den matematiska skapelsen. Införandet av nya koncept gör det möjligt att konstruera ett bevis gradvis och därigenom göra bevisen mer begripliga. Matematiken fortskrider genom att uppfinna nya matematiska begrepp som möjliggör konstruktion av högre nivå och mer allmänna bevis som skulle vara mycket mer komplexa och till och med omöjliga utan dem. Exempelvis gör exponentnotationen det möjligt att genomföra beräkningar utöver multiplikationens komplexitet - och argumentera om resultaten. I det andra extrema,uppfinningen av kategoriteori underlättade uttalandet och beviset på mycket generella resultat om algebraiska strukturer som automatiskt gäller för en hel rad sådana. Matematik handlar inte bara om bevis; det innebär också abstraktion och skapande av nya begrepp och notering. I motsats till detta använder formella korrekthetsbevis i allmänhet inte skapandet av nya begrepp eller engagerar sig i processen med matematisk abstraktion. Däremot är abstraktion inom datavetenskap (§6.1) koncentrerad till de idéer som behövs för programdesign. Men hur är dessa två begrepp om abstraktion relaterade? Vi kommer att säga lite mer om detta senare.det innebär också abstraktion och skapande av nya begrepp och notering. I motsats till detta använder formella korrekthetsbevis i allmänhet inte skapandet av nya koncept eller engagerar sig i processen med matematisk abstraktion. Däremot är abstraktion inom datavetenskap (§6.1) koncentrerad till de idéer som behövs för programdesign. Men hur är dessa två begrepp om abstraktion relaterade? Vi kommer att säga lite mer om detta senare.det innebär också abstraktion och skapande av nya begrepp och notering. I motsats till detta använder formella korrekthetsbevis i allmänhet inte skapandet av nya begrepp eller engagerar sig i processen med matematisk abstraktion. Däremot är abstraktion inom datavetenskap (§6.1) koncentrerad till de idéer som behövs för programdesign. Men hur är dessa två begrepp om abstraktion relaterade? Vi kommer att säga lite mer om detta senare.

4.3 Fysisk och abstrakt korrekthet

Även om vi lägger dessa epistemologiska bekymmer åt sidan, ifrågasätter en andra och till synes mer förödande kritik av korrekthet vad som faktiskt fastställs av dem. Till synes tillhandahåller ett bevis på korrekthet endast korrekthet upp till programmets textliga representation. Ingen form av formellt arbete kan få oss förbi den abstrakta / fysiska barriären: vi kan aldrig garantera att någon speciell exekvering av programmet på en fysisk maskin faktiskt kommer att fortsätta som förväntat (Fetzer 1988; Fetzer 1999; Colburn 2004).

Men vad betyder det att program p är korrekt? Antag att vi har en specifikation av programmet och att det kan vara formellt eller informellt. Anta sedan att vi genomför en serie testkörningar för att verifiera att programmet uppfyller specifikationen. Om de lyckas har vi empiriska bevis för att den fysiska motsvarigheten till det textuella programmet verkligen är korrekt eftersom det fungerar enligt specifikationen. Enligt denna uppfattning är det den fysiska motsvarigheten som testades; inte det textuella programmet.

Denna analys antyder att det finns en dualitet i uppfattningen om programmets korrekthet. I överensstämmelse med programmens dubbla karaktär kan vi säga att det textuella programmet är föremål för matematisk korrekthet, medan dess fysiska motsvarighet är föremål för empirisk verifiering.

5. Beräknbarhet

Beräknbarhet är ett av de äldsta ämnena som kan märkas som PCS. Det är emellertid ämnet för flera SEP-poster (t.ex. Barker-Plummer 2004), så vi kommer bara att nämna några ämnen och deras kopplingar till resten av den nuvarande posten.

5.1 The Church-Turing Thesis

En av de centrala frågorna är Church-Turing Thesis. Och här finns det två tvister, en historisk och en empirisk. De fokuserar på följande två möjliga tolkningar av avhandlingen:

  1. Turingmaskiner kan göra allt som kan beskrivas som”tumregel” eller”rent mekaniskt”.
  2. Oavsett vad som kan beräknas av en maskin (arbetar med begränsad data i enlighet med ett ändligt program med instruktioner) är Turing-maskinberäknbar.

Tolkning I är avsett att fånga uppfattningen om en effektiv eller mekanisk metod i logik och matematik. Det är avsett att återspegla den informella uppfattningen om algoritm implicerad i matematik och fördes fram av Hilberts program. Tolkning II är tänkt att styra fysiska maskiner. Faktum är att (Gandy 1980) kan ses som en ytterligare uppackning av II. Gandy föreslår fyra principer som är avsedda att karakterisera beräkning av en fysisk maskin. Han visar att sådana maskiner exakt stämmer med Turing karaktärisering (Gandys sats). I samband med vår diskussion om olika semantiska paradigmer är det uppenbart att många av maskinerna som ligger till grund för denotational semantik (§3.1) inte betecknas som Gandy-maskiner. De arbetar oftast med extensionsfunktioner med högre ordning,och dessa kan inte anses utgöra begränsad information och inte uppfylla Gandys villkor.

Vissa hävdar (Copeland 2004; Copeland 2008) att avhandlingen som föreslagits av Church and Turing endast avser tolkning I och inte sätter en gräns för maskiner i allmänhet. Hodges (2007) håller inte med. Han hävdar att Church och Turing inte skilde mellan de två tolkningarna. Detta är den historiska tvisten.

Den fysiska tvisten rör faktiska maskiners funktioner (tolkning II.) Många tar det för givet att avhandlingen från Church-Turing karakteriserar och föreskriver faktisk fysisk beräkning. Till exempel verkar detta vara det implicita antagandet inom mainstream datavetenskap. Det är verkligen så att varje program skrivet på ett befintligt implementerat programmeringsspråk är Turing beräkningsbart och omvänt, att alla allmänna programmeringsspråk är Turing komplett, dvs att de innehåller alla kontrollkonstruktioner som är nödvändiga för att simulera en universal Turing-maskin.

Copeland (2007) hävdar att Gandys karaktärisering av en diskret deterministisk mekanisk anordning är för snäv, och följaktligen finns det exempel på möjliga fysiska maskiner vars kapacitet går utöver klassen för Turing beräknbara funktioner. Många av dessa kräver oändlig hastighet, varigenom ett oändligt antal beräkningar kan utföras fysiskt på en begränsad tid. Kvantberäkning har nämnts som ett möjligt exempel för sådana maskiner, men detta har ifrågasatts (Hodges 2007; Hagar 2007).

Hodges handlar också om tillämpningen av standard matematisk argumentation i fysik i de fall där oändlig precision är inblandad. Detta antyder att denna tvist inte är en enkel empirisk. Det finns faktiskt de som ifrågasätter om det är fysiskt möjligt att slutföra ett oändligt antal uppgifter på en begränsad tid. Dummett (2006) ifrågasätter om själva uppfattningen om en oändlig uppgift som ska utföras i det fysiska världen inte bara är en fysisk omöjlighet utan också en konceptuell. Så tvisten är inte bara en empirisk utan går till kärnan i vår förståelse av förhållandet mellan våra matematiska modeller och den fysiska verkligheten.

6. Programmering och programmeringsspråk

Utformning av program och programmeringsspråk är en av de traditionella aktiviteterna inom datavetenskap. En mängd konceptuella frågor omger dem (§1), av vilka många inte har fått någon filosofisk uppmärksamhet. Här ska vi kort se över två av dessa problem.

6.1 Abstraktion

Abstraktion är en av de konceptuella hörnstenarna i datavetenskap. Det är en integrerad del av programdesign och konstruktion och utgör en kärnmetodik för design av programmeringsspråk. Det driver faktiskt skapandet av nya programmeringsparadigmer. Det ligger till grund för uppfinningen av föreställningar såsom procedurell och funktionell abstraktion, polymorfism, abstraktion av data, objekt och klasser, designmönster, arkitektoniska stilar, subtypning och arv. Många grenar inom programvaruteknik (t.ex. mjukvarumodellering, programförståelse, programvisualisering, om- och omkonstruktion) är främst upptagna med att undersöka lämpliga mekanismer för programabstraktion. Och mycket av framstegen inom mjukvaruteknik har uppnåtts på grund av införandet av nya abstraktionsmekanismer.

Men vad är abstraktionens natur i datavetenskap? Vad är den bakomliggande filosofiska förklaringen? Tyvärr, i allmänhet, är själva tanken på abstraktion filosofiskt problematisk. Enligt den traditionella uppfattningen, som har sitt ursprung i filosofisk psykologi, är abstraktion en mental process där nya föreställningar bildas genom att överväga flera objekt eller idéer och utelämna de egenskaper som skiljer dem. (Rosen 2001). Men denna strategi har få, om några, samtida filosofiska förespråkare.

En mer logisk metod för analys av abstraktion, som har viss stark förespråkning (Wright 1983; Hale 1987). Men det är oklart om dessa idéer, som utvecklades för matematisk abstraktion, är tillämpliga på datavetenskap. Det är uppenbart att några av idéerna om abstraktion inom datavetenskap var antingen inspirerade av eller undersökta med hjälp av abstraktioner i matematik. Men vad är det begreppsmässiga förhållandet mellan abstraktion inom dessa discipliner? Är de grundläggande olika? Tyvärr, även om det finns betydande litteratur om de filosofiska grunden för matematisk abstraktion (se Wright 1983; Hale 1987; Fine 2002), är den begreppsmässiga undersökningen av abstraktion inom datavetenskap i sin barndom. Colburn (2007) föreslår att skillnaden mellan abstraktion i matematik och abstraktion inom datavetenskap ligger i det faktum att i matematikabstraktion är informationsförsummelse medan det inom datavetenskap är information som döljer sig. Det vill säga abstraktioner i matematik ignorerar det som bedöms vara irrelevant (t.ex. färgen på liknande trianglar). Däremot, inom datavetenskap, får alla detaljer som ignoreras på en abstraktionsnivå (t.ex. Java-programmerare inte oroa sig för den exakta platsen i minnet som är associerade med en viss variabel) inte ignoreras av en av de lägre nivåerna (t.ex. den virtuella maskinen hanterar alla minnesallokeringar).abstraktioner i matematik ignorerar vad som bedöms vara irrelevant (t.ex. färgen på liknande trianglar). Däremot, inom datavetenskap, måste alla detaljer som ignoreras på en abstraktionsnivå (t.ex. Java-programmerare inte behöva oroa sig för den exakta platsen i minnet som är associerad med en viss variabel) inte ignoreras av en av de lägre nivåerna (t.ex. den virtuella maskinen hanterar alla minnesallokeringar).abstraktioner i matematik ignorerar vad som bedöms vara irrelevant (t.ex. färgen på liknande trianglar). Däremot, inom datavetenskap, måste alla detaljer som ignoreras på en abstraktionsnivå (t.ex. Java-programmerare inte behöva oroa sig för den exakta platsen i minnet som är associerad med en viss variabel) inte ignoreras av en av de lägre nivåerna (t.ex. den virtuella maskinen hanterar alla minnesallokeringar).

Men är detta baserat på en för förenklad uppfattning om abstraktion i matematik? Finns det bara en slags uppfattning? Till exempel är informationen som gömmer sig i Bishop's analys (Bishop 1970) ganska annorlunda än Wrights föreställning om abstraktion - och verkligen liknar datavetenskapen.

6.2 Typer och ontologi

Programmeringsspråk är mestadels typspråk, där den moderna begreppet typ har sitt ursprung i Frege och Russell och särskilt i Russells enkla typteori (Irvine 2003). Naturligtvis var Russell motiverad av de logiska och semantiska paradoxerna och denna funktion är inte central för tillämpningen av typer på datavetenskap. Å andra sidan, för Russell-typer snider upp diskursuniverset på sätt som har både grammatisk och semantisk import. Och denna idé har gått över till datavetenskap. Typteorierna har faktiskt inspirerats och berikats av datavetenskap. Till exempel är Russells teori om typer, även om det matematiskt är kraftfullt, något förarmat i sin uttrycksfulla kraft jämfört med typteorierna för moderna datorspråk (Coquand 2006; Pierce 2002). Förutom en rad grundtyper som nummer och booléer, innehåller programmeringsspråk en samling typkonstruktörer (sätt att bygga nya typer från gamla). Till exempel inkluderar dessa förmågan att bilda någon typ av kartesisk produkt och ändliga uppsättningar. I många objektorienterade programmeringsspråk kan typer (klasser) importera (och åsidosätta) operationer från andra typer och erbjuda mer sofistikerade konstruktörer som stöder bildandet av abstrakta datatyper och olika former av polymorfism.typer (klasser) kan importera (och åsidosätta) operationer från andra typer och erbjuda mer sofistikerade konstruktörer som stöder bildandet av abstrakta datatyper och olika former av polymorfism.typer (klasser) kan importera (och åsidosätta) operationer från andra typer och erbjuda mer sofistikerade konstruktörer som stöder bildandet av abstrakta datatyper och olika former av polymorfism.

Inom datavetenskap spelar typer en roll som är halvvägs mellan syntax och semantik. För det första utvidgar de vår normala uppfattning om sammanhangsfri grammatik. Vissa språkfunktioner, särskilt de som gör det möjligt att fixa typen av en variabel efter sammanhang (dvs språkdeklarationer) kräver en form av grammatik som är mer flexibel än den vanliga. Så kallade två nivåers grammatik, även om det är tekniskt tillräckligt, fångar inte det sätt på vilket variabler tilldelas sina typer på moderna språk. Och de är väldigt klumpiga att använda. De anpassar sig inte heller lätt till polymorfiska system på många språk. Moderna typsystem gör bättre: variabler tilldelas sina typer via deklarationer, t.ex. x: Boolean. Därefter kan en kompilator typkontrollera programmet, t.ex.det kan säkerställa att förekomsten av en variabel i efterföljande uttalanden (t.ex. x

Men typer spelar också en korrekt roll som normalt inte skulle beskrivas i syntaktiska termer. Det gör detta genom att utöka det traditionella fysiska begreppet dimensionell analys till ett mycket rikare system av typer. Att få rätt typstruktur för ett program går på något sätt för att säkerställa dess korrekthet. Och detta bestäms av strukturen som typer påför ett språk. Typer fixar vilka saker det finns i ett programmeringsspråk. Så till exempel, alla programmeringsspråk som tillåter antal, produkter och klasser, och inget annat, sätter en konceptuell ram för programmeraren som hon måste arbeta inom. Problem måste vara formulerade och lösningar finns inom de representationsmedel som tillhandahålls av typsystemet. När typstrukturen för ett programmeringsspråk har fastställts har mycket av dess ontologiska inställning fixats.

Eller har det? Kanske måste vi gå tillbaka och först fråga hur de ontologiska åtagandena för ett språk ska fastställas. Är det semantiken som avgör frågor (Turner & Eden 2007)? En lång tradition som härrör från Frege skulle föreslå det (Dummett 1991). Förutsatt att analogin med naturliga språk är legitim, bestäms ontologin för ett språk av strukturerna som krävs för att tillhandahålla dess semantiska domäner. Men vilken semantisk teori ska vi anta? Medan varje semantik måste ta hänsyn till typer, skulle den semantiskt bestämda ontologin gå utöver dem och återspegla de semantiska domänerna, och dessa skulle återspegla implementeringsdetaljen som ingår i semantiken. På samma sätt, som med jämställdhet, bestämmer olika semantiska tolkningar olika ontologier. Av detta följer att det inte är förnuftigt att prata om ontologin för ett programmeringsspråk utan om flera ontologier som är beroende av abstraktionsnivån i semantiken. Till exempel kan ontologin också delvis bestämmas av programmeringsparadigmet.

7. Juridiska och etiska frågor

Vissa frågor inom datoretik tillhör PCS genom att aktiviteten för att bygga och använda programvara väcker etiska frågor. Många är emellertid inte specifika för datavetenskap i den smala betydelsen av detta inträde; de påverkar hela informationstekniken och datortillämpningar (Bynum 2001). Följaktligen ska vi bara nämna två som verkar centrala för datavetenskapen.

7.1 Upphovsrätt, patent och identitet

Upphovsrätt ger ett visst skydd för programvara, men de kan inte skydda dess semantiska kärna. Och vi anser att det senare ska bestämmas av ett semantiskt konto (§3) för det programmeringsspråk som programmet skrivs i. Antagligen rör kärnan i denna fråga problemet med programidentitet (§3.3). Men om det finns många möjliga semantiska idéer om identitet, vilken är lämplig för juridisk tillämpning?

Ett informellt semantiskt konto som ofta citeras i lag identifierar programmet med de idéer som uttrycks där, oftast anses det vara den underliggande algoritmen. Men inte bara är det ofta svårt att säga exakt vad denna algoritm är, utan också, som med matematiska teorem, kan algoritmer inte upphovsrättsskyddas. Och ungefär samma öde väntar på något formellt semantiskt konto eftersom något sådant skulle bestämmas av någon matematisk uppfattning, vare sig det är algoritmer eller någon aning om funktion eller matematisk funktion.

Men även om vi kunde hitta ett semantiskt konto som skulle övergå till upphovsrättslagarna, skulle den rättsliga bilden inte vara fullständig. Upphovsrättsintrång hänger ofta inte bara på en del av identiteten utan också på om det är troligt att anta att någon skulle komma med samma program. Så att avsiktliga överväganden kommer in i ramen. Med andra ord, även om två program anses vara likvärdiga enligt vårt semantiska kriterium, om det kunde ses som troligt att de byggdes oberoende, skulle det inte vara intrång i upphovsrätten.

Patent (särskilt verktygspatent) går inte bättre. De är ännu svårare att få för mjukvara eftersom man inte kan patentera mentala processer, abstrakta idéer och algoritmer. Och det är algoritmer snarare än källkoden som ofta innehåller de nya idéerna. Men än en gång är det identifierings- och identitetsfrågorna som är den centrala filosofiska frågan. Och dessa involverar både semantiska och avsiktliga överväganden.

7.2 Korrekthet och ansvar

Är det rätt att mjukvara säljs med liten garanti för lämplighet för ändamål? (Coleman 2008) ägnas åt denna fråga. Detta är en särskilt relevant fråga för säkerhetskritiska system, t.ex. system som övervakar medicinska tillstånd, driver kärnkraftverk och kommunicerar med rymdbussar. Det verkar väsentligt att verkställa strängare tester och bevis på korrekthet. Men i etiska termer, är det fallet med en programmerare som inte analyserar och testar sitt program annorlunda än det för en civilingenjör som inte utför den nödvändiga matematiska modelleringen och tester i en byggnadskonstruktion? De moraliska skyldigheterna verkar likadana.

Ett sätt på vilket de kan vara annorlunda hänför sig till mjukvarans komplexitet (Brooks 1987) som överstiger komplexiteten hos någon annan typ av mänsklig artefakt med storleksordningar. Många hävdar att det inte är möjligt att erbjuda någon sådan garanti för korrekthet (DeMillo et al. 1979); mjukvara är så komplex att processen med rigorösa matematiska bevis och mjukvarutestning är omöjlig. Och förmodligen kan man bara ha en (moralisk eller juridisk) skyldighet att genomföra en genomförbar process.

Men hur balanserar man de bevisande och testande aspekterna av mjukvaruutveckling mot den avsedda användningen av programvaran? Bör mjukvara utvecklad för underhållning omfattas av samma grad av noggrann bevisning och testning som mjukvara som är säkerhetskritisk? Förmodligen inte, men vi kanske fortfarande frestas att fråga, är det här nya etiska problem eller ger de oss bara ytterligare fallstudier av befintliga etiska dilemma? Till exempel kan även säkerhetsbrister i programvara som används i underhållningsindustrin medföra ekonomiska påföljder.

8. Nya vändningar eller nya problem?

Till och med denna ganska korta översikt över PCSborde övertyga läsaren att datavetenskap väcker intressanta och krävande filosofiska frågor. Ett av de överväldigande intrycka är faktiskt att det har väsentliga kopplingar till de flesta filosofiska traditionella grenar. Det finns tydliga samband med ontologi, etik, epistemologi och filosofierna i matematik, fysik och språk. Vår första lista med frågor väcker faktiskt många fler teman som kopplas till andra filosofiska områden. I synnerhet finns det en betydande litteratur om datavetenskapens tillämpningar. Konstgjord intelligens och kognitiv vetenskap ger filosofiska frågor som tillhör sinnesfilosofin (McLaughlin 2004). Naturligtvis kommer mycket av detta från Turing (1950). Andra tillämpningar av datavetenskap på traditionella vetenskapsområden, så kallad computational science,skapa problem för vetenskapsfilosofin: vad är den epistemologiska effekten av datorsimuleringar, särskilt där det är den enda genomförbara formen av experiment? Den beräknande vändningen i ontologin ger nya tekniker att bära strukturen i någon form av begreppsmässig ontologi. Logikfilosofin berikas av en massa material: ett stort antal nya logiska system har dykt upp för att representera och resonera om beräkningssystem.ett stort antal nya logiska system har dykt upp för att representera och resonera om beräkningssystem.ett stort antal nya logiska system har dykt upp för att representera och resonera om beräkningssystem.

Även om det är uppenbart att datavetenskap väcker många viktiga vändningar till traditionella filosofiska problem, är det mindre tydligt om det genererar några verkligt nya filosofiska problem: finns det frågor i PCS som inte har någon parallell i någon annan filosofisk gren?

Bibliografi

  • Allison, A., Currall, J., Moss, M. och Stuart, S., 2005, "Digital identitetsfrågor", Journal of American Society Information Science and Technology 56 (4): 364–372.
  • Arkoudas, K. och Bringsjord, S., 2007, "Datorer, motivering och matematisk kunskap", Minds and Machines 17 (2): 185–202.
  • Barendregt, HP, 1993, "Lambda calculi with types", i: Handbook of logic in computer science, Vol. 2, New York, NY: Oxford University Press Inc.
  • Barker-Plummer, D., 2008, "Turing Machines", The Stanford Encyclopedia of Philosophy (Fall 2008 Edition), Edward N. Zalta (red.), URL = .
  • Bishop, Errett, 1977, Foundations of constructive analysis, McGraw-Hill.
  • Blass, Andreas och Gurevich, Yuri, 2003, “Algoritms: A Quest for Absolute Definitions”, Bulletin of the European Association for Theoretical Computer Science (EATCS) No.81: 195-225.
  • Bowen, JP och Hinchey, MG, 1995, "Tio bud av formella metoder", IEEE Computer 28 (4): 56–63.
  • Bowen, JP och Hinchey, MG, 2005, "Tio bud av formella metoder: tio år senare", IEEE Computer 39 (1): 40–48.
  • Brooks, FP, 1987, "No Silver Bullet: Essence and Accidents of Software Engineering", IEEE Computer 20 (4): 10-19.
  • Burge, T., 1998, "Computer Proof, A Priori Knowledge and Other Minds", Philosophical Perspectives 12: 1–37.
  • Bynum, T., 2001, "Computer Ethics: Basic Concepts and Historical Oversikt", The Stanford Encyclopaedia of Philosophy (Winter 2001 Edition), Edward N. Zalta (red.), URL =
  • Colburn, T., 2004, "Methodology of Computer Science", Blackwell Guide to the Philosophy of Computing and Information, Luciano Floridi (red.), Malden: Blackwell, s. 318–326.
  • Colburn, T. och Shute, G., 2007, "Abstraktion inom datavetenskap", Minds and Machines 17 (2): 169–184.
  • Coleman, KG, 2008, "Computing and Moral Responsibility", The Stanford Encyclopedia of Philosophy (Fall 2008 Edition), Edward N. Zalta (red.), URL = .
  • Copeland, B. Jack, 2008, "The Church-Turing Thesis", The Stanford Encyclopedia of Philosophy (hösten 2008 Edition), Edward N. Zalta (red.), URL = .
  • Copeland, B. Jack, 2004, "Computation", Blackwell Guide to the Philosophy of Computing and Information, Luciano Floridi (red.), Malden: Blackwell, s. 3–17.
  • Coquand, Thierry, 2006, "Type Theory", The Stanford Encyclopedia of Philosophy (Winter 2006 Edition), Edward N. Zalta (red.), URL = .
  • DeMillo, RA, Lipton, RJ och Perlis, AJ, 1979, "Sociala processer och bevis för teorier och program", Kommunikation av ACM 22 (5): 271–280.
  • Denning, PJ, 1980, "Om folksteorier och folkmyter", Kommunikation av ACM 23 (9): 493–494.
  • Denning, PJ, 1980b, "Vad är experimentell datavetenskap?" Kommunikation av ACM 23 (10): 534–544.
  • Denning, PJ, 1981, "Performance Analysis: Experimental Computer Science as its Best", Communications of ACM 24 (11): 725–727.
  • Denning, PJ, 1985, "The Science of Computing: What is computer science?" American Scientist 73 (1): 16–19.
  • Denning, PJ (red.), Et al., 1989, "Computing as a Discipline", Communications of ACM 32 (1): 9–23.
  • Dijkstra, E., 1968. "Gå till uttalande anses skadligt", meddelanden om ACM 11 (3): 147–148.
  • Dummett, M., 1991, "The Logical Base of Metaphysics", Harvard University Press.
  • Dummett, M., 2006, "Tanke och verklighet", Oxford University Press.
  • Eden, Amnon, 2007, “Three Paradigms in Computer Science”, Minds and Machines 17 (2): 135–167.
  • Feferman, S., 1992, "Logik för avslutande och korrekthet av funktionella program", Logic for Computer Science: 95–127, MSRI Pubs. vol. 21, New York, NY: Springer-Verlag.
  • Fetzer, JH, 1988, "Programverification: The Very Idea", Kommunikation av ACM 31 (9): 1048–1063.
  • Fetzer, JH, 1999, "Modellenes roll i datavetenskap", The Monist 82 (1): 20–36.
  • Fine, K., 2008, "The Limits of Abstraction". Oxford: Oxford University Press.
  • Floridi, Luciano, 2004.”Information”, Blackwell Guide to the Philosophy of Computing and Information, Luciano Floridi (red.), Malden: Blackwell, s. 40–62.
  • Floridi, Luciano 2007, "Semantic Conceptions of Information", The Stanford Encyclopedia of Philosophy (Spring 2007 Edition), Edward N. Zalta (red.), URL = .
  • Forrest, P., 2006, "The Identity of Indiscernibles", The Stanford Encyclopedia of Philosophy (Fall 2008 Edition), Edward N. Zalta (red.), Kommande URL =. >.
  • Fuchs, NE, 1992, "Specifikationer är (helst) körbara". Software Engineering Journal 7 (5): 323–334.
  • Gandy, R., 1980, "Kyrkans avhandling och principer för mekanismer", The Kleene symposium, Barwise, J., Keisler, HJ och Kunen, K. (red.), Amsterdam: Nord-Holland.
  • Hagar, Amit, 2007, “Kvantealgoritmer: Filosofiska lektioner”, Minds and Machines 17 (2): 233–247.
  • Hale, B. och Wright, C., 2001, "The Reason's Proper Study: Essays into Neo-Fregean Philosophy of Mathematics", Oxford Scholarships on Line, Oxford: Oxford University Press.
  • Hartmanis, J., 1993, "Vissa observationer om datavetenskapens natur", Föreläsningsanteckningar i datavetenskap 761, Shyamasundar, RK (red.): 1–12.
  • Hartmanis, J., 1994, "Turing Award Lecture: On Computational Complexity and the Computer of Science Science", Communications of the ACM 37 (10): 37–43.
  • Hoare, CAR, 1969, "En axiomatisk grund för datorprogrammering". Kommunikation av ACM 12 (10): 576–585. [Skriv ut på nytt tillgängligt online]
  • Hodges, A., 2006, "Har Church and Turing en avhandling om maskiner?", Church's Thesis efter 70 år Olszewski, Adam (red.)
  • Hodges, A., 2007, "Kan kvantberäkning lösa klassiskt olösliga problem?"
  • Horsten, L., 2008, "Philosophy of Mathematics", The Stanford Encyclopedia of Philosophy (hösten 2008-utgåvan), Edward N. Zalta (red.), URL = .
  • Immerman, N., 2006, "Computability and Complexity", The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (red.), URL = .
  • Irvine, AD, 2003, "Russells paradox", The Stanford Encyclopedia of Philosophy (hösten 2006-utgåvan), Edward N. Zalta (red.), URL =
  • Jones, CB och Hayes, IJ, 1990, "Specifikationer är inte (nödvändigtvis) skadliga", Software Engineering Journal 4 (6): 330–339.
  • Krishnamurthi, S., 2003. Programmeringsspråk: tillämpning och tolkning,
  • Kreisel, G., Gandy, RO, 1975, "Några skäl för att generalisera rekursionsteori." Journal of Symbolic Logic 40 (2): 230–232.
  • Kripke, S., 1982, Wittgenstein om regler och privata språk. Harvard University Press.
  • Kuhn, TS, 1970, The Structure of Scientific Revolutions, 2nd. red., Chicago: Univ. från Chicago Press.
  • Landin, PJ, 1964, "Den mekaniska utvärderingen av uttryck", Computer Journal 6 (4): 308–320.
  • Milne, R. och Strachey, C., 1977, A Theory of Programming Language Semantics, New York, NY: Halsted Press.
  • McLaughlin, B., 2004, "Computationalism, Connectionism and the Philosophy of Mind", Blackwell Guide to Philosophy of Computing and Information, Floridi, Luciano (red.) Malden: Blackwell, s. 135–152.
  • Minsky, M., 1970, "ACM Turing Lecture: Form and Content in Computer Science", Journal of the Association for Computing Machinery 17 (2): 197–215.
  • Moor, JH, 1978, "Three Myths of Computer Science", The British Journal for the Philosophy of Science 29 (3): 213–222.
  • Moschovakis, YN, 1998, "On grundande teorin om algoritmer", Truth in Mathematics Dales, Harold G. och Oliveri, Gianluigi (red.), Oxford: Oxford University Press.
  • Pierce, Benjamin C., 2002, Typer och programmeringsspråk, Cambridge, MA: MIT Press.
  • Plotkin, GD, 1981, "A Structural Approach to Operational Semantics", Tech. Rep. DAIMI FN-19, datavetenskapliga avdelningen, Aarhus universitet, Aarhus, Danmark.
  • Rapaport, WJ, 2005a, "Filosofi för datavetenskap: en introduktionskurs", Teaching Philosophy 28 (4): 319–341.
  • Rapaport, WJ, 2005b, "Implementering är semantisk tolkning: ytterligare tankar." Journal of Experimental and Theoretical Artificial Intelligence 17 (4): 385–417.
  • Rosen, Gideon, 2001. "Abstract Objects", The Stanford Encyclopedia of Philosophy (Fall 2001 Edition), Edward N. Zalta (red.), URL = .
  • Shapiro, S., 1997, Philosophy of Mathematics: Structure and Ontology, Oxford: Oxford University Press.
  • Sieg, Wilfried, 2008, "Church without Dogma: Axioms for Computability", New Computational Paradigms, Lowe, B., Sorbi, A. and Cooper, B. (eds.), Springer-Verlag, 139–152.
  • Smith, BC, 1996, "Limits of Correctness in Computers", Computerization and Controversy, Kling, R. (red.), Morgan Kaufman, s. 810–825.
  • Szabó, ZG, 2007, "Compositionality", The Stanford Encyclopedia of Philosophy (Spring 2007 Edition), Edward N. Zalta (red.), URL = .
  • Thomason, R., 2005, "Logic and Artificial Intelligence", The Stanford Encyclopedia of Philosophy (Summer 2005 Edition), Edward N. Zalta (red.), URL = .
  • Turner, Raymond och Eden, Amnon H., 2007, "Mot programmeringsspråkontologi", Computation, Information, Cognition-The Nexus and the Liminal, Dodig-Crnkovic, Gordana and Stuart, Susan (red.), Cambridge, Storbritannien: Cambridge Scholars Press, s. 147–159.
  • Turner, Raymond, 2005, “The Foundations of Specification”, Journal of Logic Computation 15: 623–662.
  • Turner, Raymond, 2007, "Förstå programmeringsspråk". Minds and Machines 17 (2): 129-133
  • Tymoczko, T., 1979, "Det fyrafärgiga problemet och dess filosofiska betydelse", Journal of Philosophy 76 (2): 57–83.
  • White, G., 2004, "The Philosophy of Computer Språk", Blackwell Guide to the Philosophy of Computing and Information, Floridi, Luciano (red.), Malden: Blackwell, s. 318–326.
  • Wing, JM, 2006, "Computational Thinking", Communications of the ACM, 49 (3): 33–35.
  • Wittgenstein, L., 1953. Philosophical Investigations. Blackwell Publishing.
  • Wright, Crispin, 1983, Freges Conception of Numbers as Objects, Aberdeen University Press.

Andra internetresurser

  • Filosofi för datavetenskap vid Essex universitet
  • International Association for Computing and Philosophy

Rekommenderas: