Kääntöportti (symboli)

Portti
⊢
◄ ⊞ ⊟ ⊠ ⊡ ⊢ ⊣ ⊤ ⊥ ⊦ ►
Ominaisuudet
Nimi oikea takki
Unicode U+22A2
HTML-koodi ⊢ tai ⊢
UTF-16 0x22A2
URL-koodi %E2%8A%A2
Muistitekniikka ⊢
⊢

Kääntöportti  – Matemaattisessa logiikassa ja tietojenkäsittelytieteessä symbolia kutsutaan "kääntöportiksi", koska se muistuttaa ylhäältä katsottuna tyypillistä kääntöporttia . Sitä kutsutaan myös nimellä "tee" ja sitä luetaan usein "antaa", "todistaa", "tyydyttää" tai "aiheuttaa".

TeX :ssä kääntöportin symboli saadaan komennolla \ vdash . Unicodessa kääntöportin merkkiä ( \vdash ) kutsutaan "oikeaksi painikkeeksi" ja se on koodipaikassa U+22A2 [1] . Koodipaikkaa U+22A6 kutsutaan vahvistusmerkiksi ( \vdash ). Kirjoituskoneessa kääntöportti voi koostua pystypalkista (|) ja viivasta (-). LaTeX :ssä on turnstile-paketti, joka tuottaa tämän merkin monissa tapauksissa ja pystyy sijoittamaan merkkejä sen ala- tai yläpuolelle oikeisiin paikkoihin. [2]

Merkitys

Kääntöportti on binäärirelaatio . Sen tulkinta on erilainen eri yhteyksissä:

:

voidaan lukea: "Tiedän, että A on totta".

Samaan tapaan ehdollinen lausunto :

voidaan lukea näin:

" P :stä tiedän, että Q " tarkoittaa, että Q on johdettavissa P :stä järjestelmässä. Johdatettavuuden käytön mukaan, jota seuraa lauseke ilman mitään edeltävää se tarkoittaa lausetta , eli lauseke voidaan johtaa säännöistä käyttämällä tyhjää aksioomijoukkoa . Sellaisenaan ilmaisu tarkoittaa, että Q on järjestelmän lause. tarkoittaa, että S on todistettavissa T :stä . [5] Tämä käyttö on esitelty lauselogiikkaa käsittelevässä artikkelissa . Todistettavuuden syntaktinen seuraus tulee asettaa vastakkain semanttiselle seuraukselle, joka on merkitty kaksoiskierrosmerkillä . Se sanoo, että se on semanttinen seuraus , tai , kun kaikki mahdolliset arvioinnit , jotka ovat tosia, ovat myös tosia. Propositiologiikassa voidaan osoittaa, että semanttinen seuraus ja johdettavuus ovat toistensa ekvivalentteja. Toisin sanoen lauselogiikka on tervettä ( implis ) ja täydellistä ( impliks ). [6]

Funktorin G kanssa . [9] Harvemmissa tapauksissa kääntöporttia ( ), kuten kohdassa , käytetään osoittamaan, että funktori G on suoraan funktorin F vieressä . [kymmenen]

  • APL : ssä symbolia kutsutaan "oikeaksi tackiksi" ja se edustaa ambivalenttia oikeaa identiteettifunktiota, jossa ja , ja ovat . Käänteistä symbolia kutsutaan "vasemmaksi tackiksi" ja se edustaa samanlaista vasenta identiteettiä, jossa  on ja  on . [11] [12]
  • Kombinatoriikassa tarkoittaa , että se on luvun osio . [13]
  • Hewlett - Packardin HP-41C ja HP-42S -sarjojen laskimissa FOCAL-merkistössä olevaa merkkiä (koodipisteessä 127) kutsutaan nimellä "Lisää merkki" ja sitä käytetään osoittamaan, että seuraavat merkit lisätään alfarekisteriin sen sijaan, että ne korvaisivat rekisterin nykyisen sisällön. Tätä merkkiä tuetaan myös (koodikohdassa 148) muissa HP:n laskimissa käytetyn HP Roman -fontin muunnelmassa .
  • Casion fx - 92 College 2D- ja fx-92+ Speciale College -sarjan laskimissa [14] symboli tarkoittaa moduulioperaattoria ; näyttöön tulee syöte , jossa Q on osamäärä ja R on jäännös . Muissa CASIO-laskimissa (kuten belgialaisissa muunnelmissa - fx-92B Speciale College- ja fx-92B College 2D-laskimet [15] - joissa desimaalierotin esitetään pisteellä pilkun sijaan), modulo-operaattori merkitään .

Katso myös

Muistiinpanot

  1. ↑ Unicode-standardi . Haettu 16. toukokuuta 2021. Arkistoitu alkuperäisestä 13. toukokuuta 2011.
  2. ↑ CTAN Kattava TEX-arkistoverkko, hakemisto - makrot/lateksi/contrib/turnstile . Haettu 16. toukokuuta 2021. Arkistoitu alkuperäisestä 17. toukokuuta 2021.
  3. ↑ Martin-Lof, 1996 , s. 6, 15
  4. ↑ Luku 6, Muodollinen kieliteoria . Haettu 16. toukokuuta 2021. Arkistoitu alkuperäisestä 4. huhtikuuta 2018.
  5. ↑ Troelstra & Schwichtenberg, 2000
  6. ↑ Dirk van Dalen, Logic and Structure (1980), Springer, ISBN 3-540-20879-8 . Katso luku 1, kohta 1.5.
  7. ↑ Peter Selinger, Lecture Notes on the Lambda Calculus . Haettu 16. toukokuuta 2021. Arkistoitu alkuperäisestä 6. toukokuuta 2021.
  8. ↑ Schmidt, 1994
  9. ↑ adjoint Functor nLabissa . Haettu 16. toukokuuta 2021. Arkistoitu alkuperäisestä 13. toukokuuta 2021.
  10. ↑ FunctorFact. Functor Fact Twitterissä . [twiitti] . Twitter (5. heinäkuuta 2016) .
  11. ↑ Iverson, APL sanakirja . Haettu 16. toukokuuta 2021. Arkistoitu alkuperäisestä 25. huhtikuuta 2020.
  12. ↑ Iverson, 1987
  13. ↑ Stanley, Richard P. Enumeratiivinen kombinatoriikka. – 1. - Cambridge: Cambridge University Press, 1999. - Voi. Voi. 2. - s. 287.
  14. ↑ fx-92 Speciale College Mode d'emploi . - CASIO COMPUTER CO., LTD., 2015. - S. 12. Arkistoitu 16. huhtikuuta 2021 Wayback Machinessa
  15. ↑ Jäännöslaskelmat - Casio fx-92B:n käyttöopas [Sivu 13 | ManualsLib] . www.manualslib.com . Haettu 24. joulukuuta 2020. Arkistoitu alkuperäisestä 16. toukokuuta 2021.

Linkit