#rC3 Type theory and meaning in linguistics

rc3 hacc preroll music

Herald: All right, we are back again from
the HACC or about:future studios on the

rc3 remote Congress 3 this year sadly
remote so we'll do as we can. We have a

really nice talk coming up here about type
theory in linguistics and about meaning in

linguistics. From daherb. He will be
talking about the uses of type theory in

both programing languages and natural
languages and maybe draw, like,

similarities between them. He has a PhD in
computer science, was in Sweden for 6 years

at a university and is now back in
Germany. There is sadly no translation for

this talk because there aren't enough
angels to do all the translation work.

There is a pixelflut behind me. It's my
own implementation. So if you want to spam

me, you can. I'm not sure if it will work,
but apart from that, I think that's enough

of introduction. Let's go to daherb.

daherb: Thanks, and a little bit about me:
I would call myself a computational

linguist, even though my Ph.D. officially
just says computer science. And I see

myself in the tradition of this slightly
outdated xkcd where people try to use

computers to test linguistic theories. In
addition to that, I spent my time in

Sweden in a very well known functional
programming group and basically next to a

research group dedicated to type theory.
So my interests are both into functional

programming, and I got a little bit spoiled
also by type theory. And that inspired me

to give this talk. And to start: The
question is what is meaning in natural

language? So I came up with a few
examples, example sentences. And the

question is: what is the meaning of these
sentences? But before we dive into that, a

little bit about linguistics. So there are
several subdisciplines in linguistics: one

is syntax, which is mostly people drawing
trees. And people are really good at

drawing trees these days. On the slide,
you can see various formalisms, how people

draw trees, and that's pretty well
established these days. But that's

basically: what are valid sentences in a
language? The next question is: what is

the meaning of these sentences? And within
linguistics, for a long time, semantics

was something you would not really try to
approach because it's really, really

difficult. But actually, semantics is the
literal meaning, and in addition to

semantics, we might have the meaning in
context. So this is a very great example

of so-called pragmatics. Question: your
greatest weakness? Answer of the person:

interpreting semantics of a question, but
ignoring the pragmatics. Could you give an

example? Yes. So in this example, the
person only looked at the literal meaning.

Can you give an example? Yes, I can give
an example. Not interpreted as the request

to actually give an example. So we have
the literal meaning and decide that we

even have an additional meaning in
context. So if we look at statements in

natural language, we might have challenges
in interpreting: what do they mean?

All men are mortal. Every man is mortal.

That we can interpret
pretty literal. Yesterday it was raining.

Tomorrow it will be raining. The first one
could be a literal fact. The one about the

future. Who knows? Then there are
statements about things that could

potentially happen. It could be raining.
Then there are statements which in our

world could never actually happen, like
John is searching for a unicorn. It's

pretty much a matter of fact that there
are no real life unicorns. So if John is

searching for a unicorn, we don't really
claim that there might be unicorns in our

world. And then we have questions like,
could you pass me the salt where we don't

really have the literal meaning or we
don't care about the literal meaning, we

don't care if the answer is yes or no.
What we actually – what the person

making the statement actually means is,
please hand me the salt. Please pass me

the salt. And in addition, there is kind
of an assumption that there is actually

salt on the table. But we don't really
assume that if John is searching for a

unicorn, that there is a unicorn, if
someone asks the question, can you pass me

the salt? there is actually salt on the
table. So meaning is a very philosophical

problem. And why do people care about it?
There are relevant questions, for example,

when are two statements equivalent, when
do they mean the same? "All men are

mortal" Does it mean the same as every man
is mortal? Or the more challenging "I saw

the morning star", "I saw the evening
star" "I saw Venus". As a matter of fact,

these three are meaning exactly the same,
but if someone says, I saw the morning

star, do we know that they actually also
know that they saw Venus, that the morning

star is the same as Venus? And another
relevant question is, when does one

statement follow from other statements?
And especially in computational

linguistics, we want to find automatic
ways to decide these questions. There are

a few more examples. So there is a very
well-known example: all men are mortal,

Socrates is a man. So we should come to
the conclusion that Socrates is also

mortal. Or more challenging: every
European, has the right to live in Europe.

Every European is a person. Every person
who has the right to live in Europe can

travel freely in Europe. Can we answer
the question, can every European travel

freely within Europe? and hopefully find
some way to answer this question with yes.

Humans are – People are usually pretty
good at deciding that with a little bit of

logic and a lot of intuition. But
computers are really bad about intuition.

So we are interested in models or ways
that actually also work for computers. And

these days there are basically two big
branches: the one the formal approaches.

And the other are the statistical
approaches. The formal approaches use

logic to try to answer the questions,
while the statistical approaches, just

look at plenty of data, I shouldn't say
"just", they use a lot of data to answer

the questions we are interested
in. In this talk, I will only focus on the

formal approaches because I like them
more. But both approaches, both kinds of

approaches have the right to exist and can
be also very helpful in their own way. So,

back to the kind of the title of the talk
now slightly paraphrased: type theory and

semantics. And there are basically two big
approaches to type theory. OK, what is

type theory? In computer science type
theory is the study of what systems of

types exist and how, what properties do
they have? We will shortly see what

that could mean. So that … If we go back
in history, then there are simply typed

languages. They go back to Alonzo
Church. I think in 1940 he described the

simply typed lambda calculus. And then a
few decades later, a guy called Richard

Montague used this approach or adopted
this approach, which was purely from logic

to natural languages. And Richard Montague
was a very particular person. He was … he

had a great influence, but also he was not
an easy person, he openly attacked

colleagues and … but his influence on
linguistics started in the 70s. There are

still people trying to work out details
about his theory. Now we come to the

one answer: what is meaning in
linguistics? And that's so-called truth

conditional or model theoretic semantics.
So, what is the meaning of the sentences

like "all men are mortal". And the meaning
of this sentence is: can we come up with a

model which is kind of a picture of a
world that makes this sentence true? And

here in the picture, we have an example of
that: we have the set of all mortal

things. And we have the set of all men in
our world, and they are a subset, meaning

everything that's a man is also a mortal
thing. And then we have the second

sentence, which says "Socrates is a man",
which means we know that Socrates is one

of these objects in the set of all men.
And then is the question "is Socrates

mortal?", and because we know that all men
are in the set of mortal things, we can

answer this question quite easily with
yes. So one approach to meaning of natural

language is: can we find a world in which
all the properties are in a way that all

the sentences we are given are true?
And because we look at models, it's called

model theoretic semantics. And the big
influence of Montague was … As I mentioned

before, there was already the theory by
Alonzo Church of the simply typed lambda

calculus, which was an approach in logic,
and then there came around Montague and

made the statement, this very bold
statement: "There is, in my opinion, no

important theoretical difference between
natural languages and the artificial

languages of logicians. Indeed, I consider
it possible to comprehend the syntax and

semantics of both kinds of languages that
think a single natural and mathematically

precise theory". And that's a really bold
statement, because we know that usually if

we, for example, look at programming
languages, they are very small and very

well-defined compared to what we can
express in natural languages. But yeah, he

made the statement and then he started to
demonstrate that this is actually

possible. Then, let's look a bit at times,
and I called this a simply typed language,

and we can give … We have infinitely many
types, and every object in our

logic language has a
type. And the type is either e for an

entity, t for truth value, or if we have
some type alpha, and some other type beta,

then we have this pair <alpha,beta>, which
is a type. And then logicians like to be

very precise and they say "nothing else is
the type in this language". And. That's,

again, rather abstract. Let's look at some
examples. We have certain classes of words

in our language. For example, we have
names. And they … our examples are, for

example, John and Mary, and we have the
semantic type e, which is a basic type,

and then we have intransitive verbs, which
means verbs that don't take a direct

object like "sleeps" or transitive groups
that have a direct object like "love". And

then we have sentences and they have the
semantic type t, which is as a computer

scientist, I would call it boolean. It's a
truth value. It's either true or false.

And intransitive verbs have this type of a
pair ("e to t"), which, for example,

could interpret as a function from
entities to truth values. And then I have a

few examples down here. So what's in this
double square brackets? That's our natural

language. And what's not in italics, not
in these double square brackets, that's our

logic language. So for simple things like
the name John, we just claim that there's

some object representing John, we call it
just "j". The same for Mary and also "sleeps"

and "love", we translate to just some
object in our logic language. But what are

these exactly? There are two ways to look at
them: sleep' ("sleep prime"), for example,

is either the set of all objects that are
sleeping in our world. For example, the

set only consisting of only having the
element John or j representing John. So

John is the only sleeping entity in our
world, or we can represent it as a

function from entities to truth values and
the function returns true, if x is a

sleeping element in our world and false
otherwise, and if we define it the

following way, that j is mapped to true
and m is mapped to false, then we get

exactly the same representation as with
the set before. And that theory, that's

usually called a characteristic function.
So either we can treat it as a set or as a

function. In this case, it doesn't really
matter, but the next question is: "what is

love?" Or love', to be precise. And
while "sleep" is a property of an entity –

for each entity, we can decide if it's
sleeping or not. Love is not a property of

one entity, but it's the relation between
two entities. So it's either a set of

pairs. Or it is a function which takes two
parameters, and as soon as we apply to one

of the parameters, we end up with the
second function. So the function with two

parameters represent the relation between
two entities or two individuals. But if we

apply to one of the parameters, we get a
function, which is the property, for

example, to be loved by someone. Just to
keep in mind, for simple predicates, sets

and functions are equivalent, and for
these relations, it's either pairs or it's

a function. And if we apply it to one of
the arguments, we get another function.

One of the driving forces behind the
theory of Montague is compositionality.

And that's usually attributed to Frege,
even though he never really expressed it

that way. But one of the most well known
interpretations is "the meaning of a

compound expression is a function of the
meaning of its parts and the way they are

syntactically combined". So if we go back
here, we kind of have our simple and

simplest parts. We have our names and we
have our verbs, and we have rather simple

interpretations what they mean. And now
the question is how can we combine them to

form … for example, the meaning of more
complex sentences, or in general of

sentences. And for that, we need a little
bit of syntax. Syntax tells us how we can

combine these elements to form sentences.
So the rule syntax 1, for example, says if

we have a name and an intransitive verb,
we can combine them to a sentence. And the

second rule, syntax 2, says if you have a
transitive verb and a name, we can combine

it to an intransitive verb. Now we want to
look at the meaning of sentences like

"John sleeps" and the meaning of "John
sleeps" is that if we interpret the

meaning of "sleeps" and that's the
predicate which can be applied to an

entity or an individual to give a truth value.
And John is of type e, so we can apply

sleeps to John and we get, as a result,
sleep' applied to John. Or the

slightly more complex example of "John
loves Mary". We can first apply the same

semantic rule that we can apply the rest
of the sentence to the subject of the

sentence. And then we have to interpret
"loves Mary", which is this function that

takes two parameters and then is first
applied to the object and then to the

subject. So the meaning of "loves Mary" is
kind of the predicate "to be in in a state

of loving Mary". And then we apply to John
and we get the meaning: Love, Mary, John.

And now the question is: how do we
actually come up with these semantic

rules? So how do we know that we have to
apply "loves Mary" to "John". And that's

where the types give us guidance. So we
know that "loves Mary" is of the Category

IV, intransitive verb, which has the type
, and we know that John is of the

category "m", which is of semantic type e,
and if we see as a function which

takes an "e" as a parameter to produce a
"t" as a result, then we know that we can

apply "loves Mary" to John. Then I already
before mentioned the word lambda calculus

or lambda expression: Probably not
everyone knows what a lambda

expression is. It's kind of the solution
to a very … almost nit picky problem. So

if we have some formula, some expression
like "x^2 + 2 x", what does it

exactly mean? And then we could come up
with just putting numbers instead of x.

And if we put 1, we get the result 3 and
if we put 2 the result is 8 and if we put

x=3, we get 15. But what we
usually mean is: it's some kind of function

which takes a number and then maps this
number to the number's square plus two x.

That's what we mean. But it's not really
written down precisely. And that's where

logicians came up with a new operator
called lambda. Which can introduce a

variable and turn up expression, which is
not completely clear, like the one we had

before into a function. So if you write
"lambda x, x^2 + 2 x", we know

that it is a function which has a
parameter which we call x, and we use that

in our expression "x^2 + 2 x".
And then we can apply this, for example,

to 1, which means we have to replace all
"x"s in our expression by 1, and then we

get exactly the same results as we had in
our informal expression. But now it's on a

proper foundation. Why do we need that?
Because we actually have, kind of higher

order types, so we know that the E to T is
kind of a function from individuals to

truth values, that that's the same for
common noun like man, bird and so on. But

what is the type of what we call
determiners or quantifiers: some, every,

the. So the meaning of man is just
man' or man'(x), the same

as we have had with sleep before.
And the meaning of "every" now we

use this lambda. Because the meaning of
"everything" is for all things "x" that are

individuals, if they meet some predicate
P, then they also meet some predicate Q.

That's, again, very abstract, so let's
have a look at an example. So the meaning

of "every man" is: We have a new semantics
rule meeting all the types, so the type of man

is <e,t> and the semantic type of "every"
is this a slightly more complex type, but

is the function from <e,t> to something
else? So we know we can apply that terminal

to our common noun. Then we do our lamda
magic and we end up with the term lamda Q

for all x, man'(x) implies Q(x), meaning for
all things: If they are men, then they do

something or they have a certain property.
And if we now look at "every man sleeps".

We apply "every man" to "sleeps", we just had
this term on the previous slide and the

types for Q<e,t> and for sleeps match,
so we can just put that in there. And the

meaning of "every man sleeps" is for all
individuals: If they are men, then they

sleep. And that way we get a theory how we
can translate expressions of natural

language into expressions, into logic
expression, for which we can try to find

models, so we have this truth conditional
semantics, and it is compositional in the

way that the meaning of an complex
expression depends on its components. The

meaning of "every man sleeps" depends on
the meaning of "every man" and of "sleeps"

and on ways how to combine them. And these
ways how to combine them are determined by

the types we use. So we have some very
nice method of computing meaning in a

compositional way into a logic, so that
looks already pretty much like what

Montague claims, but it has certain
drawbacks. And for that reason, and also

because in logic and computers science the
research progressed, people came up with

the so-called MTTs "Modern type theories"
or the original is called "Martin-Löf type

theory". So this nice bearded guy on the
left is kind of the person who invented

everything and the nice person on the
right who likes to climb mountains, he

used to be … who is a professor in the
group where I was doing my Ph.D. used

these type theories, these modern type
theories to express the meaning of natural

language in a slightly different way. And
I'll give a quick glance at what changes

they have. But first, one of the big
advantages of this – or one of the biggest

implications of these modern type theories
is usually in computer science, in proof

systems. So one of the most or very well-
known proof assistant is the one with the

logo on the right called Coq. Another
dependently type programming language is

the language Agda, which is … both of them
are used quite extensively in formalizing,

and verifying, for example, proofs in
mathematics, and verifying and proving

properties about programs. But they can
also be used to reason about natural

language. So the different approach to
meaning in language is the so-called proof

theoretic semantics. So before we looked
at what models can be, how models can be

used to express conditions under which
things can be can be seen as true. And now

we care more about proofs than about
truth. And that goes back to logic and

computer science again. Where it's
usually referred to as the Curry-Howard

isomorphism. It's that proofs in
mathematics can be expressed as programs

in a computational framework, and that
allows us practical reasoning on

computers. And informally, if you want to
prove something, A, we can construct a

term or write a program t of this type.
And an example is at the top of the slide

where we kind of want – first it's a
function and it's the function from a

semantic representation of the sentence
"every man walks" to the sentence "John is

a man", and finally the sentence "John
walks". So we want to we have the two

sentences "every man walks" and "John is a
man". And we want to get to the conclusion

– or to figure out – if it is a conclusion
that "John walks". And this is a small

proof in the proof assistant Coq there in
a few lines of code. In a few lines of Coq

code we can find the proof that actually
from the sentence every man walks and John

is a man. We can conclude that "John
walks". The first big extension is: we

have more expressive types. So before we
had the type e for entities and the type t

for truth values. So actually the type t
doesn't change a lot. We now just called

it "prop" the type of propositions. But
for common nouns like man, which were

properties <e,t> properties of
individuals we just introduced new types

like "man", "book" and so on. And for
verbs, for example, we define them as

functions from one of these types to
properties. So not just from any

individual, but from meaningful domains.
So, for example, the meaning of talk

requires that whoever is talking is
actually human, because except for a few

situations where other things could talk,
it's usually only a human who talks. And

the meaning of mortal is that something
has to first be alive to be mortal. That's

already nice, so we can limit our domains
of predicates to very meaningful things

where people intuitively would say that
makes sense, but then we end up in the

problem. For example, if we have the
meaning of "Socrates is of type man" and

wave "mortal", but mortal is of this type:
it takes a parameter that's animate and

return a property. And now we want to
interpret "Socrates is mortal" in pretty

much the same way as we did it before, or
in a similar way as we interpreted things

before. So we want to apply this meaning
of "mortal" to Socrates, but we have the

problem, that man doesn't match the type
animate. So how does that work? And the

answer to that, to that is we can assume
subtypes, or we can introduce subtypes. So

if we assume that humans are animate and
men are human. Then we can actually apply

the function that takes an animate object
as a parameter to something that's a man,

and also we want to assume that modified
objects like a heavy book should still be

a subtype of book. And fortunately, we can
do that in the theory. And the final thing

is: some functions, so we can already rule
out some some things, with the … here, if

we say that "talk" only works for humans, we
can already rule out some nonsensical

things, but we can use a little bit of
this proof theoretic a bit more. So if we

have this. I hope it's not too
distracting that it's a bit of a weird

syntax. We define a new type which is
consumable, and we define two objects that

are consumable. It's bread and wine. And
then we define a new type of action with

the two actions. One is eat, one is drink.
And then we define a new type performance,

which depends on both a consumable object
and an action. And then we can construct

objects of this performance, by using this
construct to perform. So the meaning of

"drink wine", for example, could be:
perform, wine, drink. But we can also in

this setting define the meaning of "eat
wine" as: perform, wine, eat. And that's

usually something we want to rule out. We
want to have only to be able to drink wine

or to eat bread, but not to eat wine or
drink bread. And that we can do by

defining a new type of, for example,
edible and drinkable objects, and we

define eat bread as edible bread and drink
wine as drinkable wine, and then we modify

our action and performance, that the
action of eating needs an object of this

type edible for the thing we want to
consume. And this object is kind of the

proof that whatever consumable we want to
eat is actually edible. And then we can

still define drink wine. In a pretty
similar way, but we cannot find any way of

performing eat on wine because there is no
way of constructing an edible object for

wine. Which is a very powerful thing of
modeling how our real world happens to

work, and … that pretty much concludes my
talk. Here are a few references.

And now I'm open for questions.
Herald: Right, so, so far we have one

question I see. And the question is: so
how far can we take this? Has anyone ever

formulated a sufficiently detailed type
system for English or at least some

variant of English, which can be used to
reason about human-written or even

informal texts like algorithmic
language processing?

daherb: That's a very good question.
And that's one of the weak spots of this,

that it involves lots of work. And these
days a lot of research and effort is more

on statistical models where you hopefully,
very hope, that the computer might learn

these things. There are a few there,
there's for example a dataset. So some

logicians sat down at some point and made
many sentences in this style, like "every

European has the right to live in Europe"
and so on. I think it's a few hundred

sentences and that's kind of the benchmark
where people try to test the systems . And

that kind of works. I know there are
systems that can cover the whole benchmark

and give the right results, but there are
other datasets that are not created by

logicians, but by everyday people
crowdsourced on the Internet, and there

it's much more difficult to actually agree
on what is the conclusion?

Herald: Okay, so the main problem is that
there aren't any curated big enough data

sets to to check the algorithms against,
or?

daherb: That's part of the problem. But
it's also, yeah, it's really difficult to

make that work for the complete language,
for really big parts. But if you have a

small application, a small domain, then
it's definitely a feasible thing to do.

And it gives you also an explanation of
why one sentence follows from another,

either by giving you the model in which
these sentences are true or in the modern

type theory by giving you a proof. So
there is lots of research in doing that

without logic and just machine learning,
and they seem to be pretty good. But then

sometimes these systems just give you the
wrong result and you have no idea why. And

yeah, that's the balance. So you get the
highly reliable results from this system,

but you have to do a lot of work to get it
working, or you use a machine learning

system which works much broader, but if
something goes wrong, it's much more

difficult to figure out what is exactly
going wrong.

Herald: Okay, thank you very much. We have
a question from Gordon in the IRC –

live.hacc.media for anyone who isn't there
yet. How you not managed to mention

Lojban? I'm not really sure on how to
pronounce that.

daherb: So, um. I don't know too much
about Lojban except that it's an

artificial language that I think was
designed to have a clear semantics,

probably something like first order logic
so that approach is different and, these

people, at least, who work on this, which
I presented at least could pretend that

they work with proper English. Even though
some people could also turn it around and

say they defined a nice formal language,
which just looks very much like English,

but it's actually it's a formal language.
Herald: Okay, and we have Bob asking

whether there is any effort to create a
combination of a statistical and logical

approach, and if not, why hasn't it been
done or what are the challenges?

daherb: There are definitely approaches
that try to do that. The question

is, where do you put the machine learning
and where do you put the logic and what

parts you can replace by machine learning,
for example? But there is definitely

approaches. I think one is called
CCG Lamda by people in Japan.

So there are definitely these approaches.
Herald: And we have Klondyke asking

whether there is any work on trying to
infer types and rules from the corpuses.

daherb: I'm not really aware of
anything like that.

Herald: Did you try generating valid
sentences by random.

daherb: depends on what you define as
valid sentences. One answer to this

question would be I once wrote a Twitter
bot which generates random sentences which

are all total tautologies. So I used many
of these techniques I presented to

generate natural language sentences,
which all have a certain logic structure.

And if you have a system like that,
generating is usually not a big issue,

analysis is usually the bigger issue.
Herald: Okay, we have one more question

where I can get the context to about the
xkcd cartoon – maybe go back to the slide,

and they want to know whether you can say
something about why there are many

competing syntax trees for the same
language or more like what the tree is

exactly for, what are the differences
daherb: In this, the main difference is

how much effort you want to put into the
analysis. So the syntax tree at

the top left is basically textbook
level. It gives a very simple analysis and

from a linguistic point of view, people
could argue what exactly is, for example,

this category for copula. And the other
two sentences are kind of – I don't want

to really say competing syntactic
theories, so there are lots of theories,

where they try to explain how natural languages
work. I said people are really good at

drawing trees, but they still struggle to
explain certain things. And over the last

almost hundred years, people came up with
lots and lots of theories, how syntax

actually works. And these theories usually
have nice advantages and on the other

hand, drawbacks. So the syntax tree on the
top right is called combinatory categorial

grammars and it uses categories which are
also kind of function types. So NP/N and

can be seen as a function which takes a N
as a parameter on the right and generates an

NP. So the syntactic categories are kind
of in parallel to the semantic categories.

And that way it's easy to translate from
the syntax tree into the semantic

representation while for other syntax
formalisms it might be more challenging to

to do that. So it strongly depends what
you want to do, how to express that

concept. Yeah, it goes a bit in the
direction of this xkcd. I can subscribe to

any dozen of contradictory models and
still be taken seriously.

Herald: Okay, are there any issues on
these trees with garden path sentences?

daherb: I should know more about
garden path entrances because it's one of

the main examples where things go wrong.
At the moment. I cannot really answer

that. I try to give a simple high
level overview of it. And there are many

interesting problems: garden path
sentences, donkey sentences, where syntax

or semantics or both can go wrong.
Herald: Okay, so far, I don't see any more

questions, so I would like to know from
you, how does one get into type

theory or language analytics or semantics
daherb: Hanging out with the wrong people

or, yeah. So computational linguistics is
a pretty established field these days, so

it's what people call interdisciplinary,
it's taking a lot of computer science and

hopefully still a bit of linguistics, and
then you try to tackle certain problems.

And one of the big problems of natural
language is what do they mean? And when

you study that, for example, then you get
some you learn something about it, and if

you're curious about it, you can put
research into it. And to be honest, my

research was something completely
different. But the topic of semantics was

kind of one of the reasons why I wanted to
do some more research and stay in

academia.
Herald: Okay, thank you. Back again to AI

language processing. Do you think there is
a kind of new, bigger field coming? Well,

there was the last few years with natural
language processing getting more and more

accessible to the public and better. And
do you think that there is still a chance

for only analytical approaches, or do you
think that AI will be in the end, more

prevalent?
daherb: So actually, if you look at the

research output in recent years, then you
only find a little bit about what I was

talking about and you find a lot about
… what I have listed here as statistical

approaches, especially language models. I
guess most people who haven't been away

from the Internet in the last few months
have at least heard a little bit about,

for example, GPT-3, which is one of these
fancy AI models which you can use for

generating text based on some
sentence to start the text. Or people even

implemented a dungeon crawl text adventure
using it. So that's the hot shit in in

research, kind of. But these suffer from
this problem that as soon as something

goes wrong, it's really difficult to
figure out what's going wrong. And you

need shitloads of data.
Herald: Okay, we have some more questions.

Just came in. We have some book
recommendations in the IRC if anyone is

interested. And we have one person asking
whether a function word like conjunctions

or some grammar like that-clauses can be
present in type systems.

daherb: So I haven't done anything
about conjunction and so on. In the simply

typed language, they are just translated
to their logic operators. So you only have

usually conjunctions on the sentence level
so you could make sentences. "John loves

Mary" and "Mary sleeps". And because the
type of sentence is t, which is truth

value, which is kind of a boolean
variable, you can use boolean operations

on it. So you analyze the first sentence
and then you analyze the second sentence

and then you check if the logic
conjunction holds between them. And if you

translate that in into models, conjunction
can also be translated into the set operation

of intersection. So conjunctions
and disjunctions like the

function words "and" and "or" are pretty
easy, or still rather easy to express.

There is, …, still many, many challenges
which into which I couldn't go in the

time.
Herald: Okay. I think that answers the

question from before. And there is also a
new one: This "for all" thing. I always

thought that required dependent types. Did
I miss something or is that actually

wrong?
daherb: If it is a simply typed

language, then it doesn't require
dependent types. There is is an equivalent

to the "for all" in dependent types – in
dependently typed languages. I think that

should be the Pi types which are
dependent function types, but in a simply

typed language you just have the forall
operator.

Herald: Okay. Are there new questions? I
think there are. Can you recommend an intro

to linguistics or a book? I think we just
had some, but maybe, you know, some off

the top of your mind.
daherb: So except for the ones I have in

my literature list, there are a few books
by a professor called Emily Bender, which

she coauthored with other people. One is
about syntax, one is about semantics. And

I haven't read them myself, but I think
they are pretty good from what I heard.

Because they also bridge between the
linguistic knowledge and the requirements

you have these days with more
computational.

Herald: Okay. I think, I'm not sure
whether the "no" is directed towards me or

you, but apparently some of these were
only programing language books, so

probably the ones in the IRC. There is
also a question relayed from Twitter

whether semantic web still is a thing in
your community.

daherb: It's a community on its own. And I
don't know too much about it. It it's

definitely still a thing. There are still
people working on it, but I cannot say too

much about it. I think that was probably
going in this direction, new attempts for

multilingual Wikipedia, where you use
semantic representation for the Wikipedia

page and then use that to generate the
articles in various languages.

Herald: Okay, I think the end –
daherb: And of course,

Herald: The IRC, you're already satisfied
–

daherb: Maybe another answer to the
semantics web and in addition, an answer

to a question that was before about
actually inferring these types somehow is

so what you can do with
these types, especially with expressive

types, is you kind of create something
that's called an ontology, which is in a way

a representation of the world. So what I
try to do here is I define what is edible,

what is drinkable, and it's tedious to
hard code all these things about the

world. And a lot of this is represented in
either datasets or, for example, in the

semantic web. So people already put effort
into encoding that somehow and then you

just need to extract it and use it.
Herald: Okay, we are already at the end

of time, there is three minutes left. We
have one more question. I think after that

we'll close it: And are you aware of
natural language, hand-wavy formal text

like codes of law which have been type
checked?

daherb: I know that there are people
who spend their whole Ph.D. on trying to

formalize law texts.
I think there was also

some work on formalizing the GDPR, but
I heard about a few of these things, but

I'm not fully aware of what's available
and where it is available.

Herald: Okay, so if you don't have anything
more to say, say so. And apart from that,

I think we are done here,
at least for my part.

daherb: Yep, then thanks for listening!

postroll music

Subtitles created by c3subtitles.de
in the year 2021. Join, and help us!