John V. Tucker

John Vivian Tucker (född 4 februari 1952) är en brittisk datavetare och expert på beräkningsteori , även känd som rekursionsteori . Beräkningsbarhetsteorin handlar om vad som kan och inte kan beräknas av människor och maskiner. Hans arbete har fokuserat på att generalisera den klassiska teorin för att hantera alla former av diskret/ digital och kontinuerlig/ analog data; och om att använda generaliseringarna som formella metoder för systemdesign; baserat på abstrakta datatyper och på gränssnittet mellan algoritmer och fysisk utrustning.

Biografi

Född i Cardiff, Wales, utbildades han vid Bridgend Boys' Grammar School, där han undervisades i matematik, logik och datoranvändning. Han läste matematik vid University of Warwick (BA 1973) och studerade matematisk logik och grunderna för datoranvändning vid University of Bristol (MSc 1974, PhD 1977). Han har haft tjänster vid Oslo universitet , CWI Amsterdam, och vid Bristol och Leeds universitet , innan han återvände till Wales som professor i datavetenskap vid Swansea University 1989. Förutom teoretisk datavetenskap föreläser Tucker också om datorernas historia och historia. om vetenskapens och teknikens historia och Wales.

Tucker grundade British Colloquium for Theoretical Computer Science 1985 och var dess president från starten fram till 1992. Han är fellow i British Computer Society och redaktör för flera internationella vetenskapliga tidskrifter och monografiserier. På Swansea har han varit chef för datavetenskap (1994–2008), chef för fysikaliska vetenskaper (2007–11) och vice prorektor (2011–2019). Han är medlem av Academia Europaea . Utanför datavetenskap har Tucker varit förvaltare av den walesiska tankesmedjan, Institute of Welsh Affairs och ordförande för Swansea Bay- filialen. Han är också förvaltare av South Wales Institute of Engineers Educational Trust och Gower Society .

Professor Tucker är gift med Dr. TE Rihll, tidigare läsare i antik historia vid Swansea University.

I början av 1990-talet började han lobba för en nationell akademi för Wales. 2008 började en process för att skapa en sådan akademi sponsrad av det dåvarande University of Wales . Professor Tucker är en av grundarna av Learned Society of Wales och i juli 2010 utsågs han till dess konstituerande generalsekreterare, en post han innehade fram till maj 2017.

Arbeta med beräkningsbarhet och datatyper

Klassisk beräkningsbarhetsteori är baserad på datatyperna strängar eller naturliga tal . I allmänhet modelleras datatyper, både diskreta och kontinuerliga, av universella algebror , som är uppsättningar av data utrustade med operationer och tester. Tuckers teoretiska arbete tar itu med problemen med: hur man definierar eller specificerar egenskaper för operationer och tester av datatyper; hur man programmerar och resonerar med dem; och hur man implementerar dem.

I en serie satser och exempel, med början 1979, etablerade Jan Bergstra och Tucker uttryckskraften hos olika typer av ekvationer och andra algebraiska formler på vilken diskret datatyp som helst, styrd av satser av formen:

På alla diskreta datatyper kan funktioner definieras som de unika lösningarna för små finita ekvationssystem om, och endast om, de är beräkningsbara med algoritmer.

Deras program klassificerade heltäckande specifikationsmetoder för datatyper. Resultaten kombinerade tekniker för universell algebra och rekursionsteori, inklusive termomskrivning och Matiyasevichs teorem .

För de andra problemen har han och hans medarbetare utvecklat två oberoende disparata generaliseringar av klassisk beräkningsbarhet/rekursionsteori, som är likvärdiga för många kontinuerliga datatyper.

Den första generaliseringen, skapad med Jeffrey Zucker, fokuserar på imperativ programmering med abstrakta datatyper och täcker specifikationer och verifiering med Hoare-logik . Till exempel visade de att:

Alla beräkningsbara funktioner på de reella talen är de unika lösningarna till ett enda ändligt system av algebraiska formler.

Den andra generaliseringen, skapad med Viggo Stoltenberg-Hansen , fokuserar på att implementera datatyper med hjälp av approximationer som finns i domänteorins ordnade strukturer .

De allmänna teorierna har tillämpats som formella metoder i mikroprocessorverifieringar, datatyper och verktyg för volymgrafik och modellering av exciterande media inklusive hjärtat.

Arbeta med beräkningsbarhet och fysik

Sedan 2003 har Tucker arbetat med Edwin Beggs och Felix Costa på en allmän teori som analyserar gränssnittet mellan algoritmer och fysisk utrustning. Teorin ger svar på olika frågor om:

  1. hur algoritmer kan förstärkas av fysiska enheter för speciella ändamål som fungerar som "orakel";
  2. hur algoritmer styr fysiska experiment som är designade för att göra mätningar.

Genom att omvandla idén om oraklet i beräkningsbarhetsteorin kombinerar de algoritmiska modeller med exakt specificerade modeller av fysiska processer. Till exempel ställer de frågan:

Om ett fysiskt experiment skulle styras helt av en algoritm, vilken effekt skulle algoritmen ha på de fysiska mätningarna som experimentet möjliggör?

Deras centrala idé är att, precis som Turing modellerade den mänskliga datorn 1936 av en Turing-maskin, modellerar de en tekniker som utför en experimentell procedur som styr ett experiment, av en Turing-maskin . De visar att beräkningsmatematiken sätter grundläggande gränser för vad som kan mätas i klassisk fysik:

Det finns ett enkelt Newtonskt experiment för att mäta massa, baserat på kolliderande partiklar, för vilket det finns oräkneligt många massor m så att det för varje experimentell procedur som styr utrustningen bara är möjligt att bestämma ändligt många siffror av m, även medge godtyckliga långa körtider för proceduren. I synnerhet finns det oräkneligt många massor som inte går att mäta.

Arbeta med det digitala samhället

Sedan 2004 har Tucker och Victoria Wang studerat karaktären och rollen av digital data i personliga, sociala och organisatoriska sammanhang, särskilt övervakning. Först har de skapat en teori om phatic teknologier och integrerat den i teorin om modernitet som utvecklats av Anthony Giddens . För det andra har de en teori om att övervaka människor och föremål som används för att analysera många övervakningssammanhang och processer; detta har lett till matematiska modeller av övervakningssystem härledda från abstrakt datatypteori .

Arbeta med vetenskapens och teknikens historia

2007 grundade Tucker History of Computing Collection vid Swansea University . Han har föreläst om beräkningens historia sedan 1994, med intressen för datorer före datorer och teorier om data och beräkning. Han är en av grundarna av redaktionen för Springer -bokserien History of Computing. Han föreläser också om vetenskapens och teknikens historia i Wales och är en av grundarna av redaktionen för University of Wales Press- bokserien Scientists of Wales .

  1. JA Bergstra och JV Tucker, Ekvationella specifikationer, fullständiga termomskrivningssystem och beräkningsbara och semiberäknade algebror, Journal of the ACM , Volym 42 (1995), pp1194–1230.
  2. V Stoltenberg-Hansen och JV Tucker, Effektiva algebras , i S Abramsky, D Gabbay och T Maibaum (red.), Handbook of Logic in Computer Science, Volym IV: Semantic Modeling , Oxford University Press (1995), pp357–526.
  3. V Stoltenberg-Hansen och JV Tucker, Computable rings and fields , i E Griffor (red.), Handbook of Computability Theory , Elsevier (1999), pp363–447.
  4. JV Tucker och JI Zucker, Computable functions and semicomputable sets on many sorted algebras , i S Abramsky, D Gabbay och T Maibaum (red.), Handbook of Logic in Computer Science, Volym V: Logic and Algebraic Methods , Oxford University Press (2000) ), sid. 317-523.
  5. JV Tucker och JI Zucker, Abstrakt beräkningsbarhet och algebraisk specifikation , ACM Transactions on Computational Logic , Volym 5 (2004), pp. 611–668.
  6. JA Bergstra och JV Tucker, The rational numbers as an abstract data type, Journal of the ACM, 54: 2 (2007), Artikel 7. https://dl.acm.org/doi/10.1145/1219092.1219095 .
  7. JA Bergstra, Y Hirschfeld och JV Tucker, Meadows and the equational specification of division , Theoretical Computer Science , 410 (2009), 1261–1271. doi : 10.1016/j.tcs.2008.12.015
  8. EJ Beggs, JF Costa, B Loff och JV Tucker, Beräkningskomplexitet med experiment som orakel , Proceedings Royal Society Series A , 464 (2008) 2777–2801.
  9. EJ Beggs, JF Costa, B Loff och JV Tucker, Beräkningskomplexitet med experiment som orakel II: Upper bounds , Proceedings Royal Society Series A , 465 (2009) 1453–1465.
  10. EJ Beggs, JF Costa och JV Tucker, Gränser för mätning i experiment styrda av algoritmer , Mathematical Structures in Computer Science, 20 (2010) 1019–1050.
  11. Victoria Wang och JV Tucker, Phatic systems in digital society. Technology in Society, 46 (2016), 140-148, http://dx.doi.org/10.1016/j.techsoc.2016.06.002
  12. Victoria Wang, Kevin Haines och JV Tucker, Deviance and Control in Communities with Perfect Surveillance – The Case of Second Life, Surveillance and Society, 9 (2011) 31-46, https://doi.org/10.24908/ss.v9i1/ 2,4096 <a i=2>. .
  13. Victoria Wang och JV Tucker, 'I am not a number': Conceptualising identity in digital surveillance Technology in Society, 67, november 2021, 101772, https://doi.org/10.1016/j.techsoc.2021.101772 .
  14. JV Tucker, Robert Recorde: data, computation and the Tudor kunskapsekonomi , i G Roberts och F Smith (red), Robert Recorde: Life and Work , University of Wales Press, 2012, 165–187.
  15. JV Tucker, Richard Price and the History of Science, Transactions of the Honorable Society of the Cymmrodorion , New Series 21 (2017), 69–86.
  16. JV Tucker, The Computer Revolution and Us: Computer Science at Swansea University från 1960-talet, Swansea University Centenary Essays, https://collections.swansea.ac.uk/s/swansea-2020/page/computer-science .

externa länkar

Hämtad från " https://en.wikipedia.org/w/index.php?title=John_V._Tucker&oldid=1085193734 "