Funzione Composizione Funzione VS Applicazione

Question

1. Qualcuno può dare un esempio di composizione di funzione?

2. Questa è la definizione di operatore di composizione di funzione?

   (.) :: (b -> c) -> (a -> b) -> a -> c 
   f . g = \x -> f (g x) 
   

Questo dimostra che ci vogliono due funzioni e restituire una funzione, ma mi ricordo che qualcuno ha espresso la logica in inglese come

ragazzo è umano -> ali è ragazzo -> Ali è umano

1. Cosa questa logica correlava alla composizione delle funzioni?
2. Qual è il significato del forte legame tra applicazione e composizione della funzione e quale è il legame più forte dell'altro?

Si prega di aiutare.

Grazie.

Answer 1

(Edit 1: ho perso un paio di componenti della sua domanda la prima volta intorno, vedere il fondo della mia risposta.)

Il modo di pensare a questo tipo di dichiarazione è quello di esaminare i tipi . La forma di argomentazione che hai è chiamata sillogismo; tuttavia, penso che stai ricordando male qualcosa. Esistono molti tipi diversi di sillogismi, e il tuo, per quanto posso dire, non corrisponde alla composizione della funzione. Consideriamo una specie di sillogismo che fa:

1. Se c'è il sole, mi scalderò.
2. Se divento caldo, andrò a nuotare.
3. Pertanto, se c'è il sole, andrò a nuotare.

Questo è chiamato hypothetical syllogism. In termini logici, scriveremo come segue: let S stand per la proposizione "è soleggiato", let H stand per la proposizione "I'll get hot", e lasciare W stand per la proposizione "Andrò a nuotare".Scrivendo α → β per "α implica β", e scrivendo ∴ per "dunque", siamo in grado di tradurre il precedente per:

1. S → H
2. H → W
3. ∴ S → W

Naturalmente, questo funziona se si sostituisce S, H e W con qualsiasi arbitraria α, β e γ. Ora, questo dovrebbe sembrare familiare. Se cambiamo il → implicazione freccia alla funzione freccia ->, questo diventa

1. a -> b
2. b -> c
3. ∴ a -> c

ed ecco, abbiamo i tre componenti del tipo dell'operatore di composizione! Per pensare a questo come un sillogismo logico, si potrebbe prendere in considerazione quanto segue:

1. Se ho un valore di tipo a, posso produrre un valore di tipo b.
2. Se si ha un valore di tipo b, è possibile produrre un valore di tipo c.
3. Pertanto, se ho un valore di tipo a, posso produrre un valore di tipo c.

Questo dovrebbe dare un senso: in f . g, l'esistenza di una funzione g :: a -> b ti dice che premessa 1 è vero, e f :: b -> c ti dice che premessa 2 è vero. Pertanto, è possibile concludere l'istruzione finale, per la quale la funzione è un testimone.

Non sono del tutto sicuro di cosa si traduca il tuo sillogismo. È quasi un'istanza di modus ponens, ma non del tutto. Gli argomenti di Modus Ponens hanno la seguente forma:

1. Se piove, allora mi bagnerò.
2. Sta piovendo.
3. Pertanto, mi bagnerò.

scrittura R per "piove", e W per "Mi metterò bagnato", questo ci dà la forma logica

1. R → W
2. R
3. ∴ W

Sostituzione della freccia implicazione con la freccia la funzione ci dà la seguente:

1. a -> b
2. a
3. ∴ b

E questo è semplicemente funzione di applicazione, come abbiamo può vedere dal tipo di ($) :: (a -> b) -> a -> b. Se si vuole pensare a questo come un argomento logico, potrebbe avere la forma

1. Se ho un valore di tipo a, posso produrre un valore di tipo b.
2. Ho un valore di tipo a.
3. Pertanto, Posso produrre un valore di tipo b.

Qui, considerare l'espressione f x. La funzione f :: a -> b è un testimone della verità della proposizione 1; il valore x :: a è un testimone della verità della proposizione 2; e quindi il risultato può essere di tipo b, dimostrando la conclusione. È esattamente ciò che abbiamo trovato dalla prova.

Ora, il sillogismo originale ha la seguente forma:

1. Tutti i ragazzi sono umani.
2. Ali è un ragazzo.
3. Pertanto, Ali è umano.

Trasformiamo questo in simboli. Bx indicherà che x è un ragazzo; Hx indicherà che x è umano; a indicherà Ali; e ∀ x. φ afferma che φ è vero per tutti i valori di x.Poi abbiamo

1. ∀ x. Bx → Hx
2. Ba
3. ∴ Ha

Questo è quasi modus ponens, ma richiede un'istanza del forall. Sebbene logicamente valido, non sono sicuro di come interpretarlo a livello di sistema di tipi; se qualcuno vuole dare una mano, sono tutto orecchie. Un'ipotesi sarebbe un tipo di grado 2 come (forall x. B x -> H x) -> B a -> H a, ma sono quasi sicuro che sia sbagliato. Un'altra ipotesi sarebbe un tipo più semplice come (B x -> H x) -> B Int -> H Int, dove Int sta per Ali, ma di nuovo, sono quasi sicuro che sia sbagliato. Di nuovo: se lo sai, per favore fatemelo sapere!

E un'ultima nota. Guardare le cose in questo modo, seguendo la connessione tra prove e programmi, porta alla magia profonda dello Curry-Howard isomorphism, ma questo è un argomento più avanzato. (E 'davvero cool, però!)

---

Edit 1: Avete chiesto anche per un esempio di composizione di funzione. Ecco un esempio. Supponiamo che io abbia una lista di nomi medi delle persone. Ho bisogno di costruire una lista di tutte le iniziali centrali, ma per farlo devo prima escludere ogni secondo nome inesistente. È facile escludere tutti quelli il cui secondo nome è nullo; abbiamo solo include tutti il ​​cui secondo nome è non null con filter (\mn -> not $ null mn) middleNames. Allo stesso modo, possiamo facilmente ottenere l'iniziale media di qualcuno con head, e quindi abbiamo semplicemente bisogno di map head filteredMiddleNames per ottenere l'elenco. In altre parole, abbiamo il seguente codice:

allMiddleInitials :: [Char] 
allMiddleInitials = map head $ filter (\mn -> not $ null mn) middleNames 

Ma questo è irritantemente specifico; vogliamo davvero una funzione di generazione iniziale centrale. Quindi cambiamo questo in uno:

getMiddleInitials :: [String] -> [Char] 
getMiddleInitials middleNames = map head $ filter (\mn -> not $ null mn) middleNames 

Ora, diamo un'occhiata a qualcosa di interessante. La funzione map ha il tipo (a -> b) -> [a] -> [b] e dal head ha il tipo [a] -> a, map head ha il tipo [[a]] -> [a]. Allo stesso modo, filter ha tipo (a -> Bool) -> [a] -> [a] e quindi filter (\mn -> not $ null mn) ha tipo [a] -> [a]. Così, possiamo sbarazzarci del parametro, e invece scrivere

-- The type is also more general 
getFirstElements :: [[a]] -> [a] 
getFirstElements = map head . filter (not . null) 

e si vede che abbiamo un'istanza bonus di composizione: not è di tipo Bool -> Bool, e null ha digitare [a] -> Bool, così not . null ha tipo [a] -> Bool: si prima controlla se la lista data è vuota, e poi restituisce se è non è. Questa trasformazione, a proposito, ha cambiato la funzione in point-free style; cioè, la funzione risultante non ha variabili esplicite.

Hai anche chiesto informazioni su "binding forte". Quello a cui penso si riferisce è la precedenza degli operatori . e $ (e probabilmente anche l'applicazione di funzione).In Haskell, proprio come nell'aritmetica, alcuni operatori hanno una precedenza più alta di altri, e quindi si legano più strettamente. Ad esempio, nell'espressione 1 + 2 * 3, questo viene analizzato come 1 + (2 * 3). Questo perché in Haskell, i seguenti dichiarazioni sono in vigore:

infixl 6 + 
infixl 7 * 

Maggiore è il numero (il livello di precedenza), prima che tale operatore è chiamato, e quindi il più strettamente l'operatore lega. L'applicazione della funzione ha effettivamente una precedenza infinita, quindi si lega più strettamente: l'espressione f x % g y verrà analizzata come (f x) % (g y) per qualsiasi operatore %. Il . (composizione) e $ operatori (applicazione) hanno le seguenti dichiarazioni fissità:

infixr 9 . 
infixr 0 $ 

livelli di precedenza vanno da zero a nove, così che cosa dice questo è che l'operatore . lega più strettamente di qualsiasi altro (tranne l'applicazione di funzione), e lo $ lega meno meno. Pertanto, l'espressione f . g $ h verrà analizzata come (f . g) $ h; e infatti, per la maggior parte degli operatori, f . g % h sarà (f . g) % h e f % g $ h sarà f % (g $ h). (Le uniche eccezioni sono i rari pochi altri zero o nove operatori di precedenza.)