Help with definitions for abstract object theory

Stream: lean4

[Avi Craimer]

I'm starting an implementation of Edward Zalta's abstract object theory.

The issue in the definition below is an error:

(kernel) arg #3 of 'Formula.applied' contains a non valid occurrence of the datatypes being declared

I guess I can't use Term as an argument to relsToTerms inside of the type definition. I don't know how to express that the terms applied to the term of an nary-relation $R: [r_1, ... r_n]$ must be of type $[Term \; r_1, \; ... \;, \; Term \; r_n]$.

inductive Rel : Type  where
  | Ind : Rel
  | NAry : (List Rel) -> Rel
deriving Repr
open Rel

def relsToTerms (T: (Rel -> Type)) (rels: List Rel ) : Type :=
   match rels with
   | [] => PUnit
   | (r :: rs) => (T r) × (relsToTerms T rs)

mutual
  inductive Formula : Type where
    | atom : Term (Rel.NAry []) -> Formula
    | applied :
    Term (Rel.NAry (rels: List Rel)) ->
    (relsToTerms Term rels) ->
    Formula
    | ifThen : Formula -> Formula -> Formula
    | not : Formula -> Formula

  inductive Term : Rel -> Type where
    | Name : (R:Rel) -> String -> Term R
    | Variable: (R:Rel) -> String -> Term R
    | formulaTerm : Formula -> Term (Rel.NAry [])
end

[David Wärn]

You can write it like this, assuming you intend rels to be an argument to applied (not sure what happens when you write it like you did). I just replaced yourrelsToTerms with another mutual inductive definition

inductive Rel : Type  where
  | Ind : Rel
  | NAry : (List Rel) -> Rel
deriving Repr
open Rel

mutual
  inductive Formula : Type where
    | atom : Term (Rel.NAry []) -> Formula
    | applied :
    (rels : List Rel) ->
    Term (Rel.NAry rels) ->
    (TermList rels) ->
    Formula
    | ifThen : Formula -> Formula -> Formula
    | not : Formula -> Formula

  inductive Term : Rel -> Type where
    | Name : (R:Rel) -> String -> Term R
    | Variable: (R:Rel) -> String -> Term R
    | formulaTerm : Formula -> Term (Rel.NAry [])

  inductive TermList : List Rel -> Type where
    | nil : TermList []
    | cons (r : Rel) (rs : List Rel) : Term r -> TermList rs -> TermList (r :: rs)
end

I don't know what kind of mutual inductive definitions are allowed by Lean, but basically what you wrote only makes sense because relsToTerms is in some sense positive in its T argument (more terms of T r means more terms of relstoTerms T rs)

[Avi Craimer]

Thanks @David Wärn This gave me exactly the direction I needed to make it work!

inductive Rel : Type  where
  | Ind : Rel
  | NAry : (List Rel) -> Rel
deriving Repr
open Rel

inductive TermSyntax where
| var
| name
| abstraction
open TermSyntax

mutual
  inductive Term : Rel -> TermSyntax -> Type where
    | Name : (r:Rel) -> String -> Term r name
    | Variable: (r:Rel) -> String -> Term r var
    | abstraction : Formula -> Term relType var -> Term relType abstraction


  inductive Formula : Type where
    | atom :   (Term (NAry []) tSyn)  -> Formula
    | applied :  (rels: FullList Rel) -> (initialTerm:  Term (NAry (rels.toList)) tSyn)  ->
      (TermList rels) -> Formula
    | ifThen : Formula -> Formula -> Formula
    | not : Formula -> Formula
    | forAll : Formual -> Term relType var -> Formula
    | necessary : Formula -> Formula

  inductive TermList: FullList Rel ->  Type where
    | single :  (t: Term r tSyn) -> TermList (FullList.single r)
    | multi : (rels: FullList Rel) ->  Term (rels.head) tSyn -> TermList rels.tail ->  TermList rels
end

I didn't include the definition of FullList, but it's an inductive type like List except it always has at least one value.

So now I've finished the easy part of describing how terms and formulas are formed. The hard part is enforcing the extra constraints on the formation and introduction.

Universal quantification and abstraction both have the constraint that the variable being bound by $\lambda$ or $\forall$ cannot be an "initial" variable. That is it cannot be a variable that binds the second argument of the applied term constructor.

$R(x,y)$ can be made into $\lambda x. R(x,y)$ but not $\lambda R . R(x,y)$ however, if R is not initial it can be bound, e.g., where $\Phi$ is a relation from properties of individuals to individuals, the formula $\Phi(R, x)$ can be abstracted to $\lambda R . \Phi(R,x)$

Ideally, I'd like to make it impossible to construct invalid abstraction terms or forall formulas. But it might be a bit heavy to include this level of logic in the type definitions (and I'm not sure how I'd even do it). Another option is to have a set of designated term factory functions which apply these extra checks.

Does anybody have any ideas how to implement such constraints? Maybe there have been similar things done elsewhere.

---

Update: I realized that the easiest way to implement this is just to allow the use of initial variables as parameters but not to allow substitution for initial variables when doing beta-reduction.