Sequence Length Function

A Sequence Length Function is a length function that is restricted to sequences (a count function that maps a sequence to a non-negative number of the count of the symbols in the sequence)

• Context:
  • Input: a Sequence.
  • Output: a Non-Negative Integer (that represents the number of Members in the Sequence).
• Example(s):
  • a String Length Function.
• See: Set Cardinality Function, Infinite Sequence.

---

---

References

• http://www.isi.edu/~hobbs/bgt-sequences.text
  • We define "length" as follows:
    • (12)

  (forall (n s)   
     (if (sequence s) 
         (iff (length n s)
              (exists (s1 s2)
                 (and (function0 s s1 s2)(ints s1 1 n))))))

---