# The MIT License (MIT)
# Copyright (c) 2016-2024 Objectionary.com
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
# The above copyright notice and this permission notice shall be included
# in all copies or substantial portions of the Software.
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.
title: "Rule set following Nov 2024 revision"
rules:
- name: DOT
description: 'Accessing an α-binding'
pattern: |
⟦ !τ ↦ !b, !B ⟧.!τ
result: |
⌈ !b , ⟦ !τ ↦ !b, !B ⟧ ⌉(ρ ↦ ⟦ !τ ↦ !b, !B ⟧)
when:
- nf: '!b'
- nf: '⟦ !B ⟧' #TODO: change the condition, every object in !B should be in the nf
tests:
- name: 'Contextualization changes ξ'
input: ⟦ a ↦ ξ ⟧.a
output: ['⟦ a ↦ ξ ⟧ (ρ ↦ ⟦ a ↦ ξ ⟧)']
- name: 'Contextualization applies recursively'
input: ⟦ a ↦ ξ.b ⟧.a
output: ['⟦ a ↦ ξ.b ⟧.b (ρ ↦ ⟦ a ↦ ξ.b ⟧)']
- name: Phi Paper - Example E2
input: '⟦ x ↦ ξ.t, t ↦ ∅ ⟧.x'
output: ['⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)']
- name: Phi Paper - Example E3 - first R_dot
input: '⟦ x ↦ ⟦t ↦ ⟦ρ ↦ ⟦⟧⟧⟧.t ⟧.x'
output: ['⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦t ↦ ⟦ρ ↦ ⟦⟧⟧⟧) ⟧.x']
- name: Phi Paper - Example E3 - second R_dot
input: '⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧.x'
output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦x ↦ ⟦ρ ↦ ⟦⟧⟧⟧)']
- name: Phi Paper - Example E4 - first R_dot
input: '⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.y'
output: ['⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧.x(ρ ↦ ⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧)']
- name: Phi Paper - Example E4 - second R_dot
input: ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.x(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)
output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)']
- name: Phi Paper - Example E5 - first R_dot
input: ⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.x ⟧
output: ['⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧']
- name: Phi Paper - Example E5 - second R_dot
input: ⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.φ.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧
output: ['⟦ m ↦ ⟦ t ↦ ⟦⟧ ⟧(ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧).t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧']
- name: COPY
description: 'Application of α-binding'
pattern: |
⟦ !τ1 ↦ ⟦ !τ2 ↦ ∅, !B1 ⟧(!τ2 ↦ !b, !B2) * !t, !B3 ⟧
result: |
⟦ !τ1 ↦ ⟦ !τ2 ↦ ⌈ !b , ⟦ !τ1 ↦ ⟦ !τ2 ↦ ∅, !B1 ⟧(!τ2 ↦ !b, !B2), !B3 ⟧ ⌉, !B1 ⟧(!B2) * !t, !B3 ⟧
when:
- nf: '!b'
- nf: '⟦ !B1 ⟧'
- nf: '⟦ !B3 ⟧'
tests:
- name: Should match
input: ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧
output: ['⟦ a ↦ ⟦ b ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧ ⟧ () ⟧']
- name: 'Should match'
input: ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ).a ⟧
output: ['⟦ a ↦ ⟦ b ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧ ⟧ ().a ⟧']
- name: Phi Paper - Example E1
input: ⟦ k ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧(t ↦ ⟦ρ ↦ ⟦⟧⟧) ⟧
# output: ['⟦ k ↦ ⟦ x ↦ ξ.t, t ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧() ⟧']
output: ['⟦ k ↦ ⟦ t ↦ ⟦ρ ↦ ⟦⟧⟧, x ↦ ξ.t ⟧() ⟧']
- name: Phi Paper - Example E4 - dispatch on y
input: ⟦ k ↦ ⟦ x ↦ ∅, y ↦ ξ.x ⟧(x ↦ ⟦ρ ↦ ⟦⟧⟧).y ⟧
output: ['⟦ k ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧().y ⟧']
- name: Phi Paper - Example E4 - remove dispatch on y
input: ⟦ k ↦ ⟦ x ↦ ∅, y ↦ ξ.x ⟧(x ↦ ⟦ρ ↦ ⟦⟧⟧) ⟧
output: ['⟦ k ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧() ⟧']
- name: RHO
description: 'Application of a ρ-binding'
pattern: |
⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧
result: |
⟦ !τ ↦ ⟦ !B1, ρ ↦ ⌈ !b , ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧ ⌉ ⟧(!B2) * !t, !B3 ⟧
when:
- nf: '!b'
- absent_attrs:
attrs: ['ρ']
bindings: ['!B1']
tests:
- name: Phi Paper - Example E5 - first R_rho
input: ⟦ m ↦ ⟦ t ↦ ⟦⟧ ⟧(ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧).t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧
output: ['⟦ m ↦ ⟦ t ↦ ⟦⟧, ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧ ⟧().t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧']
- name: phi
description: 'Accessing a decorated object'
pattern: |
⟦!B ⟧.!τ
result: |
⟦!B ⟧.φ.!τ
when:
- nf: '⟦ !B ⟧'
- present_attrs:
attrs: ['φ']
bindings: ['!B']
- absent_attrs:
attrs: ['!τ']
bindings: ['!B']
tests:
- name: Phi Paper - Example E5 - R_phi
input: ⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧
output: ['⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.φ.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧']
# there's no B2 in the result
- name: STAY
description: 'Application of a ρ-binding when ρ already exists'
pattern: |
⟦ ρ ↦ !b1, !B1 ⟧ (ρ ↦ !b, !B2)
result: |
⟦ ρ ↦ !b1, !B1 ⟧ (!B2)
when: []
tests:
- name: Phi Paper - Example E3 - first R_stay
input: ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧)(ρ ↦ ⟦ x ↦ ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧) ⟧)
output: [⟦ ρ ↦ ⟦⟧ ⟧()(ρ ↦ ⟦ x ↦ ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧) ⟧)]
- name: 'Should match'
input: '⟦ ρ ↦ ⟦ c ↦ ∅ ⟧ ⟧ (ρ ↦ ⟦ ⟧, b ↦ ξ)'
output: ['⟦ ρ ↦ ⟦ c ↦ ∅ ⟧ ⟧ (b ↦ ξ)']
- name: OVER
description: 'Invalid application (attribute already attached)'
pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2)
result: ⊥
when:
- not_equal: ['!τ', 'ρ']
tests:
- name: ''
input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
output: ['⊥']
- name: STOP
description: 'Absent attribute access'
pattern: |
⟦ !B ⟧.!τ
result: |
⊥
when:
- absent_attrs:
attrs: ['!τ', 'φ', 'λ']
bindings: ['!B']
- nf: '⟦ !B ⟧'
tests:
- name: 'Accessing nonexistent attribute'
input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x'
output: ['⊥']
- name: 'NULL'
description: 'Void attribute access'
pattern: |
⟦ !τ ↦ ∅, !B ⟧.!τ
result: |
⊥
when: []
tests:
- name: Phi Paper Example E2 second dispatch
input: '⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)'
output: ['⊥(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)']
- name: DUP
description: 'Empty application'
pattern: |
⟦ !B ⟧()
result: |
⟦ !B ⟧
when: []
tests:
- name: Should match
input: ⟦ a ↦ ⟦⟧ ⟧()
output: ['⟦ a ↦ ⟦⟧ ⟧']
- name: Should not match
input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧)
output: []
- name: Should match in subformation
input: ⟦ a ↦ ⟦ b ↦ ⟦⟧() ⟧ ⟧
output: ['⟦ a ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧']
- name: Should work with empty formation
input: ⟦⟧()
output: ['⟦⟧']
- name: Phi Paper - Example E5 - first R_rho
input: ⟦ m ↦ ⟦ t ↦ ⟦⟧, ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧ ⟧().t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧
output: ['⟦ m ↦ ⟦ t ↦ ⟦⟧, ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧']
- name: MISS
description: 'Invalid application (absent attribute)'
pattern: ⟦ !B1 ⟧(!τ ↦ !b, !B2)
result: ⊥
when:
- absent_attrs:
attrs: ['!τ']
bindings: ['!B1']
- not_equal: ['!τ', 'ρ']
tests:
- name: ''
input: '⟦ t1 ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
output: ['⊥']
- name: Should not match if attr is present
input: ⟦ t ↦ ⟦⟧ ⟧(t ↦ ⟦ a ↦ ∅ ⟧)
output: []
- name: Should not match for rho
input: ⟦ ⟧(ρ ↦ ⟦ ⟧)
output: []
- name: Should apply in subformations
input: ⟦ a ↦ ⟦ b ↦ ⟦⟧(t ↦ ⟦⟧) ⟧ ⟧
output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']
- name: DD
description: 'Accessing an attribute on bottom'
pattern: |
⊥.!τ
result: |
⊥
when: []
tests:
- name: 'Dispatch on bottom is bottom'
input: '⊥.a'
output: ['⊥']
- name: 'Dispatch on anything else is not touched'
input: '⟦ ⟧.a'
output: []
- name: DC
description: 'Application on bottom is bottom'
pattern: |
⊥(!B)
result: |
⊥
when: []
tests:
- name: Should apply in subformations
input: ⟦ a ↦ ⟦ b ↦ ⊥(t ↦ ⟦⟧, u ↦ ⟦⟧) ⟧ ⟧
output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']
- name: Phi Paper Example E2 last application
input: '⊥(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)'
output: ['⊥']