Derivation calucli: meta functions vs. substitutions for equality elimination

Master / Vertiefung Wissensrepräsentation und -Verarbeitung
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Derivation calucli: meta functions vs. substitutions for equality elimination
In the section “Semantics: Absolute Semantics for BOL”, the lecture slides introduce an elimination rule for ≡:


(NB: there is a missing ⊢ in front of f(d); NB 2: contexts are left out in that part of the slides and in this post for readability)

Here, I suppose [m]f[/m] is a meta-level function from BOL concept expressions to BOL formula expressions.

Why cannot [m]f[/m] pattern-match on its argument and thus cheat its way through the rule?
Is this rule possibly only valid in foundations that disallow pattern-matching (e.g. LF, not CIC)?

Let me make my case more concrete. Say, we defined BOL’s grammar inductively in Coq:

[code]Inductive BOLConcept =
| conAtomic: string → BOLConcept
| conUnion: BOLConcept → BOLConcept → BOLConcept
| …
.

Inductive BOLFormula =
| formNeg: BOLFormula → BOLFormula (* negation; not part of the BOL version from lecture )
| formEquiv: BOLConcept → BOLConcept → BOLFormula ( in slides written as: 1 ≡ 2 )
| formSubsumption: BOLConcept → BOLConcept → BOLFormula ( 1 ⊑ 2 *)
| …
.
[/code]

Then we could define a Coq function [m]f: BOLConcept → BOLFormula[/m] such that

  • [m]f (conAtomic “x”) = formEquiv (conAtomic “x”) (conAtomic “x”)[/m], i.e., the return value is trivially provable in all contexts containing “x: concept”, and
  • [m]f (conAtomic “y”) = formNeg (formEquiv (conAtomic “x”) (conAtomic “x”))[/m], i.e., a contradiction in all contexts containing “x: concept”.

Now from [m]⊢ x ≡ y[/m] we would be able to infer [m]⊢ ¬(x ≡ x)[/m], a contradiction.

Would the following rule using substitutions instead of a meta function be better?

Assuming we would define a suitable notion of substitutions for BOL, of course.

3

In the rule, f(x) is a FOL-expression with a free variable x and f(e) is the notation for the result of substituting x with e in f.

That is common practice in paper descriptions of formal languages.

In some framework, notably LF but not Coq or Scala, we can use meta-level functions to represent expressions with free variables.
That is called higher-order abstract syntax.
In that case, we can mimic the paper notations elegantly in the framework, in particular with function application representing substitution.

Stronger meta-theories, in particular those allowing functions f that inspect their arguments such as by pattern-matching, cannot do this trick and need to represent substitutions and substitution applications explicitly.
In return, they can represent compositional translations as inductive functions.

The combination of the advantages of these two approaches is an open research problem.

1 „Gefällt mir“