1 of 52

Knowledge Graph Conference

May 2024

Joshua Shinavier, PhD

jshinavier@microsoft.com

Graphs, Logic, and Lambda Calculus

bit.ly/lg-discord

bit.ly/hydra-source

2 of 52

Graphs

3 of 52

4 of 52

5 of 52

6 of 52

7 of 52

8 of 52

9 of 52

10 of 52

11 of 52

12 of 52

13 of 52

Curry-Howard Correspondence

14 of 52

Curry-Howard Correspondence

	Logic	Lambda Calculus

15 of 52

	Logic	Lambda Calculus

16 of 52

	Logic	Lambda Calculus
	proposition	type

17 of 52

	Logic	Lambda Calculus
	proposition	type
	proof	term

18 of 52

	Logic	Lambda Calculus
	proposition	type
	proof	term
	conjunction	product type
	disjunction	sum type
	basic predicate	primitive type
	universal quantification	forall type
	implication	function type

19 of 52

	Logic	Lambda Calculus
	proposition	type
	proof	term
	conjunction	product type
	disjunction	sum type
	basic predicate	primitive type
	universal quantification	forall type
	implication	function type
	proposition(constant)	constant term
	conjunction of proofs	tuple / record
	disjunction of proofs	injection / variant
	projection function	projection
	disjunction of equalities	case statement
	predicate definition	lambda term
	predicate	primitive function
	variable substitution	let term

20 of 52

Graphs	Logic	Lambda Calculus
	proposition	type
	proof	term
	conjunction	product type
	disjunction	sum type
	basic predicate	primitive type
	universal quantification	forall type
	implication	function type
	proposition(constant)	constant term
	conjunction of proofs	tuple / record
	disjunction of proofs	injection / variant
	projection function	projection
	disjunction of equalities	case statement
	predicate definition	lambda term
	predicate	primitive function
	variable substitution	let term

21 of 52

Graphs	Logic	Lambda Calculus
?	proposition	type
?	proof	term
?	conjunction	product type
?	disjunction	sum type
?	basic predicate	primitive type
?	universal quantification	forall type
?	implication	function type
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

22 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
?	proof	term
?	conjunction	product type
?	disjunction	sum type
?	basic predicate	primitive type
?	universal quantification	forall type
?	implication	function type
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

23 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
?	conjunction	product type
?	disjunction	sum type
?	basic predicate	primitive type
?	universal quantification	forall type
?	implication	function type
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

24 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
?	disjunction	sum type
?	basic predicate	primitive type
?	universal quantification	forall type
?	implication	function type
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

25 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
?	basic predicate	primitive type
?	universal quantification	forall type
?	implication	function type
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

26 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
?	universal quantification	forall type
?	implication	function type
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

27 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
?	implication	function type
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

28 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
?	proposition(constant)	constant term
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

29 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
?	conjunction of proofs	tuple / record
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

30 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
element and properties	conjunction of proofs	tuple / record	g.addV('Person').property('...
?	disjunction of proofs	injection / variant
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

31 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
element and properties	conjunction of proofs	tuple / record	g.addV('Person').property('...
variant element	disjunction of proofs	injection / variant	g.addV('Pizza')
?	projection function	projection
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

32 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
element and properties	conjunction of proofs	tuple / record	g.addV('Person').property('...
variant element	disjunction of proofs	injection / variant	g.addV('Pizza')
tail / head / lookup	projection function	projection	e.outV().get('name')
?	disjunction of equalities	case statement
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

33 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
element and properties	conjunction of proofs	tuple / record	g.addV('Person').property('...
variant element	disjunction of proofs	injection / variant	g.addV('Pizza')
tail / head / lookup	projection function	projection	e.outV().get('name')
pattern match	disjunction of equalities	case statement	e.choose(...).option(...
?	predicate definition	lambda term
?	predicate	primitive function
?	variable substitution	let term

34 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
element and properties	conjunction of proofs	tuple / record	g.addV('Person').property('...
variant element	disjunction of proofs	injection / variant	g.addV('Pizza')
tail / head / lookup	projection function	projection	e.outV().get('name')
pattern match	disjunction of equalities	case statement	e.choose(...).option(...
"active" element or value	predicate definition	lambda term	g.V().filter{it.get()...
?	predicate	primitive function
?	variable substitution	let term

35 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
element and properties	conjunction of proofs	tuple / record	g.addV('Person').property('...
variant element	disjunction of proofs	injection / variant	g.addV('Pizza')
tail / head / lookup	projection function	projection	e.outV().get('name')
pattern match	disjunction of equalities	case statement	e.choose(...).option(...
"active" element or value	predicate definition	lambda term	g.V().filter{it.get()...
primitive function	predicate	primitive function	lTrim()
?	variable substitution	let term

36 of 52

Graphs	Logic	Lambda Calculus
type / label	proposition	type	Person
typed value / labeled element	proof	term	g.addV('Person')
record type / element type	conjunction	product type	{out:Person, in:Organization}
union of types	disjunction	sum type	Piano \| Pizza
property type	basic predicate	primitive type	string
polymorphic element type	universal quantification	forall type	DeliveryService<Truck, Piano>
"active" element or value type	implication	function type	Function<Piano, Company>
property value	proposition(constant)	constant term	"Arthur Dent"
element and properties	conjunction of proofs	tuple / record	g.addV('Person').property('...
variant element	disjunction of proofs	injection / variant	g.addV('Pizza')
tail / head / lookup	projection function	projection	e.outV().get('name')
pattern match	disjunction of equalities	case statement	e.choose(...).option(...
"active" element or value	predicate definition	lambda term	g.V().filter{it.get()...
primitive function	predicate	primitive function	lTrim()
graph	variable substitution	let term	e.as('a')

37 of 52

38 of 52

Types

[...]

39 of 52

Terms

[...]

40 of 52

Typing rules

41 of 52

Typing rules

42 of 52

Graphs as terms

43 of 52

let x = 10

y = 32

z = x + y in z

44 of 52

let x = 10

y = 32

z = x + y in z

45 of 52

46 of 52

let p1 = Person {name = "Joshua", twitter = "joshsh"}

p2 = Person {name = "Deborah", twitter = "dlmcguinness"}

p3 = Person {name = "Alastair"}

p4 = Person {name = "Molham", twitter = "molhamaref"}

p5 = Person {name = "Ora", twitter = "oralassila"}

f12 = follows {_out = p1, _in = p2}

f14 = follows {_out = p1, _in = p4}

f15 = follows {_out = p1, _in = p5}

f21 = follows {_out = p2, _in = p1}

f25 = follows {_out = p2, _in = p5}

f45 = follows {_out = p4, _in = p5}

f51 = follows {_out = p5, _in = p1}

f52 = follows {_out = p5, _in = p2}

in {}

47 of 52

let p1 = Person {name = "Joshua", twitter = "joshsh"}

p2 = Person {name = "Deborah", twitter = "dlmcguinness"}

p3 = Person {name = "Alastair"}

p4 = Person {name = "Molham", twitter = "molhamaref"}

p5 = Person {name = "Ora", twitter = "oralassila"}

s1 = Session {name = "Graph Standards Rebooted"}

f12 = follows {_out = p1, _in = p2}

f14 = follows {_out = p1, _in = p4}

f15 = follows {_out = p1, _in = p5}

f21 = follows {_out = p2, _in = p1}

f25 = follows {_out = p2, _in = p5}

f45 = follows {_out = p4, _in = p5}

f51 = follows {_out = p5, _in = p1}

f52 = follows {_out = p5, _in = p2}

m11 = moderator {_out = s1, _in = p1}

p12 = panelist {_out = s1, _in = p2}

p13 = panelist {_out = s1, _in = p3}

p14 = panelist {_out = s1, _in = p4}

p15 = panelist {_out = s1, _in = p5}

in {}

48 of 52

let p1 = Person {name = "Joshua", twitter = "joshsh"}

p2 = Person {name = "Deborah", twitter = "dlmcguinness"}

p3 = Person {name = "Alastair"}

p4 = Person {name = "Molham", twitter = "molhamaref"}

p5 = Person {name = "Ora", twitter = "oralassila"}

s1 = Session {name = "Graph Standards Rebooted"}

f12 = follows {_out = p1, _in = p2}

f14 = follows {_out = p1, _in = p4}

f15 = follows {_out = p1, _in = p5}

f21 = follows {_out = p2, _in = p1}

f25 = follows {_out = p2, _in = p5}

f45 = follows {_out = p4, _in = p5}

f51 = follows {_out = p5, _in = p1}

f52 = follows {_out = p5, _in = p2}

m11 = moderator {_out = s1, _in = p1}

p12 = panelist {_out = s1, _in = p2}

p13 = panelist {_out = s1, _in = p3}

p14 = panelist {_out = s1, _in = p4}

p15 = panelist {_out = s1, _in = p5}

in SessionInfo {created = "2024-05-01T17:32:41Z",

lastUpdated = "2024-05-06T08:51:03Z"}

49 of 52

let p1 = Person {name = "Joshua",

twitter = "joshsh",

follows = [p2, p4, p5]}

p2 = Person {name = "Deborah",

twitter = "dlmcguinness",

follows = [p1, p5]}

p3 = Person {name = "Alastair",

follows = []}

p4 = Person {name = "Molham",

twitter = "molhamaref",

follows = [p5]}

p5 = Person {name = "Ora",

twitter = "oralassila",

follows = [p1, p2]}

in let s1 = Session {name = "Graph Standards Rebooted",

moderator = p1,

panelists = [p2, p3, p4, p5]}

in SessionInfo {session = s1,

created = "2024-05-01T17:32:41Z",

lastUpdated = "2024-05-06T08:51:03Z"}

50 of 52

let p1 = Person {name = "Joshua",

twitter = "joshsh",

follows = [p2, p4, p5]}

p2 = Person {name = "Deborah",

twitter = "dlmcguinness",

follows = [p1, p5]}

p3 = Person {name = "Alastair",

follows = []}

p4 = Person {name = "Molham",

twitter = "molhamaref",

follows = [p5]}

p5 = Person {name = "Ora",

twitter = "oralassila",

follows = [p1, p2]}

in let s1 = Session {name = "Graph Standards Rebooted",

moderator = p1,

panelists = [p2, p3, p4, p5]}

in let sessionSize = λs . 1 + (length s.panelists)

in SessionInfo {session = s1, size = sessionSize s1,

created = "2024-05-01T17:32:41Z",

lastUpdated = "2024-05-06T08:51:03Z"}

51 of 52

Schema graph (LPG)

Schema graph (hypergraph)

52 of 52

Graphs, Logic, and Lambda Calculus

jshinavier@microsoft.com

bit.ly/lg-discord

bit.ly/hydra-source