29/01/2020, 17:31
29/01/2020, 20:35
arnett ha scritto:1. Credo che questo si faccia usando che ${0,1}$ sta in Dyn,
\(\mathbb N\) è l'algebra iniziale dell'endofuntore \(\_\sqcup 1 : \sf Set \to Set\).2. Ma questo non crea un problema di circolarità? L'affermazione che $(\NN, s, 0)$ sta in Dyn segue dal teorema di ricorsività, che però è provato usando anche l'induzione.
Sistemi \(\sf Dyn\)amici. Un insieme \(f : X \to X\) con un endomorfismo fissa l'orbita di un monoide, quello degli endomorfismi di \(X\) che agisce su \(X\) con le iterate di \(f\); se vuoi, esiste un unico omomorfismo di monoidi \(\Phi_f : \mathbb N \to \text{End}(X)\) tale che \(\Phi_f(n)=f^{\circ n}\).3. "Dyn" per cosa sta?
30/01/2020, 15:09
Non è importante saperlo; hai chiesto se si crea una circolarità nella definizione, la risposta era per dirti: no, non mi pare. Del resto, cosa intendi per "dimostrare" che \(\mathbb N\) è un oggetto di \(\sf Dyn\)? Un oggetto di \(\sf Dyn\) è un insieme puntato con un endomorfismo. \(\mathbb N\) è definito daMi spiace, non so cosa sia l'algebra di un endofuntore, argh, e di conseguenza non capisco come questo si leghi alla domanda che ho fatto.
data (N : Set) where
Z : N
Suc : N -> N
Z : N
e Suc : N -> N
sono proprio l'elemento distinto e l'endomorfismo in questione.
10/02/2020, 15:24
13/02/2020, 07:44
Sì e c'hai ragione. Solo che la richiesta è un'altra, essenzialmente: fai tabula rasa di ciò che già sai e per te ora \(\mathbb N\) è l'oggetto iniziale di \(\mathbf{Dyn}\). Sono impostazioni diverse: in una il principio di induzione è assioma e questa dimostra la proprietà di ricorsione, mentre qui è assioma la proprietà di ricorsione e con questa dimostri il principio di induzione.arnett ha scritto:Che $\NN$ stia in Dyn non presuppone altro che il dato dell'insieme con la mappa di successivo e lo zero; ma il fatto che $\NN$, così strutturato, sia iniziale in Dyn non dipende dall'induzione? Cioè il fatto che in Dyn ci sia una sola freccia che esce da $\NN$ non si dimostra per induzione?
13/02/2020, 17:10
impostazioni diverse: in una il principio di induzione è assioma e questa dimostra la proprietà di ricorsione, mentre qui è assioma la proprietà di ricorsione e con questa dimostri il principio di induzione.
01/05/2020, 09:34
01/05/2020, 12:57
01/05/2020, 16:43
01/05/2020, 17:14
Skuola.net News è una testata giornalistica iscritta al Registro degli Operatori della Comunicazione.
Registrazione: n° 20792 del 23/12/2010.
©2000—
Skuola Network s.r.l. Tutti i diritti riservati. — P.I. 10404470014.
Powered by phpBB © phpBB Group - Privacy policy - Cookie privacy
phpBB Mobile / SEO by Artodia.