Perché i programmi non possono essere dimostrati?

https://stackoverflow.com/questions/476959

20-08-2019
|

Domanda

Perché un programma per computer non può essere dimostrato proprio come può esserlo un'affermazione matematica?Una dimostrazione matematica è costruita su altre dimostrazioni, le quali sono costruite a partire da altre dimostrazioni fino agli assiomi: quelle verità che riteniamo evidenti.

I programmi per computer non sembrano avere una tale struttura.Se scrivi un programma per computer, come puoi prendere lavori precedenti comprovati e usarli per mostrare la verità del tuo programma?Non puoi perché non ne esistono.Inoltre, quali sono gli assiomi della programmazione?Le verità atomiche del campo?

Non ho buone risposte a quanto sopra.Ma sembra che il software non possa essere dimostrato perché è arte e non scienza.Come si dimostra un Picasso?

Soluzione

Prove sono programmi.

La verifica formale dei programmi è una enorme area di ricerca. (Vedi, ad esempio, il gruppo di Carnegie Mellon .)

Molti programmi complessi sono stati verificati; per esempio, vedi questo kernel scritto in Haskell .

Altri suggerimenti

I programmi assolutamente possono essere dimostrati corretti. Programmi difficili sono difficili da dimostrare. Per farlo anche ragionevolmente bene, devi evolvere il programma e la prova mano nella mano.

Non puoi automatizzare la prova a causa del problema di arresto. Puoi, tuttavia, provare manualmente le post-condizioni e i presupposti di qualsiasi dichiarazione arbitraria o sequenza di dichiarazioni.

Devi leggere Una disciplina della programmazione di Dijsktra.

Quindi, devi leggere The Science of Programming di Gries. / p>

Allora saprai come dimostrare i programmi corretti.

Solo un piccolo commento a coloro che hanno sollevato incompletezza - non è il caso di tutti sistemi assiomatici, solo sufficientemente potenti .

In altre parole, Godel ha dimostrato che un sistema assiomatico abbastanza potente da descrivere se stesso sarebbe necessariamente incompleto. Ciò non significa che sarebbe inutile, tuttavia, e come altri hanno collegato, sono stati fatti vari tentativi di prove del programma.

Anche il duplice problema (scrivere programmi per verificare le prove) è molto interessante.

È infatti possibile scrivere programmi perfettamente corretti. Microsoft, ad esempio, ha creato un'estensione del linguaggio C # denominata Spec # che include un prover di teorema automatizzato. Per java esiste ESC / java . Sono sicuro che ci sono molti altri esempi là fuori.

( modifica : apparentemente spec # non è più in fase di sviluppo, ma gli strumenti di contratto entreranno a far parte di .NET 4.0 )

Vedo alcuni poster che sventolano a mano sul problema di arresto o teoremi di incompletezza che presumibilmente impediscono la verifica automatica dei programmi. Questo ovviamente non è vero; questi problemi ci dicono semplicemente che è possibile scrivere programmi che non possono essere dimostrati corretti o errati . Ciò non ci impedisce di costruire programmi che sono dimostrabilmente corretti.

Il problema di arresto mostra solo che ci sono programmi che non possono essere verificati. Una domanda molto più interessante e più pratica è quale classe di programmi può essere verificata formalmente. Forse tutti i programmi che interessano a qualcuno potrebbero (in teoria) essere verificati. ~~In pratica, finora, solo programmi molto piccoli sono stati dimostrati corretti.~~

Se sei davvero interessato all'argomento, lasciami prima raccomandare " di David Gries; The Science of Programming " ;, un classico lavoro introduttivo sull'argomento.

In realtà è possibile dimostrare i programmi corretti in una certa misura. È possibile scrivere precondizioni e postcondizioni e quindi dimostrare che, dato uno stato che soddisfa le precondizioni, lo stato risultante dopo l'esecuzione soddisferà le postcondizioni.

Dove diventa difficile, tuttavia, sono i loop. Per questi, è inoltre necessario trovare un invariante di loop e per mostrare la terminazione corretta è necessario trovare una funzione di limite superiore sul numero massimo possibile di iterazioni rimanenti dopo ciascun loop. Devi anche essere in grado di dimostrare che questo diminuisce di almeno uno dopo ogni iterazione attraverso il ciclo.

Una volta che hai tutto questo per un programma, la prova è meccanica. Ma sfortunatamente, non c'è modo di derivare automaticamente le funzioni invarianti e associate per i loop. L'intuizione umana è sufficiente per casi insignificanti con piccoli loop, ma realisticamente programmi complessi diventano rapidamente intrattabili.

Innanzitutto, perché stai dicendo " I programmi NON POSSONO essere dimostrati " ;?

Cosa intendi con " programmi " comunque?

Se per programma intendi algoritmi non conosci Kruskal? di Dijkstra? MST? di Prim? Ricerca binaria? Mergesort? DP? Tutte quelle cose hanno modelli matematici che descrivono i loro comportamenti.

descrivere. La matematica non spiega il perché delle cose semplicemente disegna un'immagine del come. Non posso dimostrarti che il Sole sorgerà domani a est, ma posso mostrare i dati su dove ha fatto quella cosa in passato.

Hai detto: " Se scrivi un programma per computer, come è possibile prendere precedenti lavori comprovati e usarli per mostrare la verità del tuo programma? Non è possibile poiché nessuno esiste & Quot;

Wait? NON PUOI? http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis

Non posso mostrarti " verità " Ho un programma tanto quanto non posso mostrarti & Quot; verità & Quot; sulla lingua. Entrambe sono rappresentazioni della nostra comprensione empirica del mondo. Non su & Quot; verità & Quot ;. Mettendo da parte tutte le incomprensioni, posso dimostrarti matematicamente che un algoritmo di fusione ordinerà gli elementi in un elenco con prestazioni O (nlogn), che un Dijkstra troverà il percorso più breve su un grafico ponderato o che l'algoritmo di Euclide ti troverà il migliore divisore comune tra due numeri. Il & Quot; verità nel mio programma & Quot; in quest'ultimo caso forse ti troverò il più grande divisore comune tra due numeri, non credi?

Con un'equazione di ricorrenza posso delinearti come funziona il tuo programma Fibonacci.

Ora, la programmazione al computer è un'arte? Sono sicuro che lo sia. Tanto quanto la matematica.

Non vengo da un background matematico, quindi perdona la mia ignoranza, ma cosa significa " per dimostrare un programma " significare? Cosa stai provando? La correttezza? La correttezza è una specifica che il programma deve verificare per essere & Quot; correct & Quot ;. Ma questa specifica è decisa da un essere umano e come si verifica che questa specifica sia corretta?

A mio avviso, ci sono bug in programma perché gli umani hanno difficoltà ad esprimere ciò che vogliono veramente. alt text http://www.processdevelopers.com/images/PM_Build_Swing.gif

Allora, cosa stai dimostrando? Bug causati dalla mancanza di attenzione?

Inoltre, quali sono gli assiomi della programmazione? Le verità atomiche del campo?

Ho tenuto un corso chiamato Programmazione basata sul contratto (homepage del corso: http: // www.daimi.au.dk/KBP2/ ). Ecco cosa posso estrapolare dal corso (e da altri corsi che ho seguito)

Devi definire formalmente (matematicamente) la semantica della tua lingua. Pensiamo a un semplice linguaggio di programmazione; uno che ha solo variabili globali, ints, int array, arithmetic, if-then-else, while, assegnazione e do-nothing [probabilmente puoi usare un sottoinsieme di qualsiasi linguaggio tradizionale come " implementazione " ; di questo].

Uno stato di esecuzione sarebbe un elenco di coppie (nome della variabile, valore della variabile). Leggi & Quot; {Q1} S1 {Q2} & Quot; come " l'esecuzione dell'istruzione S1 ti porta dallo stato di esecuzione Q1 allo stato Q2 " ;.

Un assioma sarebbe quindi "if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}". Cioè, se l'istruzione S1 ti porta dallo stato Q1 a Q2 e l'istruzione S2 ti porta da Q2 a Q3, quindi & Quot; S1; S2 quot &; (S1 seguito da S2) ti porta dallo stato Q1 allo stato Q3.

Un altro assioma sarebbe "if {Q1 && e != 0} S1 {Q2} and {Q1 && e == 0} S2 {Q2}, then {Q1} if e then S1 else S2 {Q2}".

Ora, un po 'di raffinatezza: i Qn in {} sarebbero in realtà dichiarazioni su stati, non stati stessi.

Supponi che M (out, A1, A2) sia un'istruzione che fa una fusione di due array ordinati e memorizza il risultato in out, e che tutte le parole che utilizzo nell'esempio successivo sono state espresse formalmente (matematicamente). Quindi "{sorted(A1) && sorted(A2)} A := M(A1, A2) {sorted(A) && permutationOf(A, A1 concatened with A2)}" è l'affermazione che M implementa correttamente l'algoritmo di unione.

Si può provare a dimostrarlo usando gli assiomi sopra (probabilmente ne sarebbero necessari alcuni altri. Probabilmente avrai bisogno di un ciclo, per uno).

Spero che questo illustri un po 'di come potrebbero apparire i programmi di prova corretti. E fidati di me: ci vuole molto molto di lavoro, anche per algoritmi apparentemente semplici, per dimostrarli corretti. Lo so, ho letto molti tentativi ;-)

[se leggi questo: il tuo hand-in andava bene, sono tutti gli altri che mi hanno causato mal di testa ;-)]

Certo che possono, come altri hanno pubblicato.

Fornire una subroutine molto piccola corretta è un buon esercizio che IMHO ogni studente universitario in un corso di laurea relativo alla programmazione dovrebbe essere necessario . Ti dà una grande idea nel pensare a come rendere il tuo codice chiaro, facilmente revisionabile e gestibile.

Tuttavia, nel mondo reale è di uso pratico limitato.

Innanzitutto, proprio come i programmi hanno dei bug, così come le prove matematiche. In che modo dimostrare che una dimostrazione matematica è davvero corretta e non presenta errori? Non puoi. E per contro-esempio, qualsiasi numero di prove matematiche pubblicate ha avuto errori scoperti in esse, a volte anni dopo.

In secondo luogo, non è possibile dimostrare che un programma sia corretto senza avere "a priori" una definizione inequivocabile di ciò che il programma dovrebbe fare. Ma qualsiasi definizione inequivocabile di cosa dovrebbe fare un programma è un programma. (Sebbene possa trattarsi di un programma in una sorta di linguaggio di specifica per il quale non si dispone di un compilatore.) Pertanto, prima di poter dimostrare che un programma è corretto, è necessario disporre di un altro programma equivalente e conosciuto in anticipo per essere corretti. Quindi QED è tutto inutile.

Consiglierei di rintracciare il classico " Nessun proiettile d'argento " articolo di Brooks.

C'è molta ricerca in questo settore .. come altri hanno già detto, i costrutti all'interno di un linguaggio di programma sono complessi, e questo peggiora solo quando si cerca di convalidare o provare per ogni dato input.

Tuttavia, molte lingue consentono specifiche, su quali input sono accettabili (condizioni preliminari) e consentono anche di specificare il risultato finale (condizioni post).

Tali lingue includono: B, Evento B, Ada, fortran.

E, naturalmente, ci sono molti strumenti progettati per aiutarci a dimostrare determinate proprietà sui programmi. Ad esempio, per dimostrare la libertà di deadlock, si potrebbe sgretolare il loro programma tramite SPIN.

Esistono anche molti strumenti che ci aiutano a rilevare errori logici. Questo può essere fatto tramite analisi statiche (goanna, satabs) o esecuzione effettiva del codice (gnu valgrind?).

Tuttavia, non esiste uno strumento che consenta davvero di provare un intero programma, dall'avvio (specifica), all'implementazione e alla distribuzione. Il metodo B si avvicina, ma il suo controllo dell'implementazione è molto debole. (Si presume che gli esseri umani siano infalibili nella traduzione di speicficaiton in impianto).

Come nota a margine, quando usi il metodo B, ti troverai spesso a costruire prove complesse da assiomi più piccoli. (E lo stesso vale per altri esagerati dimostratori di teoremi).

Possono. Ho trascorso molte, molte ore come matricola del college facendo prove di correttezza del programma.

La ragione per cui non è pratico su una scala macro è che scrivere una prova di un programma tende ad essere molto più difficile che scrivere il programma. Inoltre, i programmatori oggi tendono a costruire sistemi, non a scrivere funzioni o programmi.

Su micro scala, a volte lo faccio mentalmente per singole funzioni e tendo ad organizzare il mio codice per renderli facilmente verificabili.

C'è un famoso articolo sul software dello space shuttle. Fanno prove o qualcosa di equivalente. È incredibilmente costoso e richiede tempo. Tale livello di verifica può essere necessario per loro, ma per qualsiasi tipo di società di software commerciale o di consumo, con le tecniche attuali, il tuo pranzo verrà consumato da un concorrente che offre una soluzione al 99,9% all'1% del costo. Nessuno pagherà $ 5000 per un MS Office che è leggermente più stabile.

Se stai cercando fiducia, l'alternativa alla dimostrazione dei programmi è testarli. Questo è più facile da capire e può essere automatizzato. Inoltre, consente la classe di programmi per i quali le prove matematiche non sono matematicamente possibili, come descritto sopra.

Soprattutto, nessuna prova è un sostituto per superare i test di accettazione: *

Solo perché un programma fa davvero quello che dice di fare, non significa che fa ciò che l'utente vuole che faccia.
- Salvo puoi dimostrare che ciò che dice di fare è ciò che l'utente dice di voler.
  - Che poi devi dimostrare è ciò che vogliono davvero , perché, essendo un utente, quasi sicuramente non sanno cosa vogliono. ecc. Reductio ad absurdum.

* per non parlare di unità, copertura, funzionalità, integrazione e tutti gli altri tipi di test.

Spero che questo ti aiuti nel tuo cammino.

Qualcosa che non è stato menzionato qui è il B - Metodo che è un sistema formale basato sul metodo. È stato utilizzato per sviluppare il sistema di sicurezza della metropolitana di Parigi. Sono disponibili strumenti per supportare lo sviluppo di B e Event B, in particolare Rodin .

Non solo puoi provare i programmi, ma puoi anche lasciare che il tuo computer costruisca programmi da prove. Vedi Coq . Quindi non devi nemmeno preoccuparti della possibilità di aver fatto un errore nella tua implementazione.

Teoremi di Godel nonostante ... Quale sarebbe il punto ? Che semplicistico & Quot; verità & Quot; ti piacerebbe provare? Cosa vorresti derivare da quelle verità? Mentre posso mangiare queste parole ... dov'è la praticità?

I programmi POSSONO essere provati.È abbastanza semplice se li scrivi in un linguaggio come ad esempio Standard ML del New Jersey (SML/NJ).

La tua affermazione è ampia, quindi sta catturando molti pesci.

La linea di fondo è: alcuni programmi possono sicuramente essere dimostrati corretti. Tutti i programmi non possono essere dimostrati corretti.

Ecco un esempio banale che, sia chiaro, è esattamente lo stesso tipo di prova che ha distrutto la teoria degli insiemi nel passato: crea un programma in grado di determinare se è corretto, e se scopre che è corretto, fornisce una risposta errata.

Questo è G & # 246; teorema di del, chiaro e semplice.

Ma questo non è così problematico, dal momento che possiamo dimostrare molti programmi.

Supponiamo che un linguaggio puramente funzionale (cioè Haskell). Gli effetti collaterali possono essere presi abbastanza chiaramente in considerazione in tali lingue.

Dimostrando che un programma produce il giusto risultato è necessario specificare:

una corrispondenza tra tipi di dati e insiemi matematici
una corrispondenza tra le funzioni di Haskell e le funzioni matematiche
un insieme di assiomi che specifica quali funzioni ti è permesso di costruire dagli altri e la corrispondente costruzione sul lato matematico.

Questo insieme di specifiche è chiamato semantica denotazionale . Ti consentono di dimostrare la ragione dei programmi che usano la matematica.

La buona notizia è che " struttura dei programmi " (punto 3 sopra) e la " struttura degli insiemi matematici " sono abbastanza simili (la parola d'ordine è topos , o categoria chiusa cartesiana ), quindi 1 / le prove che fai sul lato matematico saranno facilmente trasferite in costruzioni programmatiche 2 / il i programmi che scrivi vengono facilmente dimostrati matematicamente corretti.

Leggi il problema di arresto (che riguarda la difficoltà di provare qualcosa di così semplice come se un programma sia completato o meno). Fondamentalmente il problema è legato a G & # 246; teorema di incompletezza di del.

Alcune parti dei programmi possono essere provate. Ad esempio, il compilatore C # che verifica staticamente e garantisce la sicurezza dei tipi, se la compilazione ha esito positivo. Ma sospetto che il nocciolo della tua domanda sia dimostrare che un programma funziona correttamente. Molti algoritmi (non oserei dire di più) possono essere dimostrati corretti, ma un intero programma probabilmente non può essere dimostrato staticamente a causa di quanto segue:

La verifica richiede che vengano attraversate tutte le possibili filiali (chiamate, if e interupts), che nel codice di programma avanzato ha una complessità temporale super-cubica (quindi non verrà mai completata entro un tempo ragionevole).
Alcune tecniche di programmazione, attraverso la creazione di componenti o l'utilizzo di reflection, rendono impossibile prevedere staticamente l'esecuzione del codice (ovvero non sai come un altro programmatore utilizzerà la tua libreria e il compilatore fa fatica a prevedere in che modo la riflessione in un consumatore invocherà funzionalità.

E quelli sono solo alcuni ...

Se il programma ha un obiettivo ben definito e ipotesi iniziali (ignorando Godel ...) può essere provato. Trova tutti i numeri primi, x, per 6 & Lt; = x & Lt; = 10, la tua risposta è 7 e questo può essere provato. Ho scritto un che riproduce NIM (il primo programma Python Ho mai scritto) e in teoria il computer vince sempre dopo che il gioco cade in uno stato in cui il computer può vincere. Non sono stato in grado di dimostrarlo come vero, ma è vero (matematicamente con una prova di somma binaria digitale) credo a meno che non abbia fatto un errore nel codice. Ho fatto un errore, sul serio, qualcuno può dirmi se questo programma è battibile?

Ci sono alcuni teoremi matematici che sono stati " provato " con codice del computer come il teorema dei quattro colori . Ma ci sono obiezioni, perché come hai detto, puoi provare il programma?

Inoltre, quali sono gli assiomi della programmazione? Le verità atomiche del campo?

I codici operativi sono " verità atomiche " ;? Ad esempio, vedere ...

mov ax,1

... un programmatore non potrebbe affermare come assiomatico che, salvo un problema hardware, dopo aver eseguito questa affermazione il registro ax della CPU conterrebbe ora 1?

Se si scrive un programma per computer, come è possibile prendere precedenti lavori comprovati e usarli per mostrare la verità del proprio programma?

Il " opera precedente " quindi potrebbe essere l'ambiente di runtime in cui viene eseguito il nuovo programma.

Il nuovo programma può essere dimostrato: oltre alle prove formali, può essere dimostrato " mediante ispezione " e con varie forme di " testing " (incluso " testing di accettazione ").

Come si dimostra un Picasso?

Se il software è più simile al design industriale o all'ingegneria che all'arte, una domanda migliore potrebbe essere " come si dimostra un ponte o un aeroplano? "

la dimostrazione di un programma corretto può essere eseguita solo in relazione alle specifiche del programma; è possibile ma costoso / che richiede tempo

alcuni sistemi CASE producono programmi più suscettibili alle prove di altri - ma ancora una volta, ciò si basa su una semantica formale delle specifiche ...

... e quindi come si dimostrano le specifiche corrette? Destra! Con più specifiche!

Ho letto un po 'su questo, ma ci sono due problemi.

Innanzitutto, non puoi provare qualcosa di astratto chiamato correttezza. Se le cose sono impostate correttamente, puoi dimostrare che due sistemi formali sono equivalenti. Puoi provare che un programma implementa una serie di specifiche ed è più semplice farlo costruendo la prova e il programma più o meno in parallelo. Pertanto, le specifiche devono essere sufficientemente dettagliate per fornire qualcosa da dimostrare, e quindi le specifiche sono effettivamente un programma . Il problema di scrivere un programma per soddisfare uno scopo diventa il problema di scrivere una specifica formale dettagliata di un programma per soddisfare uno scopo, e questo non è necessariamente un passo avanti.

Secondo, i programmi sono complicati. Quindi sono le prove della correttezza. Se riesci a commettere un errore durante la scrittura di un programma, puoi sicuramente provare. Dijkstra e Gries mi dissero, in sostanza, che se fossi un matematico perfetto avrei potuto essere un buon programmatore. Il valore qui è che la dimostrazione e la programmazione sono due processi di pensiero leggermente diversi, e almeno nella mia esperienza commetto diversi tipi di errori.

Nella mia esperienza, provare i programmi non è inutile. Quando sto cercando di fare qualcosa che posso descrivere formalmente, dimostrando che l'implementazione corretta elimina molti errori difficili da trovare, principalmente lasciando quelli stupidi, che posso facilmente cogliere nei test. Su un progetto che deve produrre un codice estremamente privo di bug, può essere un'aggiunta utile. Non è adatto a tutte le applicazioni e sicuramente non è un proiettile d'argento.

Come altri hanno sottolineato, è possibile dimostrare (alcuni) programmi.

Un problema in pratica, tuttavia, è che per prima cosa hai bisogno di qualcosa (cioè un'ipotesi o un teorema) che vuoi dimostrare. Quindi, per provare qualcosa su un programma, devi prima una descrizione formale di ciò che dovrebbe fare (ad es. Pre e post-condizioni).

In altre parole, è necessaria una specifica formale del programma. Ma ottenere anche una specifica ragionevole (molto meno rigorosa formale) è già una delle cose più difficili nello sviluppo del software. Pertanto è generalmente molto difficile provare interessanti su un programma (reale).

Vi sono tuttavia alcune cose che possono essere (e sono state) più facilmente formalizzate (e provate). Se riesci almeno a dimostrare che il tuo programma non si bloccherà, è già qualcosa :-).

A proposito, alcuni avvisi / errori del compilatore sono essenzialmente (semplici) prove su un programma. Ad esempio, il compilatore Java dimostrerà che non accederai mai a una variabile non inizializzata nel tuo codice (altrimenti ti darà un errore del compilatore).

Non ho letto tutte le risposte, ma il modo in cui la vedo, dimostrando i programmi è inutile, ecco perché nessuno lo fa.

Se hai un progetto relativamente piccolo / medio (diciamo, 10K righe di codice), allora la prova sarà probabilmente anche 10k righe, se non di più.

Pensaci, se il programma può avere dei bug, la prova può anche avere " bugs " ;. Forse avrai bisogno di una prova per la prova!

Un'altra cosa da considerare, i programmi sono molto formali e precisi. Non puoi essere più rigoroso e formale, perché il codice del programma deve essere eseguito da una macchina molto stupida.

Mentre le prove saranno lette dagli umani, quindi tendono ad essere meno rigorose del codice reale.

Le uniche cose che vorresti dimostrare sono algoritmi di basso livello che operano su strutture dati specifiche (ad es. quicksort, inserimento in un albero binario, ecc.)

Queste cose sono piuttosto complicate, non è immediatamente ovvio il motivo per cui funzionano e / o se funzioneranno sempre. Sono anche elementi di base per tutti gli altri software.

La maggior parte delle risposte si è concentrata sulla pratica e va bene: in pratica non ti interessa la correzione formale. Ma cosa c'è in teoria?

I programmi possono essere dimostrati proprio come un'istruzione matematica. Ma non nel senso che intendevi! In qualsiasi abbastanza potente framework, ci sono dichiarazioni matematiche (e programmi) che non possono essere provate! Vedi qui

Tanto rumore qui, ma ho intenzione di urlare nel vento comunque ...

" Dimostrare " corrette; ha significati diversi in contesti diversi. In sistemi formali , & Quot; dimostrare corretto & Quot; significa che una formula può essere derivata da altre formule comprovate (o assiomatiche). " Dimostrare " corretto; nella programmazione mostra semplicemente che il codice equivale a una specifica formale. Ma come si dimostrano corrette le specifiche formali? Sfortunatamente, non c'è modo di mostrare che una specifica sia priva di bug o di risolvere qualsiasi problema del mondo reale se non attraverso i test.

Solo i miei 2 centesimi, aggiungendo alle cose interessanti già lì.

Di tutti i programmi che non possono essere dimostrati, i più comuni sono quelli che eseguono IO (alcune interazioni imprevedibili con il mondo o gli utenti). Anche le prove automatiche a volte dimenticano solo che & Quot; comprovato & Quot; & Programmi quot; gira su hardware fisico, non su quello ideale descritto dal modello.

Dall'altro lato, le prove matematiche non tengono molto al mondo. Una domanda ricorrente con la matematica è se descrive qualcosa di reale. Viene sollevato ogni volta che viene inventato qualcosa di nuovo come numeri immaginari o spazio non euclideo. Quindi la domanda viene dimenticata poiché queste nuove teorie sono strumenti così validi. Come un buon programma, funziona e basta.

Autorizzato sotto: CC-BY-SA insieme a attribuzione

Non affiliato a StackOverflow