TIL
přednáška 2
Marie Duží
http://www.cs.vsb.cz/duzi/

Sémantické schéma
n Výraz
n        vyjadřuje
n
n     označuje Význam (konstrukce)
n        konstruuje
n
n denotát
qOntologie TIL: rozvětvená hierarchie typů

Základní pojmy
nKonstrukce
qProměnné x, y, p, w, t, … v-konstruují
qTrivializace 0X dodá objekt X
qKompozice [F A1 … An] aplikace funkce
qUzávěr [lx1…xn X] konstrukce funkce
qProvedení 1X, Dvojí provedení 2X
nJednoduchá teorie typů
qBáze: {o, i, t, w}
qFunkcionální typy: (ab1…bn)
nParciální funkce (b1 ´… ´ bn) ® a

Základní pojmy
nDenotát chápeme vždy jako funkci, včetně nulárních funkcí (atomické entity jako čísla, individua)
nDenotát může být:
q(PWS-)intense: (aw), nejčastěji ((at)w), zkráceně atw
qExtense: funkce, jejíž doména není w
qKonstrukce
qnic (parcialita)
nTypické extense:
qMnožiny jsou extense typu (oa)
qRelace jsou extense typu (oab)
nTypické intense:
qVlastnosti individuí/(oi)tw, individuové úřady (role)/itw, propozice/otw, vztahy mezi
individui/(oii)tw, atributy/(ab)tw …

Základní pojmy, notace
nVýrokově-logické spojky implikace (É), konjunkce (Ù), disjunkce (Ú) a ekvivalence (º) jsou funkce
typu (ooo),
negace (Ø) je typu (oo).
qPro spojky užíváme infixní notaci bez Trivializace.
qTak např. místo [0Ù [0É p q] [0Øq]] můžeme psát
[[p É q] Ù Øq].
nPro a-identity, tj. relace =a /(oaa), budeme rovněž používat infixní notaci bez vyznačení indexu
typu a.
qNapř. nechť =i/(oii) je identita individuí, =((ot)w)/(ootwotw) identita propozic; a, b ®v i, P
®v (oi)tw. Pak místo
q[0É [0=i a b] [0=((ot)w) [lwlt [Pwt a]] [lwlt [Pwt b]]]]
q budeme většinou psát prostě
q [[a = b] É [lwlt [Pwt a] = lwlt [Pwt b]]].

Základní pojmy, notace
nKvantifikátory (totální funkce) "a, $a / (o(oa)).
qJe-li x ®v a, B ®v o, tedy lx B(x) ®v (oa), pak
q[0"a lx B(x)] konstruuje T, pokud lx B(x) konstruuje celý typ a, jinak F,
q[0$a lx B(x)] konstruuje T, pokud lx B(x) konstruuje neprázdnou množinu prvků typu a, jinak F.
qNotace: "x B(x), $x B(x)
nSingularizátory (parciální funkce) Ia / (a(oa)).
q[0Ia lx B(x)] konstruuje jediný a-prvek množiny konstruované lx B(x), pokud je to jednoprvková
množina (singleton), jinak nedefinován.
qNotace: ix B(x) čteme „to jediné x, že B“

Příklad
n„ten jediný člověk, který zaběhl 100 m pod 9 s“
qMan/(oi)tw, Time/(t(ot)): délka časového intervalu, Run/(oit)tw, I/(i(oi)): ten jediný…, celý
výraz ozn. itw.
qlwlt [0I lx [[0Manwt x] Ù [0Time lt [0Runwt x 0100]] < 09]]
q      (oi)     i          (oit)   i     t
q   (t(ot)) (ot) o
q           t         (ott) t
q (i(oi)) o    (ooo) o
q        (oi)
q   i
q itw

Rozvětvená teorie typů
nT1 (typy řádu 1) – neprocedurální objekty, jednoduchá teorie typů
nCn (konstrukce řádu n)
nNechť x je proměnná, která v-konstruuje objekty typu řádu n. Pak x je konstrukce řádu n nad B.
nNechť X je prvek typu řádu n. Pak 0X, 1X, 2X jsou konstrukce řádu n nad B.
nNechť X, X1, ..., Xm (m > 0) jsou konstrukce řádu n nad B. Pak
[X X1... Xm] je konstrukce řádu n nad B.
nNechť x1, ..., xm, X (m > 0) jsou konstrukce řádu n nad B. Pak
[lx1...xm X] je konstrukce řádu n nad B.
nNic jiného …
nTn+1 (typy řádu n + 1)
n Nechť *n je kolekce všech konstrukcí řádu n nad B.
n*n a každý typ řádu n jsou typy řádu n + 1 nad B.
nJsou-li a, b1,...,bm (m > 0) typy řádu n + 1 nad B, pak (a b1 ... bm), tj. kolekce parciálních
funkcí, je typ řádu n + 1 nad B.
nNic jiného …

Příklady, notace: C/a ®v b
n0+/*1 ® (ttt), x /*1 ®v t
n[0+ x 01]/*1 ®v t
nlx [0+ x 01]/*1 ®v (tt) funkce následníka
n[lx [0+ x 01] 05] /*1 ®v t číslo 6
n[0: x 00]/*1 ®v t nic
nlx [0: x 00]/*1 ®v (tt)  degenerovaná funkce
nNechť Improper je množina konstrukcí řádu 1, které jsou v-nevlastní pro každou valuaci v. Tedy
Improper je extenzionální objekt typu (o*1), což je typ řádu 2.
qPak [0Improper 0[0: x 00]] /*2 ® o
je prvek *2, což je typ řádu 3, i když konstruuje  pravdivostní hodnotu P, což je objekt typu řádu
1.

Příklady, notace: C/a ®v b
nNechť Aritmetic je množina unárních aritmetických funkcí definovaných na přirozených číslech, tedy
Aritmetic je objekt typu (o(nn)), a nechť proměnná x ®v n, kde n je typ přirozených čísel.
nPak Kompozice [0Aritmetic [lx [0+ x 01]]] patří do *1, což je typ řádu 2, a konstruuje T, protože
Uzávěr [lx [0+ x 01]] konstruuje unární funkci následníka, což je aritmetická funkce.

Příklady, notace: C/a ®v b
nKompozice [0Aritmetic 2c]/*3 ®v o v-konstruuje pravdivostní hodnotu T, pokud proměnná c/*2
®v *1 v-konstruuje např. Uzávěr [lx [0+ x 01]].
qDvojí Provedení 2c v-konstruuje to, co je v-konstruováno tímto Uzávěrem, a to je aritmetická
funkce následníka.
qKompozice [0Aritmetic 2c] je objekt patřící do *3, což je typ řádu 4;
qproměnná c v-konstruuje Uzávěr [lx [0+ x 01]] typu *1, a proto c patří do *2, což je typ řádu 3.
qDvojí provedení zvyšuje řád konstrukce, proto 2c je prvek typu *3, což je typ řádu 4. Tedy celá
Kompozice
[0Aritmetic 2c] patří do *3, typu řádu 4.

Empirické výrazy
nEmpirické výrazy označují netriviální (nekonstantní) intense
n„francouzský král“, „prezident ČR“, „nejvyšší hora na světě“ označují úřady typu itw, a aktuálně
referují (v daném w a t, což ale není záležitost logiky, nýbrž empirických faktů) po řadě k ničemu,
k Miloši Zemanovi a k Mount Everest.
nPredikáty jako „být studentem“, „být vysoký“, „být veselý“, „být 60 let starý“ označují vlastnosti
typu (oi)tw a referují ke své populaci, tj. množině individuí, kteří jsou aktuálně studenty,
vysocí, veselí a staří 60 let.
nOznamovací věty jako „Praha je větší než Brno“ označují propozice typu otw a referují
k pravdivostní hodnotě (daná věta k T).
nTedy uvedené výrazy jsou empirické v tom smyslu, že to, k čemu referují v daném stavu světa, je
již mimo oblast logické analýzy a může být zjišťováno pouze empirickým zkoumáním stavu světa
v daném čase.

Analytické výrazy
nAnalytické výrazy označují extense nebo triviální (konstantní) intense
nJejich extensi můžeme určit pouze na základě porozumění výrazu, bez zkoumání stavu světa.
nMatematické a logické výrazy jsou analytické, označují extense
nVýrazy, které obsahují empirické podvýrazy, jsou analytické, pokud označují konstantní intense.
Tedy referovaný objekt je analyticky nutně, tj. ve všech w a t jeden a tentýž.
n„Žádný starý mládenec není ženatý“
n„Velryby jsou savci“

Omezené kvantifikátory
nVšichni studenti jsou chytří.
nNěkteří studenti jsou líní.
qlwlt "x [[0Studentwt x] É [0Chytrýwt x]]
qlwlt $x [[0Studentwt x] Ù [0Línýwt x]]
q Toto nejsou doslovné analýzy, odporují tzv. „Parmenidovu principu“ a naší metodě analýzy: věty
nezmiňují ", $, É, Ù.
nAll, Some, No, Most, … / ((o(oi))(oi))
n[0All M], kde M ®v (oi), v-konstruuje množinu všech nadmnožin množiny M
n[0Some M], kde M ®v (oi), v-konstruuje množinu všech těch množin, které mají neprázdný průnik s M
n[0No M], kde M ®v (oi), v-konstruuje množinu všech množin, které jsou disjunktní s M
n lwlt [[0All 0Studentwt] 0Chytrýwt]
n lwlt [[0Some 0Studentwt] 0Línýwt]

Analytické výrazy
n“No bachelor is married”  ® TRUE
nBachelor, Married/(oi)tw; No/((o(oi))(oi))
nlwlt [[0No 0Bachelorwt] 0Marriedwt]
nDefinujme a zjemňujme:
nm, n/*1 ®v (oi), x ®v i:
0No = lm ln Ø$x [[m x] Ù [n x]], [[0No m] n] = Ø$x [[m x] Ù [n x]].
n0Bachelor = lwlt lx [Ø[0Marriedwt x] Ù [0Manwt x]].
q(být neženatý a být muž jsou rekvizity vlastnosti být starý mládenec)
n[[0No 0Bachelorwt] 0Marriedwt] =
Ø[0$ lx [[0Bachelorwt x] Ù [0Marriedwt x]]] =
Ø[0$ lx [Ø[0Marriedwt x] Ù [0Manwt x] Ù [0Marriedwt x]]].
qv-konstruuje T pro libovolnou valuaci v, protože třída v-konstruovaná lx [Ø[0Marriedwt x] Ù
[0Manwt x] Ù [0Marriedwt x]] je prázdná, proto můžeme generalizovat:
n"w"t Ø$x [Ø[0Marriedwt x] Ù [0Manwt x] Ù [0Marriedwt x]].

Analytické vs. empirické výrazy
nNutně, 8 > 5
nPočet planet = 8
n           ¾¾¾¾¾¾¾¾¾¾¾ ???
nNutně, počet planet > 5
n"w"t [0> 08 05]    (analyticky nutně)
nlw lt [[0Počet 0Planetwt] = 08]   (empiricky, náhodně)
n¾¾¾¾¾¾¾¾¾¾¾¾¾¾
nlw lt [0> [0Počet 0Planetwt] 05]     (empiricky, náhodně)
nPočet/(t(oi)): počet prvků množiny, Planet/(oi)tw, >, =/(ott)
qDk.:
1)[0> 08 05] 1. premisa, "E
2)[[0Počet 0Planetwt] = 08] 2. premisa, lE
3)[0> [0Počet 0Planetwt] 05] 1, 2 Leibniz
4)lwlt [0> [0Počet 0Planetwt] 05] 3, lI

Práce s parcialitou, v-nevlastní konstrukce
nChybné typování
qJestliže X není konstrukce řádu n (n ³ 1), pak 1X je nevlastní;
qJestliže X není konstrukce řádu n (n ³ 2), pak 2X je nevlastní;
qJestliže X, X1, …, Xn nejsou konstrukce vyhovující typově Definici, pak [X X1…Xn] je nevlastní,
nekonstruuje nic.
qPř.: 1Tom, 15, lwlt [0Studentwt 05], 2[lwlt [0Studentwt 0Tom]]
nAplikace funkce f na argument a takový, že f je nedefinována na a
q[0: x 00] je v-nevlastní pro každou valuaci v
qlx [0: x 00] není nevlastní, konstruuje degenerovanou funkci
q0[0: x 00] není nevlastní, konstruuje [0: x 00]
q[0Improper 0[0: x 00]] konstruuje T
nImproper/(o*1): třída konstrukcí v-nevlastních pro každou valuaci v.

Parcialita a kompozicionalita
n„Jestliže pět děleno nulou je pět, pak Tom je papež“
qoznačuje degenerovanou propozici, která je všude nedefinována!
nlwlt [[[0: 05 00] =t 05] É [0Tom = 0Papežwt]] ® otw.
q0, 5/t; :/(ttt); Tom/i; Papež/itw; [0: 05 00] ® t; [[0: 05 00] = 05] ® o; 0Tom ® i; 0Papežwt ®v i;
[0Tom = 0Papežwt] ®v o; [[[0: 05 00] = 05] É [0Tom = 0Papežwt]] ®v o.
qRelaci =t není na co aplikovat, tedy spojka implikace neobdrží první argument, proto je celá
Kompozice nevlastní, nekonstruuje nic. Parcialita je propagována nahoru. Uzávěr – degenerovaná
propozice

Parcialita a kompozicionalita
nPokud intuitivně cítíme, že danou větou chtěl mluvčí naznačit to, že není pravda, že pět děleno
nulou je pět, tedy že věta by mohla být pravdivá, pak musíme analyzovat tuto větu:
n „Jestliže je pravda, že pět děleno nulou je pět, pak Tom je papež“.
nTrue*/(o*n): třída těch konstrukcí, které v-konstruují T pro všechny valuace v.
n[0True* 0C] konstruuje T, právě když C v-konstruuje T pro libovolnou valuaci v, jinak F.
n lwlt [[0True* 0[[0: 05 00] = 05]] É [0Tom = 0Papežwt]] ® otw - konstruuje propozici TRUE.
n Věta je analyticky pravdivá

Parcialita a kompozicionalita
nFalse*/(o*n) a Improper*/(o*n) jsou třídy konstrukcí v-konstruujících F resp. v-nevlastních pro
všechny valuace v:
n[0True* 0C] = Ø[0False* 0C] Ù Ø[0Improper* 0C]
n[0False* 0C] = Ø[0True* 0C] Ù Ø[0Improper* 0C]
n[0Improper* 0C] = Ø[0True* 0C] Ù Ø[0False* 0C]
nPodobně budeme často potřebovat vlastnosti propozic True, False, Undef/(ootw)tw
n2.října
n

Pravidlo b-transformace
qZákladní výpočtové pravidlo l-kalkulů a funkcionálních programovacích jazyků
qurčuje, jak provést operaci aplikaci funkce f na argument A za účelem získání hodnoty funkce f na
A.
nPř.: [lx [0+ x 01] 03] – chci hodnotu funkce následníka na čísle 3:
nb-redukce (někdy také l-redukce) „jménem“:
[lx [0+ x 01] 03] Þ [0+ 03 01] (= 04)
nb-rozvinutí (nebo také l-rozvinutí):
n [0+ 03 01] Þ [lx [0+ x 01] 03]
nRedukce obecně: [[lx1…xm Y] D1…Dm]┣ Y(Di/xi)

b-conversion: [lx C(x) A] |¾ C(A/x)
n Procedure of applying the function presented by
lx C(x) to an argument presented by A.
nThe fundamental computational rule of l-calculi and functional programming languages
nThe fundamental inference rule of HOL
q ‘by name’; the procedure A is substituted for all the occurrences of x
qnot operationally equivalent
q ‘by value’; the value presented by A is substituted for all the occurrences of x

b-conversion: [lx C(x) A] |¾ C(A/x)
nIn programming languages the difference between ‘by value’ and ‘by name’ revolves around the
programmer’s choice of evaluation strategy.
qAlgol’60: “call-by-value” and “call-by-name”
qJava: manipulates objects “by name”, however, procedures are called “by-value”
qClean and Haskell: “call-by-name”
nSimilar work has been done since the early 1970s; for instance, Plotkin (1975) proved that the two
strategies are not operationally equivalent.
nChang & Felleisen (2012)’s call-by-need reduction by value. But their work is couched in an
untyped l-calculus.

 [lx C(x) A] |¾ C(A/x)
nConversion by name à three problems.
1.conversion of this kind is not guaranteed to be an equivalent transformation as soon as partial
functions are involved.
2.even in those cases when b-reduction is an equivalent transformation, it can yield a loss of
analytic information of which function has been applied to which argument
3.In practice less efficient than ‘by value’

Problems with b-reduction ‘by name’
n1) non-equivalence
n[lx [ly [0+ x y]] [0Cotg 0p]]
n is an improper construction; it does not construct anything, because there is no value of the
cotangent function at p
n but its b-reduced Composition
n[ly [0+ [0Cotg 0p] y]]
n constructs a degenerate function
nThe improper construction [0Cotg 0p] has been drawn into the intensional context of the Closure
[ly [0+ x y]].

b-conversion by name:
  2) loss of analytic information
n[lx [x + 1] 3]
n
n b  [3 + 1]
n
n[ly [3 + y] 1]
qwhich function has been applied to which argument?
qNo ‘backward path’. Does it matter?
n

Problems with b-reduction
n2) Loss of analytic information
n“John loves his wife, and so does Peter”
à exemplary husbands (sloppy reading)
n“loving one’s own wife” vs. “loving John’s wife”
nLown (John): lwlt [lx [0Lovewt x [0Wife_ofwt x]] 0John]
nLJohn (John): lwlt [lx [0Lovewt x [0Wife_ofwt 0John]]
    0John]
nBoth b-reduce to LJohn (John):
n lwlt [0Lovewt 0John [0Wife_ofwt 0John]]
n“so does Peter”
nPeter loves John’s wife à trouble on the horizon

b-conversion by name: loss of info
n(1) lwlt [lx [0Lovewt x [0Wife_ofwt 0John]] 0John]
n(2) lwlt [lx [0Lovewt x [0Wife_ofwt x]] 0John]
n
n(3) lwlt [0Lovewt 0John [0Wife_ofwt 0John]]
nIt is uncontroversial that the contractum (3) can be equivalently expanded back both to (1) and
(2).
nThe problem is, of course, that there is no way to reconstruct which of (1), (2) would be the
correct redex

Does it matter?
nHOL tools are broadly used in automatic theorem checking and applied as interactive proof
assistants.
nThe underlying logic is usually a version of simply typed l-calculus of total functions.
nHowever, there is another application à natural language processing à hyperintensional logic is
needed so that the underlying inference machine is neither over-inferring (that yields
inconsistencies) nor under-inferring (that causes lack of knowledge).
nagents’ attitudes like knowing, believing, seeking, solving, designing, etc., because attitudinal
sentences are part and parcel of our everyday vernacular.

Hyperintensionality
nwas born out of a negative need, to block invalid inferences
qCarnap (1947, §§13ff); there are contexts that are neither extensional nor intensional (attitudes)
qCresswell; any context in which substitution of necessary equivalent terms fails is
hyperintensional
nYet, which inferences are valid in hyperintensional contexts?
nHow hyper are hyperintensions? à procedural isomorphism
nWhich contexts are hyperintensional?
nTIL definition is positive: a context is hyperintensional if the very meaning procedure is an
object of predication; TIL is a hyperintensional, partial typed l-calculus
30

b-reduction by value
n[lx C(x) A] |– C(A/x)
qunderspecified:
nHow to execute C(A/x)?
a)‘by name’: construction A is substituted for x à problems
b)‘by value’: execute A first, and only if it does not fail, substitute (a pointer to) the produced
value for x – substitution method à bingo, no problems !!! J

Substitution ‘by value’
n[lx F(x) A] = 2[0Sub [0Tr A] 0x 0F(x)]
q
1.A: execute A in order to obtain the value a; if A is v-improper, then the whole Composition is
v-improper (stop); else:
2.[0Tr A]: obtain Trivialization of (“pointer at”) the argument a
3.[0Sub [0Tr A] 0x 0F]: substitute this Trivialization for x into ‘the body’ F
4.2[0Sub [0Tr A] 0x 0F]: execute the result

Substitution ‘by value’
nSub/(*n*n*n*n) operuje na konstrukcích takto:
n[0Sub C1    C2       C3]
n            co   za_co   kam
n Nechť C1 v-konstruuje konstrukci D1,
n C2 v-konstruuje konstrukci D2,
n C3 v-konstruuje konstrukci D3,
n konstruuje konstrukci D, která vznikne korektní substitucí D1 za D2 do D3
nTr/(*n a) v-konstruuje Trivializaci a-objektu
n[0Tr x] v-konstruuje Trivializaci objektu v-konstruovaného proměnnou x, x je volná
n0x konstruuje x bez ohledu na valuaci, proměnná x je
o-vázaná

Substitution ‘by value’
nPříklad
n[0Sub [0Tr 0p] 0x 0[0Sin x]]
n konstruuje konstrukci [0Sin 0p]
n2[0Sub [0Tr 0p] 0x 0[0Sin x]]
n konstruuje hodnotu funkce Sinus na p,
tj. číslo 0
n[0Sub [0Tr y] 0x 0[0Sin x]]
n v(p/y)-konstruuje konstrukci [0Sin 0p]
n

Substitution method; broadly applied
nApplication of a function to an argument
(b-reduction by value)
nExistential quantification into hyperintensional contexts
nHyperintensional attitudes de re
nAnaphoric preprocessing
nTopic/focus articulation; presuppositions;
active vs. passive

Substitution method; broadly applied
nde re attitudes
nTilman believes of the Pope that he is wise
n
n lwlt [0Believewt 0Tilman 2[0Of [0Tr 0Popewt] 0he
0[lw*lt* [0Wisew*t* he]]]
n
nOf = Sub operates on the (hyper)intensional context of “that he is wise”

Substitution method; broadly applied
nQuantifying into …
nTom is seeking the last decimal of p
n ¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾
n There is a number such that Tom is seeking its last decimal
n
nlwlt [0Seek*wt 0Tom 0[0Last_Dec 0p]]
n ¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾
n lwlt [0$lx [0Seek*wt 0Tom
                    [0Sub [0Tr x] 0y 0[0Last_Dec y]]]]

How hyper are hyperintensions �
  procedural isomorphism
nMaybe that it is philosophically wise to adopt several notions of procedural isomorphism.
nIt is not improbable that several degrees of hyperintensional individuation are called for,
depending on which sort of discourse happens to be analysed.
nWhat appears to be synonymous in an ordinary vernacular might not be synonymous in a professional
language like the language of logic, mathematics, computer science or physics.

Procedural isomorphism
nOrdinary vernacular – no l-bound variables �
n(A1’’’): a-conversion + b-conversion by value
n + restricted b-conversion by name;
[lx [0+ x 00] y] à [0+ y 00]
n + pairs of simple synonyms
nProgramming language – variables matter �
n(A0’): a-conversion + pairs of simple synonyms