ASP_def.txt - def of simplified ASP in axiomatic language
- based on "Basics behind Answer Sets", Yuliya Lierler, U Neb Omaha, Aug 2020
https://works.bepress.com/yuliya_lierler/71/


----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
from [Lierler]:

ASP - Answer Set Programming - a form of declarative programming for
   i intelligent agents in knowledge representation and reasoning
  ii difficult combinatorial search problems
  - a contraint programming language
this simple presentation: no variables, no classical negation symbol,
   no disjunction in the heads of rules

*traditional rule*
   a0 <- a1, ..., am, not am+1, ..., not an.   0 <= m <= n
      ai - propositional atoms (symbols),
           a0 can also be _|_ (bottom) (or missing)
      - a0 is *head*, "a1 ... an" is *body*
      - traditional rule is *constraint* if head is _|_ (which is dropped)

*traditional (or propositional logic) program* - set of traditional rules
traditional rule is *positive* if n = m (no "neg" conditions)
Def 1: Set X of atoms satisfies a positive traditional rule when a0 is in X
   if a1..am are in X.
Def 2: Set of atoms X satisfies a positive traditional program P if X satisfies
   every rule in P.
Def 3: Smallest set of atoms that satisfies positive traditional program P
   is *answer set* of P.
	
*** My simplification for this axiomatic language definition:
   No _|_ for head of rules; i.e., no constraints!


----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
===== Axioms for positive traditional programs and their answer sets! =====

!/
Representation of positive program and its answer set:

  (pos_ans_set <pos prog> <ans set>)  - predicate for pos prog and its ans set
    <pos prog> - ( {<pos rule>} )    -- >=0 rules (>0 rules?)
    <pos rule> - (<a0> < {<a1..m>})  -- head atom and zero or more body atoms
       -- note that token '<' is present even if m = 0 (a "fact")
       -- (note that in this grammar my atom nonterminals have subscripts)
       -- I exclude the case where a0 could be "bottom" _|_ (or is missing)
    <a_> - <letter> {<letter> | <digit>}   -- atom symbol
    <ans set> - ( {<a>} )    -- sequence (i.e. set) of (distinct) atoms
!\

! pos_ans_set_partial - incrementally consume pos prog while generating ans set
! (pos_ans_set_partial <orig pos prog> <remaining pos prog> <partial ans set>)

  (pos_ans_set_partial %orig_posprog %orig_posprog> ()).  ! before prog consump
    ! - initial state before start of answer set generation
  (pos_ans_set_partial %orig_posprog %rules' %anset')<   ! a rule "fires"
    (pos_ans_set_partial %orig_posprog %rules %anset),
    (first_rule_that_fires %anset %rules %head %rules'),
      ! - get first rule that "fires" - get its head and remove rule
    (add_elem %anset %head %anset').    ! append head to ans set if not there
  ! - we recurse until no more rules can fire
  
! pos_ans_set - get answer set for a positive program

  (pos_ans_set %pos_prog %anset) <             ! no rule can fire - done!
    (ASP_pos_prog %pos_prog),         ! positive program is syntactically valid
    (pos_ans_set_partial %pos_prog %rules %anset),
    (no_rule_fires %anset %rules).
  ! - when no more rules can "fire", we have our answer set!

! first_rule_that_fires - process the first rule from a seq that can "fire"

  (first_rule_that_fires %anset ((%head < $body) $rules) %head ($rules))<
    (subset ($body) %anset).    ! body atoms are subset of ans set atoms
  (first_rule_that_fires %anset ((%h < $b) $rules) %head %rules')<
    (/subset ($b) %anset),      ! initial rule can't fire
    (first_rule_that_fires %anset ($rules) %head %rules').

! no_rule_fires - no rule can fire for current answer set

  (no_rule_fires %anset ()).
  (no_rule_fires %anset ((%h < $b) $rules))<  
    (/subset ($b) %anset),
    (no_rule_fires %anset ($rules)).

! ASP_pos_prog - definition of a valid ASP positive traditional program

  (def ASP_pos_prog (* ASP_pos_rule)).  ! pos prog is seq of >=0 pos rules
    ! - note that we allow a positive program to have zero rules! (?)

! ASP_pos_rule - definition of a valid ASP positive rule
! - note that token symbol < is always present, even if no body conditions

  (ASP_pos_rule (%head < $body))<
    ((* ASP_prop_sym) (%head $body)).
    
! ASP_prop_sym - ASP propositional symbol - letter {letter | digit))

  (ASP_prop_sym (%sym_atom (%ltr)))<      ! 1st atom char is letter
    (symbol_atom %sym_atom),
    (letter %ltr).
  (ASP_prop_sym (%sym_atom ($cstr %ld)))<   ! append letter or digit to
    (ASP_prop_sym (%sym_atom ($cstr))),     !   symbol char string
    (one_valid (letter %ld) (digit %ld)).


----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
from [Lierler]:

--- Answer sets of a (traditional) program with negation ---

Def: *reduct* IIX of a traditional program II relative to a set X of atoms
- set of rules from II where no am+1..an is in X.
(We drop the II rules where some am+1..an is in X and then drop the (now
satisfied) neg conditions from the kept rules to yield the IIX positive
traditional program.)

We compute a reduct IIX positive program for each subset of all the head
atoms of the traditional program.  We then compute the answer set of this
positive program.  If the reduct IIX answer set equals the set X, then
that set is an answer set of the traditional program.


----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
===== Axioms for traditional programs and their answer sets! =====

!/
Representation of a traditional program and its answer sets:

  (trad_ans_set <trad prog> <ans sets>)  - pred for trad prog and its ans sets
    <trad prog> - ( {<trad rule>} )
    <trad rule> - (<a0> < {<a1..m>} ~ {<am+1..n>})
       -- head atom and >=0 pos body atoms and >=0 neg body atoms
       -- note that tokens < ~ are present even if m = 0 and/or n = m
       -- for now we exclude the case where a0 could be "bottom" _|_
    <ans sets> - ( {<ans set>} )  -- sequence (i.e. set) of all answer sets
    <ans set> - ( {<a>} )   -- seq of (distinct) atoms of an answer set
!\
 
! reduct - get positive reduct of traditional prog for a set X of atoms

  (reduct %setX %tradprog %posprogX)<
    (map/nil (reduct_rule %setX) %tradprog %posprogX).

! reduct_rule - apply reduct step to a traditional rule

  ((reduct_rule %setX) ($hp ~ $n) ($hp))<   ! pos portion of rule is kept
    (none_in ($n) %setX).      ! none of the neg atoms are members of set X
  ((reduct_rule %seqX) ($hp ~ $n) `nil)<    ! neg atom in X - rule is discarded
    (some_in ($n) %seqX).      ! at least one neg atom is member of set X

! trad_ans_sets - answer sets of a traditional prog

  (trad_ans_set %tradprog %ansets)<
    (ASP_trad_prog %tradprog),     ! valid ASP traditional program
    (heads %tradprog %heads),      ! get head atoms of all trad prog rules
    (powerset %heads %Xsets),      ! "X sets" are all head atom subsets
    (map/nil (reduct_ans_set %tradprog) %Xsets %ansets),  ! get all ans sets

! reduct_ans_set - answer set for setX reduct of a trad prog, else `nil

  ((reduct_ans_set %tradprog) %setX %anset/nil)<
    (reduct %setX %tradprog %posprogX),  ! get reduct pos prog for this setX
    (pos_ans_set %posprogX %anset),      ! get ans set for reduct pos prog
    (=set? %anset %setX %t/f),           ! are reduct anset and setX equal?
    (t/f_sel (%anset `nil) %t/f %anset/nil).  ! if so, trad ans set found!

! ASP_trad_prog - definition of a valid ASP traditional program

  (def ASP_trad_prog (* ASP_trad_rule)).  ! trad prog is seq of >=0 trad rules
    ! - note that traditional program can have zero rules

! ASP_trad_rule - definition of a valid ASP traditional rule
! - note that token symbols < ~ are always present, even when
!   positive or negative proposition symbol conditions are not present

  (ASP_trad_rule (%head < $pcond ~ $ncond))<
    ((* ASP_prop_sym) (%head $pcond $ncond)).


----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
===== Used utility functions =====
  add_elem, subset, /subset, none_in, some_in - bit.ax
  map/nil, =set?, t/f_sel - bool.ax
  powerset - form.ax
  one_valid, *, def, heads - ho.ax
  letter, digit, symbol_atom - char.ax