namespace latin:/❚

fixmeta ur:?LF❚

/T A formalization of Discourse Representation Theory (Hans Kamp \cite{Kamp:atotas81}; 
  see also \cite{KamRey:acffodrs96}).
  This formalization is patterned after https://kwarc.info/people/mkohlhase/papers/dlc00.pdf
  only that we restrict ourselves to the first-order case. 
  We give DRSes and Conditions a mode (in the type), where modes record the binding 
  and bindable (i.e. free) discourse referents. 
  In particular, the modes allow us to predict binding potentials; just see the positive 
  referents in the mode. 
  The modes have special computation rules here, so that they are normalized correctly.
❚
  

theory DRT =
  dr: type❙ //Discourse Referents ❙
  mode : type❙  //DLC modes, they annotate the dynamic status of DRs ❙
  pos: dr ⟶ mode❘# 1 ⁺ prec 60❙
  neg: dr ⟶ mode❘# 1 ⁻ prec 60❙
  empty : mode❘# ∅❙
  punion : mode ⟶ mode ⟶ mode❘# 1 ⊎ 2 prec 50❙

  mequal : mode ⟶ mode ⟶ type❘# 1 ≐ 2 prec 30❘role Eq❙
  refl : {x} x ≐ x❙
  // bounded semi-lattice❙
  
  capture: {x} x⁺⊎x⁻ ≐ pos x❙ //specifying DR capture ❙
  
  rule ☞scala://modes.drt.latin2?NormalizePunion❙
  
  close : mode ⟶ mode❘# 1 ↓ prec 60❙
  close_pos: {x} x⁺↓ ≐ ∅❘ role Simplify❙
  close_neg: {x} x⁻↓ ≐ x⁻❘ role Simplify❙
  close_empty: ∅↓ ≐ ∅❘ role Simplify❙ 
  close_close: {x}x↓↓ ≐ x↓❘ role Simplify❙
  
  // normal form of modes: set of DR with function into boolean❙
  
  drs : mode ⟶ type❘# 1 # o prec -5❙ // type of DRSes ❙
  tm : mode ⟶ type❘# tm 1 prec -5❙ // type of terms ❙
  cond : mode ⟶ type❘# cond 1 prec -5❙ // type of conditions ❙
  
  /T DRSs❙
  atomic : {m,n} cond n ⟶ drs (m⊎n)❘# 1 | 3 prec 10❙  // m is just set of drs, all mapped with pos in the return type❙
  merge : {m,n} drs m ⟶ drs n ⟶ drs(m⊎n) ❘# 1 ⊗ 2 ❙
  seqmerge : {m,n} drs m ⟶ drs n ⟶ drs (m ⊎ n↓) ❘# 1 ;; 2 ❙

  
  /T conditions❙
  and : {m,n} cond m ⟶ cond n ⟶ cond m⊎n❘# 3 ∧ 4 prec 20❙
  dneg : {m} drs m ⟶ cond m↓❘# ¬* 2 prec 60❙
  dimpl : {m,n} drs m ⟶ drs n ⟶ cond (m⊎n↓)↓ ❘# 3 ⇒* 4 prec 20❙ 

  /T terms❙
  idref : {i:dr} tm i⁻❘# ` 1 prec 60❙
❚

theory Example : ?DRT =
  /T example for a predicate❙
  farmer : {m} tm m ⟶ cond m❘# %%prefix 1 1 prec 100❙
  donkey  : {m} tm m ⟶ cond m❘# %%prefix 1 1 prec 100❙
  stick  : {m} tm m ⟶ cond m❘# %%prefix 1 1 prec 100❙
  beat: {l,m,n} tm l ⟶ tm m ⟶ tm n ⟶ cond l⊎m⊎n❘# %%prefix 3 3 prec 100❙
  own: {m,n} tm m ⟶ tm n ⟶ cond m⊎n❘# %%prefix 2 2 prec 100❙
  u: dr❙
  v: dr❙
  w: dr❙
  uv : mode❘ = u⁺ ⊎ v⁺❙
  /T A farmer owns a donkey ❙
  fod = uv | farmer`u ∧ donkey`v ∧ own(`u)`v❙
  /T He beats it with a stick ❙
  fbds = w⁺ | stick`w ∧ beat(`u)(`v)`w❙
  /T the iconic DRT example: If a farmer owns a donkey, he beats it with a stick ❙
  donkey_sentence: drs ∅❘ = ∅ | fod ⇒* fbds❙
❚