Come evitare l'overflow dello stack o l'errore di segmentazione in Coqnness?

Attualmente sto lavorando con vellvm, sviluppando una trasformazione su di esso. Sono un principiante coq.Come evitare l'overflow dello stack o l'errore di segmentazione in Coqnness?

Durante la programmazione, ho affrontato il seguente avviso:

Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).

La mia funzione che genera questo avviso calcola una firma. La firma è divisa in bit superiori e inferiori. Dato due nats n1 e n2 che rappresentano i bit superiori e i bit inferiori, calcola (n1 * 65536) + n2 - questa è un'astrazione per mettere due numeri binari di 16 bit affiancati.

Sono rimasto piuttosto sorpreso perché la definizione di coq nat sembra gestire grandi intro dall'esterno, grazie al costruttore S.

Come evitare questa avvertenza/utilizzare numeri grandi in coq? Sono aperto a cambiare l'implementazione da nat a qualche tipo di costruzione binaria.

Grazie!

fonte

2012-12-01 fotanus

Lavorare con nats è crufty, perché sono costruiti con 'S', il che significa che ogni numero sarà * letteralmente * una sequenza di applicazioni' S': si potrebbe invece lavorare con numeri interi, che hanno principi di prova simili ma hanno un sign/magnitude (bit) rappresentazione basata: http://coq.inria.fr/library/Coq.ZArith.BinInt.html –

Come posso utilizzare le operazioni allora? (Zpos 1) + (Zpos 2) non sembra funzionare ... - Errore: il termine "1% Z" ha tipo "|" mentre si prevede che abbia tipo "nat". – fotanus

perché "+" significa più cose a seconda di dove ti trovi. In realtà "+" è solo zucchero sintattico per l'aggiunta di nats, dove 'plus' è definito in modo struttural su due nats. Si vuole usare il 'più' per i numeri interi, che vive in un _interpretation scope_ diverso rispetto a' nat' (ovvero, 'Int_scope'). Leggi informazioni sugli ambiti di interpretazione e su come aprirli e usarli. –

Invece di utilizzare il tipo nat in Coq, è a volte (quando si deve manipolare i grandi numeri) meglio utilizzare il tipo di Z, che è una formalizzazione di interi che utilizzano una rappresentazione segno coppia di grandezza. Il compromesso è che le tue dimostrazioni potrebbero essere leggermente più complesse; nat è molto semplice e ammette quindi semplici principi di prova.

Tuttavia, in Coq c'è un ampio uso della notazione per semplificare la scrittura di definizioni, teoremi e dimostrazioni. Coq ha un kernel estremamente piccolo (lo vogliamo perché vogliamo essere in grado di credere che il correttore di prove sia corretto, e possiamo leggerlo) con un sacco di annotazioni su di esso. Tuttavia, poiché vi sono diverse rappresentazioni di cose e solo pochi buoni simboli, i nostri simboli si scontrano in genere. Per superare questo, coq utilizza interpretation scopes per disambiguare i simboli e risolverli in nomi (perché "+" significa add, plus, ecc.).

Lei ha ragione, utilizzando Z_scope è dove, + per plus all'interno Z.

fonte

2012-12-01 20:05:20

Come evitare l'overflow dello stack o l'errore di segmentazione in Coqnness?

risposta

Problemi correlati