Freccia doppia in giù in LaTeX (\Downarrow)

Dove si usa

Traccia una freccia a doppio tratto verso il basso, usata per la valutazione big-step nella semantica dei linguaggi di programmazione.

La semantica operazionale scrive e \Downarrow v per dire che l'espressione e si valuta nel valore v in stile big-step, il principale uso tecnico di questo simbolo. Nei diagrammi e nelle dimostrazioni logiche può indicare un passo di inferenza verticale. Come le altre frecce verticali, \Downarrow è un delimitatore, quindi \Big\Downarrow ne dà una versione più alta. Non confondetelo con \downarrow, che nella stessa semantica può indicare la terminazione. Definite la vostra convenzione quando introducete il giudizio. La semantica small-step, invece, usa \to o \longrightarrow per i singoli passi di riduzione e \to^* per la loro chiusura riflessiva e transitiva.

Esempio minimo compilabile

Incollalo in un file .tex vuoto e compilalo con pdfLaTeX, XeLaTeX o LuaLaTeX.

\documentclass{article}
\begin{document}
Down Arrow (Double): $\Downarrow$

\[ \frac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v} \]
\end{document}

Simboli correlati

• Freccia bidirezionale\leftrightarrow
• Freccia doppia lunga a destra\Longrightarrow
• Freccia bidirezionale lunga\longleftrightarrow
• Freccia doppia lunga a sinistra\Longleftarrow
• Freccia su e giù\updownarrow
• Freccia doppia in su\Uparrow

Domande frequenti

Come si scrive Freccia doppia in giù in LaTeX?

Scrivi \Downarrow in modalità matematica, per esempio $\frac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v}$. Funziona in LaTeX standard senza caricare alcun pacchetto.

Quale pacchetto serve per \Downarrow?

Nessuno. \Downarrow fa parte di LaTeX standard, quindi compila con la sola classe del documento nel preambolo.

Posso usare \Downarrow in modalità testo o solo in modalità matematica?

Solo in modalità matematica. Fuori da $...$ LaTeX si ferma con "Missing $ inserted", quindi nel testo scrivi $\Downarrow$. Se ti serve solo il glifo nel testo, incolla invece il carattere Unicode ⇓ (con XeLaTeX o LuaLaTeX e un font che lo contenga).