I linguaggi funzionali sono una sorta di derivazione del programma?

Question

I linguaggi funzionali sono una sorta di derivazione del programma?

#1 da (2 voti)
#2 da (1 voti)
#3 da (0 voti)

1

La derivazione del programma è definita come la derivazione di un programma dalle sue specifiche. Di solito questo linguaggio di specificazione è una qualche forma di logica proposizionale, ma da quello che capisco, non è necessario. Per ragioni di specificità, ho a che fare solo con linguaggi puramente funzionali come Haskell qui.

Quando scrivi un programma in Haskell, non stai descrivendo come il calcolo è fatto, ma quali sono . Ad esempio, in questa funzione che produce i numeri di Fibonacci, viene fornita una specifica per i numeri di Fibonacci, non come dovrebbe essere implementata la funzione.

fib :: int -> int
fib n = (fib n-1) + (fib n-2)
fib 1 = 1
fib 0 = 1

Per far funzionare questo codice, il compilatore Haskell deve convertire questa specifica dichiarativa della funzione in un codice macchina imperativo. Non è questa per definizione una derivazione del genere?

haskell programming-logic formal-methods

posta Nathan BeDell 19.06.2014 - 18:15

fonte

3 risposte

Leggi altre domande sui tag haskell programming-logic formal-methods

Algoritmo per il rilevamento di finestre in una stanza URI e rappresentazione di risorse e risorse

score 2 · Answer 1

Il codice Haskell può certamente essere letto come descrizione di come eseguire il calcolo (la macchina STG è fondamentalmente un linguaggio funzionale in stile Haskell semplificato, più esplicito ma con semantica di esecuzione diretta ed evidente). Ma sì, la lettura più comune è quella dichiarativa e la programmazione dichiarativa è più vicina alle specifiche formali dei linguaggi imperativi.

Tuttavia, dovresti estendere le definizioni di derivazione del programma per includere la programmazione funzionale al suo interno. Per esempio, se si chiama qualsiasi tipo di trasformazione da una lingua a un codice macchina, allora anche un compilatore C è uno strumento di derivazione del programma. In secondo luogo, la maggior parte dei linguaggi funzionali non sono in alcun modo linguaggi di specifica : il codice è scritto per rendere evidente che viene calcolato piuttosto che come, ma continua a compitare il calcolo ( anche se lo fa in termini diversi da, ad esempio, C, e forse lascia più spazio per le ottimizzazioni del compilatore) piuttosto che lasciare che il compilatore cerchi un programma. Le distinzioni sono sfocate, ma le persone tendono a tracciare la linea da qualche parte tra Haskell e la logica proposizionale completa.

score 1 · Answer 2

Per ricavare un programma significa scrivere una specifica formale, che di solito non è eseguibile, e quindi applicare matematicamente corretta regole per ottenere un programma eseguibile che soddisfi tale specifica. Questo descrive un compilatore, in pratica.

Haskell è un linguaggio di programmazione che utilizza regole matematiche per aiutarti a verificare la correttezza del programma. uno strumento che ti aiuta a ricavare un programma. Devi ancora eseguire il processo di derivazione, entro i confini del linguaggio di programmazione.

La nozione che stai descrivendo quali sono le cose, piuttosto che come è fatto il calcolo, è ciò che significa dichiarativo vs imperativo . La programmazione imperativa è la programmazione in piccolo, specificando una ricetta; una serie di passaggi. La programmazione dichiarativa è quella in cui essenzialmente dici al computer quello che vuoi, e capisce come farlo.

La programmazione dichiarativa è caratterizzata da trasparenza referenziale, correttezza matematica, mancanza di effetti collaterali, pigrizia e concorrenza; tutte le cose che Haskell eccelle.

score 0 · Answer 3

Se è possibile generare algoritmicamente codice macchina imperativo dalle specifiche, allora la tua specifica è, per definizione, un programma stesso - molto probabilmente un linguaggio specifico di dominio.

Che dire del contrario, un programma è una specifica? Parte della definizione di una specifica è probabilmente comprensibile per l'uomo che cosa fa e perché lo fa. Chiaramente questo è abbastanza sfocato. Quali umani, quale grado di comprensione? Probabilmente la natura dichiarativa dei linguaggi funzionali li rende più comprensibili agli umani, ma lo stato delle cose oggi è che la maggior parte dei programmatori ha più familiarità con i linguaggi imperativi e li capisce meglio, quindi è piuttosto difficile prenderlo come un fatto provato.