# From Cloud to Edge: Rethinking Generative AI for Low-Resource Design
Challenges

Sai Krishna Revanth Vuruma1, Ashley Margetts2, Jianhai Su3, Faez Ahmed2,
Biplav Srivastava3

###### Abstract

Generative Artificial Intelligence (AI) has shown tremendous prospects in all
aspects of technology, including design. However, due to its heavy demand on
resources, it is usually trained on large computing infrastructure and often
made available as a cloud-based service. In this position paper, we consider
the potential, challenges, and promising approaches for generative AI for
design on the edge, i.e., in resource-constrained settings where memory,
compute, energy (battery) and network connectivity may be limited.

Adapting generative AI for such settings involves overcoming significant
hurdles, primarily in how to streamline complex models to function efficiently
in low-resource environments. This necessitates innovative approaches in model
compression, efficient algorithmic design, and perhaps even leveraging edge
computing. The objective is to harness the power of generative AI in creating
bespoke solutions for design problems, such as medical interventions, farm
equipment maintenance, and educational material design, tailored to the unique
constraints and needs of remote areas. These efforts could democratize access
to advanced technology and foster sustainable development, ensuring universal
accessibility and environmental consideration of AI-driven design benefits.

## Introduction

In the rapidly evolving landscape of engineering design, the integration of
Artificial Intelligence (AI) has catalyzed a transformative shift. Generative
AI has been shown to revolutionize design processes (Regenwetter, Nobari, and
Ahmed 2022) and optimize functional performance across diverse domains ranging
from fashion (Sbai et al. 2018) to medicine (Walters and Murcko 2020).
However, a crucial aspect often overlooked in this digital renaissance is the
need for AI accessibility in remote or resource-constrained environments — a
realm where tiny, offline machine learning (ML) models may be needed.

The need for tiny AI models in remote areas exists for two main reasons.
Firstly, these regions frequently face challenges such as limited internet
connectivity and inadequate computational resources. In such scenarios, cloud-
dependent large AI models are impractical. Tiny ML models tailored for offline
use can overcome these barriers, bringing the power of advanced design tools
to isolated communities. This democratization not only fuels local innovation
but also ensures that cutting-edge AI-assisted design solutions are not the
exclusive domain of well-resourced urban centers.

Unique challenges in applications such as medicine, agriculture, and education
in remote areas could greatly benefit from compact, offline AI models. In
medical intervention, AI-driven design tools could assist in creating medical
devices, such as a ventilator, tailored for limited-resource settings,
focusing on affordability and ease of use while ensuring high efficacy. For
the repair of farm equipment such as irrigation pumps, AI can play a pivotal
role in predicting equipment failures or guiding repairs, adapted to the
specific machinery and agricultural practices of different regions. In the
context of school supplies, AI models could help design educational materials
like toys (Jain 2023) that are not only engaging and culturally relevant but
also accessible to students with limited resources.

Secondly, engineering design problems in remote areas often possess unique
contextual nuances - from local material constraints to specific environmental
considerations and product usage patterns. Offline ML models, trained on
relevant local data, can better capture and respond to these nuances, offering
more tailored and effective design solutions in spaces such as reliable sewage
repair or low-cost greenhouse design.

Moreover, these small AI models align with the principles of sustainable
technology deployment. By reducing reliance on large data centers and
continuous internet connectivity, they contribute to lower energy consumption
and a smaller carbon footprint, which is particularly crucial in ecologically
sensitive remote areas (Prakash et al. 2023).

The challenge lies in distilling the complexity of generative models into
lightweight versions without significant loss of functionality and
performance. This requires innovative approaches in model compression,
efficient algorithm design, and perhaps the use of edge computing
architectures.

## Review of Current Models

Generative AI techniques revolutionize the way machines can learn and
replicate human behavior. They use Machine Learning (ML) techniques to create
new data that is realistic and contextually relevant. Advances in Generative
AI, combined with the introduction of the transformer architecture with BERT
(Devlin et al. 2019) led to the development of Large Language Models (LLMs).

Prominent LLMs such as Meta’s LLAMA (Touvron et al. 2023), OpenAI’s ChatGPT
built on top of InstructGPT (Ouyang et al. 2022), have demonstrated remarkable
capabilities in understanding and generating human-like text with applications
ranging from sentiment analysis to chatbots. However, current models are
primarily limited to a few modalities (such as text-based conversational
agents).

Visual input is key to understanding the nuances of generating and
understanding designs. As a result, any potential Generative AI solution must
be able to process images as input and output. One potential solution to this
problem is Diffusion models such as OpenAI’s DALL-E (Ramesh et al. 2021),
Stability AI’s Stable Diffusion (Rombach et al. 2022) or one of their more
recent models SDXL (Podell et al. 2023), which have been shown to generate
high quality images from a text prompt. However, current diffusion models do
not present a complete solution, as they often require a meticulously crafted
prompt, which can be difficult to generate.

In addition, users should have the freedom to make changes to any design that
the model generates. Hence, the model must also support a back-and-forth
conversation with the user and adapt its responses accordingly. Vision
Language Models (VLMs) combine Computer Vision principles with Natural
Language Processing enabling them to generate content that has both image and
text modalities. For example, Flamingo (Alayrac et al. 2022), a popular VLM,
can be trained to do in-context few-shot learning in open-ended tasks, such as
visual-question answering. The input to Flamingo is a sequence of arbitrarily
interleaved text and images, while its output is only text. It cannot generate
any image data. Alternatively, Microsoft’s Visual ChatGPT (Wu et al. 2023) has
shown that it can generate images, support a conversation with the user,
whilst also making changes to its responses based on user requests. It
leverages Chain-of-Thought prompting (Wei et al. 2023) in combination with
incorporating different Visual Foundation Models (VFMs) with ChatGPT to help
process images. However, it needs significant prompt engineering and is
limited by the performance of ChatGPT and the various VFMs, all of which
affect its performance on any device.

Hence there is a need for multi-modal LLMs. Surveying the current landscape of
popular multi-modal LLMs, Meta’s ImageBind (Girdhar et al. 2023) can encode
information across six different modalities including text, audio, and video.
It has been shown to generate contextual embeddings across modalities and can
also match data across modalities through a similarity score. On the other
hand, Composable Diffusion (CoDi) (Tang et al. 2023) is designed to generate a
combination of different modularities given an input of a combination of
multiple modularities, e.g., text, image, video, and audio. Another prominent
model to consider is OpenAI’s GPT-4 (OpenAI 2023) which can process both image
and text data. A recent study in evaluating GPT-4V’s design generation
capability (Picard et al. 2023), has shown that the model displayed great
potential in conceptualizing design but it lacks precision with its responses
in later stages of design. Another key finding is that the model often
performs better when additional context is provided, and is dependent on
prompt engineering for optimal results.

While the current cloud-based models are imperfect tools for engineering
design tasks, we hypothesize that these models will improve significantly in
the near future, as more data and tools become available. No matter the
performance, current models can either be deployed on cloud servers and made
available to the public via the internet or offline if large computing and
memory infrastructures are in place. Neither of which is feasible in rural and
remote areas. This position paper considers how these large multi-modal LLMs
can be deployed on edge devices, which will be key when the models become
effective design assistants.

## Design for the Developing World

Offline ML models trained on local data have the potential to break through
constraints that keep many developing communities from the benefits of global
technological advancements. A paper outlining opportunities for mechanical
design advancements in the developing world (Mattson and Winter 2016)
describes how these communities have fundamentally different constraints than
those for which many technologies are developed, and that current optimization
techniques are catered towards the developed communities they were designed
by. One specific example described is sewage systems, which have been present
across the world for many years but have not reached many developing
communities (Mattson and Winter 2016). These observations lead to the
conclusion that there is great potential for the optimization of unique design
problems in unique communities.

### Predicting Potential Impacts

Before diving into AI-generated designs, we must also consider the
implications of designing for these communities. An article detailing
principles for design in the developing world emphasizes co-designing with
people from the specific community, testing the product in the actual setting,
and adapting technology and product management techniques to the specific
context (Mattson and Wood 2014). These principles prioritize participation of
the community and customization for the situation. Analysis of failure reports
identified the most common pitfall in designing for the developing world as
”Lacking the contextual knowledge needed for significant impact” (Wood and
Mattson 2016). Again, this highlights gaining understanding of a community’s
needs before embarking on design efforts. Collecting this information usually
requires direct human interaction, such as interviews and observational
studies, but frameworks have proposed combining direct data with indirect
data, such as sensors and satellites. These frameworks used deep learning
models with a combination of direct and indirect data to predict the social
impact of the use of a water hand pump in Uganda (Stringham et al. 2020).
Another study predicted the social impacts of deploying improved cook stoves
in Uganda using ML models (Mabey et al. 2023). By predicting these social
impacts, models can make better-informed decisions about an ideal design.

When considering design for these communities, we must consider the importance
of data collection and customization, as well as the potential contributions
that AI can bring to the analysis of this data. More specifically, we can
consider how offline AI models can promote participation of a community in
their own design decisions.

### Product Design and Repair

AI models have already shown their potential contributions to smart farming
systems, which use advanced technologies to facilitate labor reduction and
convenience. Using sensor and controller data collected from smart farms, an
error detection system using ontology and Recurrent Neural Networks was
developed and implemented (Choe and Lee 2023).

While these designs have been targeted towards more technologically advanced
communities, the process of reverse engineering, where designs are first made
for poorer countries and then adapted to wealthier countries, is becoming more
globally relevant. In a reverse engineering study, designers were able to meet
the specific needs of wheelchair users in the developing world, such as going
off road, which were not obvious in the developed world design space (Judge,
Hölttä-Otto, and Winter 2015).

A design activity by Penn State researchers identified low-cost greenhouse
designs, with the selection of materials optimized for the requirements of a
given location (BriteLab 2023). Both the development and deployment of these
designs was facilitated by outside sources. Offline AI models provide the
opportunity to improve the accessibility of design generation, allowing
communities to customize their designs without external support.

An example of this workflow is demonstrated in Figure 1, which shows a user
prompting CoDi to ”Design a Greenhouse Made of Wood”. In an ideal application,
the user would be provided with both photos and instructions for design. This
example shows some helpful images, but less helpful text outputs. Based on the
resources a community has access to, they could utilize AI models to customize
their designs.

Figure 1: Images and captions generated by CoDi given a wooden greenhouse
design request.

Another potential application involves providing those with limited resources
the opportunity to repair broken systems quickly and without outside support.
More specifically, we can return to a sewage system and imagine a water pump
stops functioning in a remote area. Instead of waiting for a repairman or a
replacement part to arrive, a user could input text with requirements and
images of broken components. Light-weight, more accessible models could parse
this multi-modal input to propose repair solutions and specific design
suggestions in text and image format. An example of this workflow is shown in
Figure 2, where we inputted an image of a water pump assembly and asked for a
replacement valve design. CoDi then generated example images of replacement
parts and captions. The current state of this model does not provide
particularly helpful design outputs but demonstrates a potentially effective
interaction with a user. If trained on specific relevant data, this method
would be much more efficient than waiting for outside help or replacement
parts, and much more customizable than the design solutions that currently
exist for more developed communities.

Figure 2: Images and captions generated by CoDi given a design replacement
intent.

Most mechanical design efforts are focused on more resource-heavy communities.
Offline models provide an opportunity to customize a generated design to a
given set of constraints.

## Potential Solutions

In this section, we discuss some of the ways one can address the challenges
faced by resource-constrained areas in accessing large AI models like Language
Models (LLMs).

The most common solution is fine-tuning for Cloud-based solutions as some
resource-constrained areas may have internet access. In such areas, users can
access cloud services with minimal local computing resources. Efforts to
optimize data transfer and enable low-bandwidth operation are key in this
approach. With in-context learning, the models can potentially be adapted to
local needs. However, in this paper, we do not focus on these cloud-only
solutions. Instead, our focus is on offline AI solutions.

Academics and industry are contributing to open-source projects and community-
driven initiatives that aim to make AI more accessible. This includes sharing
resources, providing training, and supporting local developers in creating
solutions tailored to their specific needs. However, these open source models
could still be large and need significant compute resources to train. Below,
we discuss a few key solutions to make them more accessible and suitable for
deployment on the edge.

### Model Compression and Optimization

Deploying AI models on edge devices is far from straightforward. Due to memory
and computing constraints, not all models can be run on the edge. There is a
need for more efficient models that require less computational power. This is
even more pronounced when dealing with LLMs. Their higher memory and
processing requirements aren’t practical for computing at the edge, thus
making them less accessible. One of the ways to achieve this is to make these
models smaller for inference using methods like:

  * •

Model Pruning: The process of removing non-critical and redundant components
of a model without a significant loss in performance. With respect to LLMs,
this can mean removing weights with smaller gradients or magnitudes and
parameter reduction among others. Novel pruning methods like Wanda (Sun et al.
2023) and LLM-Pruner (Ma, Fang, and Wang 2023) present optimal solutions for
making LLMs smaller.

  * •

Quantization: Representing model parameters such as weights in a lower
precision, i.e. using fewer bits to store the value (Gholami et al. 2021).
This results in a smaller model size, faster inference, and a reduced memory
footprint. LLM Quantization can be achieved either in the post-training phase
(Dettmers et al. 2022) or during the pre-training or fine-tuning phase (Liu et
al. 2023).

  * •

Knowledge Distillation: Transferring the knowledge of a large teacher model to
a smaller learner model to replicate the original model’s output distribution
difference. Knowledge Distillation has been widely used to reduce LLMs like
BERT into smaller distilled versions DistilBERT (Sanh et al. 2020). More
recently, approaches like MiniLLM (Gu et al. 2023) and (Hsieh et al. 2023)
further optimize the distillation process to improve the student model’s
performance and inference speed.

### Edge Computing

Edge computing involves processing data closer to the location where it is
needed, rather than relying on a central data-processing warehouse. This can
significantly reduce the need for continuous, high-speed internet
connectivity. One solution is to deploy AI models on edge devices, like
smartphones and local servers, which can operate with intermittent
connectivity (Singh and Gill 2023; Marculescu, Marculescu, and Ogras 2020).

### Evaluation Metrics

Depending on the design objective and types of constraints, metrics can be
defined to evaluate the performance of a model. Selection of these metrics is
crucial, but can also vary greatly depending on the representation scheme, the
cost of metric evaluation, and the use case. Examples of common metrics within
the 3D design space can include statistical similarity to highly performing
designs, diversity in design candidates and design performance evaluations
(Regenwetter et al. 2023). When applied to offline models, we will need to
consider metrics that have low-resource evaluation capabilities and prioritize
low cost and performance in designs.

Other solutions for the lack of computational resources also exist. For
example, the development of custom hardware, like specialized AI chips, can
offer a more cost-effective and power-efficient way of running AI models.
These chips can be integrated into everyday devices, reducing the need for
powerful standalone computers. There’s also an emerging trend of using
multiple devices to share computational tasks. This distributed approach can
help overcome individual device limitations. Finally, there is also a need for
establishing data centers closer to resource-constrained areas to reduce
latency and improve access. This approach, however, requires significant
investment and infrastructure development.

## Discussion: Edge AI and Tiny ML

As discussed in the Review section, existing approaches like LLMs, Diffusion
models and VLMs have significant computing requirements owing to their large
parameter space which make them imperfect candidates for deployment on edge
devices. On top of the optimization and compression techniques mentioned in
the Potential Solutions section, more work needs to be done both on the
hardware and software side to increase their accessibility (Lin et al. 2023).

Recent research in Edge AI (Murshed et al. 2021; Lee, Tsung, and Wu 2018) has
shown that optimized model architectures and new embedded system technologies
improved system response times as well as user security. Similarly, TinyML is
a field of Machine Learning that deals with deploying lighter models in
resource-constrained devices that have limited computing infrastructure.
Certain key aspects of TinyML include reducing latency by leveraging edge
computing, optimizing models for computing at the edge and developing new
tools and equipment that can facilitate running ML models on edge devices.
These features enable TinyML models to provide increased user privacy due to
data being processed locally, reduced power consumption and internet usage
(Dutta and Bharali 2021; Ray 2022).

The findings from these both of these fields are crucial in realizing the goal
of democratizing Generative AI for computing at the edge.

## Conclusion

With this position paper, we want to continue the discussion on making
Generative AI models more accessible and increasing their reach to rural and
remote areas. Researchers developing solutions for data-driven design
challenges must look to create models that can also work in resource-
constrained environments, not just on the cloud. The future of AI in design at
the edge is not just about technological innovation but also about equitable
access and sustainability. It is about bringing the power of AI-driven design
to every corner of the globe, ensuring that even the most remote communities
can benefit from the advancements in AI for engineering and design solutions.

## References

  * Alayrac et al. (2022) Alayrac, J.-B.; Donahue, J.; Luc, P.; Miech, A.; Barr, I.; Hasson, Y.; Lenc, K.; Mensch, A.; Millican, K.; Reynolds, M.; et al. 2022.  Flamingo: a visual language model for few-shot learning.  _Advances in Neural Information Processing Systems_ , 35: 23716–23736.
  * BriteLab (2023) BriteLab, P. 2023.  Greenhouse Grid Design Task.  Accessed: 11-28-2023.
  * Choe and Lee (2023) Choe, H. O.; and Lee, M.-H. 2023.  Artificial Intelligence-Based Fault Diagnosis and Prediction for Smart Farm Information and Communication Technology Equipment.  _Agriculture_ , 13(11): 2124.
  * Dettmers et al. (2022) Dettmers, T.; Lewis, M.; Belkada, Y.; and Zettlemoyer, L. 2022.  LLM.int8(): 8-bit Matrix Multiplication for Transformers at Scale.  arXiv:2208.07339.
  * Devlin et al. (2019) Devlin, J.; Chang, M.-W.; Lee, K.; and Toutanova, K. 2019.  BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding.  arXiv:1810.04805.
  * Dutta and Bharali (2021) Dutta, L.; and Bharali, S. 2021.  Tinyml meets iot: A comprehensive survey.  _Internet of Things_ , 16: 100461.
  * Gholami et al. (2021) Gholami, A.; Kim, S.; Dong, Z.; Yao, Z.; Mahoney, M. W.; and Keutzer, K. 2021.  A Survey of Quantization Methods for Efficient Neural Network Inference.  arXiv:2103.13630.
  * Girdhar et al. (2023) Girdhar, R.; El-Nouby, A.; Liu, Z.; Singh, M.; Alwala, K. V.; Joulin, A.; and Misra, I. 2023.  ImageBind: One Embedding Space To Bind Them All.  In _CVPR_.
  * Gu et al. (2023) Gu, Y.; Dong, L.; Wei, F.; and Huang, M. 2023.  Knowledge Distillation of Large Language Models.  arXiv:2306.08543.
  * Hsieh et al. (2023) Hsieh, C.-Y.; Li, C.-L.; Yeh, C.-K.; Nakhost, H.; Fujii, Y.; Ratner, A.; Krishna, R.; Lee, C.-Y.; and Pfister, T. 2023.  Distilling Step-by-Step! Outperforming Larger Language Models with Less Training Data and Smaller Model Sizes.  arXiv:2305.02301.
  * Jain (2023) Jain, M. 2023.  Center for Creative Learning - Toys and Activities.  In _https://www.ccl.iitgn.ac.in/toys_.
  * Judge, Hölttä-Otto, and Winter (2015) Judge, B. M.; Hölttä-Otto, K.; and Winter, A. G. 2015.  Developing world users as lead users: a case study in engineering reverse innovation.  _Journal of Mechanical Design_ , 137(7): 071406.
  * Lee, Tsung, and Wu (2018) Lee, Y.-L.; Tsung, P.-K.; and Wu, M. 2018.  Techology trend of edge AI.  In _2018 International Symposium on VLSI Design, Automation and Test (VLSI-DAT)_ , 1–2.
  * Lin et al. (2023) Lin, Z.; Qu, G.; Chen, Q.; Chen, X.; Chen, Z.; and Huang, K. 2023.  Pushing Large Language Models to the 6G Edge: Vision, Challenges, and Opportunities.  arXiv:2309.16739.
  * Liu et al. (2023) Liu, Z.; Oguz, B.; Zhao, C.; Chang, E.; Stock, P.; Mehdad, Y.; Shi, Y.; Krishnamoorthi, R.; and Chandra, V. 2023.  LLM-QAT: Data-Free Quantization Aware Training for Large Language Models.  arXiv:2305.17888.
  * Ma, Fang, and Wang (2023) Ma, X.; Fang, G.; and Wang, X. 2023.  LLM-Pruner: On the Structural Pruning of Large Language Models.  arXiv:2305.11627.
  * Mabey et al. (2023) Mabey, C. S.; Peiffer, E. E.; MacCarty, N.; and Mattson, C. A. 2023.  Simulating the Adoption and Social Impact of Improved Cookstoves in Uganda Using Agent-Based Modeling and Neural Networks.  _Journal of Mechanical Design_ , 145(12).
  * Marculescu, Marculescu, and Ogras (2020) Marculescu, R.; Marculescu, D.; and Ogras, U. 2020.  Edge AI: Systems Design and ML for IoT Data Analytics.  In _Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining_, KDD ’20, 3565–3566. New York, NY, USA: Association for Computing Machinery.  ISBN 9781450379984.
  * Mattson and Winter (2016) Mattson, C. A.; and Winter, A. G. 2016.  Why the developing world needs mechanical design.  _Journal of Mechanical Design_ , 138(7): 070301.
  * Mattson and Wood (2014) Mattson, C. A.; and Wood, A. E. 2014.  Nine principles for design for the developing world as derived from the engineering literature.  _Journal of Mechanical Design_ , 136(12): 121403.
  * Murshed et al. (2021) Murshed, M. G. S.; Murphy, C.; Hou, D.; Khan, N.; Ananthanarayanan, G.; and Hussain, F. 2021.  Machine Learning at the Network Edge: A Survey.  _ACM Computing Surveys_ , 54(8): 1–37.
  * OpenAI (2023) OpenAI. 2023.  GPT-4 Technical Report.  arXiv:2303.08774.
  * Ouyang et al. (2022) Ouyang, L.; Wu, J.; Jiang, X.; Almeida, D.; Wainwright, C. L.; Mishkin, P.; Zhang, C.; Agarwal, S.; Slama, K.; Ray, A.; Schulman, J.; Hilton, J.; Kelton, F.; Miller, L.; Simens, M.; Askell, A.; Welinder, P.; Christiano, P.; Leike, J.; and Lowe, R. 2022.  Training language models to follow instructions with human feedback.  arXiv:2203.02155.
  * Picard et al. (2023) Picard, C.; Edwards, K. M.; Doris, A. C.; Man, B.; Giannone, G.; Alam, M. F.; and Ahmed, F. 2023.  From Concept to Manufacturing: Evaluating Vision-Language Models for Engineering Design.  arXiv:2311.12668.
  * Podell et al. (2023) Podell, D.; English, Z.; Lacey, K.; Blattmann, A.; Dockhorn, T.; Müller, J.; Penna, J.; and Rombach, R. 2023.  SDXL: Improving Latent Diffusion Models for High-Resolution Image Synthesis.  arXiv:2307.01952.
  * Prakash et al. (2023) Prakash, S.; Stewart, M.; Banbury, C.; Mazumder, M.; Warden, P.; Plancher, B.; and Reddi, V. J. 2023.  Is TinyML Sustainable? Assessing the Environmental Impacts of Machine Learning on Microcontrollers.  _arXiv preprint arXiv:2301.11899_.
  * Ramesh et al. (2021) Ramesh, A.; Pavlov, M.; Goh, G.; Gray, S.; Voss, C.; Radford, A.; Chen, M.; and Sutskever, I. 2021.  Zero-Shot Text-to-Image Generation.  arXiv:2102.12092.
  * Ray (2022) Ray, P. P. 2022.  A review on TinyML: State-of-the-art and prospects.  _Journal of King Saud University-Computer and Information Sciences_ , 34(4): 1595–1623.
  * Regenwetter, Nobari, and Ahmed (2022) Regenwetter, L.; Nobari, A. H.; and Ahmed, F. 2022.  Deep generative models in engineering design: A review.  _Journal of Mechanical Design_ , 144(7): 071704.
  * Regenwetter et al. (2023) Regenwetter, L.; Srivastava, A.; Gutfreund, D.; and Ahmed, F. 2023.  Beyond statistical similarity: Rethinking metrics for deep generative models in engineering design.  _arXiv preprint arXiv:2302.02913_.
  * Rombach et al. (2022) Rombach, R.; Blattmann, A.; Lorenz, D.; Esser, P.; and Ommer, B. 2022.  High-Resolution Image Synthesis with Latent Diffusion Models.  arXiv:2112.10752.
  * Sanh et al. (2020) Sanh, V.; Debut, L.; Chaumond, J.; and Wolf, T. 2020.  DistilBERT, a distilled version of BERT: smaller, faster, cheaper and lighter.  arXiv:1910.01108.
  * Sbai et al. (2018) Sbai, O.; Elhoseiny, M.; Bordes, A.; LeCun, Y.; and Couprie, C. 2018.  DesIGN: Design Inspiration from Generative Networks.  In _Proceedings of the European Conference on Computer Vision (ECCV) Workshops_.
  * Singh and Gill (2023) Singh, R.; and Gill, S. S. 2023.  Edge AI: a survey.  _Internet of Things and Cyber-Physical Systems_.
  * Stringham et al. (2020) Stringham, B. J.; Smith, D. O.; Mattson, C. A.; and Dahlin, E. C. 2020.  Combining direct and indirect user data for calculating social impact indicators of products in developing countries.  _Journal of Mechanical Design_ , 142(12): 121401.
  * Sun et al. (2023) Sun, M.; Liu, Z.; Bair, A.; and Kolter, J. Z. 2023.  A Simple and Effective Pruning Approach for Large Language Models.  arXiv:2306.11695.
  * Tang et al. (2023) Tang, Z.; Yang, Z.; Zhu, C.; Zeng, M.; and Bansal, M. 2023.  Any-to-Any Generation via Composable Diffusion.  _arXiv preprint arXiv:2305.11846_.
  * Touvron et al. (2023) Touvron, H.; Lavril, T.; Izacard, G.; Martinet, X.; Lachaux, M.-A.; Lacroix, T.; Rozière, B.; Goyal, N.; Hambro, E.; Azhar, F.; Rodriguez, A.; Joulin, A.; Grave, E.; and Lample, G. 2023.  LLaMA: Open and Efficient Foundation Language Models.  Cite arxiv:2302.13971.
  * Walters and Murcko (2020) Walters, W. P.; and Murcko, M. 2020.  Assessing the impact of generative AI on medicinal chemistry.  _Nature biotechnology_ , 38(2): 143–145.
  * Wei et al. (2023) Wei, J.; Wang, X.; Schuurmans, D.; Bosma, M.; Ichter, B.; Xia, F.; Chi, E.; Le, Q.; and Zhou, D. 2023.  Chain-of-Thought Prompting Elicits Reasoning in Large Language Models.  arXiv:2201.11903.
  * Wood and Mattson (2016) Wood, A. E.; and Mattson, C. A. 2016.  Design for the developing world: Common pitfalls and how to avoid them.  _Journal of Mechanical Design_ , 138(3): 031101.
  * Wu et al. (2023) Wu, C.; Yin, S.; Qi, W.; Wang, X.; Tang, Z.; and Duan, N. 2023.  Visual ChatGPT: Talking, Drawing and Editing with Visual Foundation Models.  arXiv:2303.04671.


# Matching-Logic-Based Understanding of Polynomial Functors and their
Initial/Final Models

Dorel Lucanu Alexandru Ioan Cuza University of Iași, Romania
<EMAIL_ADDRESS>
###### Abstract

In this paper, we investigate how the initial models and the final models for
the polynomial functors can be uniformly specified in matching logic.

##  1 Introduction

It is known that many data types used in programming are defined as initial
algebra or final coalgebra for an appropriate functor
$F:\mathbb{C}\to\mathbb{C}$, where $\mathbb{C}$ is a category of data types.
In this paper we assume that $\mathbb{C}$ is the category of sets (see, e.g.,
[3]). If $F$ is bicontinous, i.e., it preserves the colimits of
$\omega$-sequences and and the limits of $\omega^{\mathit{op}}$-sequences,
then the initial algebra (model) is obtained via colimit of the
$\omega$-sequence

$\mathbf{0}\xrightarrow{\raisebox{2.0pt}{\hbox{!`}}}F\;\mathbf{0}\xrightarrow{F\;\raisebox{2.0pt}{\hbox{!`}}}F\;F\;\mathbf{0}=F^{2}\;\mathbf{0}\xrightarrow{F^{2}\;\raisebox{2.0pt}{\hbox{!`}}}F^{3}\;\mathbf{0}\xrightarrow{F^{3}\;\raisebox{2.0pt}{\hbox{!`}}}\cdots$

where $\mathbf{0}$ is the initial object in $\mathbb{C}$, and
$\mathbf{0}\xrightarrow{\raisebox{2.0pt}{\hbox{!`}}}X$ is the unique arrow
from the initial object, and the final coalgebra (model) is the limit of the
$\omega^{\mathit{op}}$-sequence

$\mathbf{1}\xleftarrow{\hbox{!}}F\;\mathbf{1}\xleftarrow{F\;\hbox{!}}F\;F\;\mathbf{1}=F^{2}\;\mathbf{1}\xleftarrow{F^{2}\;\hbox{!}}F^{3}\;\mathbf{1}\xleftarrow{F^{3}\;\hbox{!}}\cdots$

where $\mathbf{1}$ is the final object in $\mathbb{C}$, and
$\mathbf{1}\xleftarrow{\hbox{!}}X$ is the unique arrow to the final object
[3].

This is a nice abstract framework, but, as we know, the evil is hidden in
details. How the elements of the initial and final models look like for
various concrete functors? How could they be handled in practice?

A possible answer can be obtained by capturing these objects in Matching Logic
(ML), the logical foundation of the K Framework, where the program languages
and the properties of their programs can be specified in a uniform way (see,
e.g., [13, 9, 14, 8, 12]). First steps are done in [7], where the initial
algebra semantics is captured in ML, and in [8], where it is shown how
examples of inductive/coinductive data types are fully specified in ML. We say
that ML captures a (inductive/coinductive) data type $\mathit{DT}$ if there is
an ML theory $\mathsf{Th}^{\sf ML}(\mathit{DT})$ such that:

  * •

from each $\mathsf{Th}^{\sf ML}(\mathit{DT})$-model $M$ we may extract a
structure $\alpha(M)$ that is isomorphic to $\mathit{DT}$, and

  * •

each deduction principle for $\mathit{DT}$ (e.g., induction or coinduction)
can be expressed as a theorem within ML using its proof system.

In this paper, we investigate how data types specified as initial $F$-algebras
or as a final $F$-coalgebras, where $F$ is a polynomial functor, can be
captured in ML. The polynomial functors can be defined in two ways:

  1. 1.

Using ”classical” inductive definition of polynomials (see, e.g., [15]): the
polynomial functors is the smallest class including the constant and the
identity functors, and it is closed to sum, product, and constant-exponent
functors.

  2. 2.

Using unary container functors (see, e.g.,[4]): a polynomial functor is of the
form $X\mapsto\sum_{a:A}X^{B[a]}$, where $a:A\vdash B[a]$ is an $A$-indexed
family.

The constant and the identity functors, together with their initial and final
models, can be easily captured in ML. Moreover, if we exclude the exponent
functor, then the initial algebra can be captured using the approach similar
to that from [7]. The exponent functor complicates the things. A possible
approach for the classical definition is as follows: supposing that we have
captured $F_{1}\;X$ and $F_{2}\;X$ by the ML theories (specifications)
$\mathrm{SPEC}(F_{1}\;X)$ and resp. $\mathrm{SPEC}(F_{2}\;X)$, then use these
specifications to build $\mathrm{SPEC}(F_{1}\;X~{}\mathit{op}~{}F_{2}\;X)$,
i,.e., to obtain something like

$\mathrm{SPEC}(F_{1}\;X~{}\mathit{op}~{}F_{2}\;X)=\mathrm{SPEC}(F_{1}\;X)~{}\overline{\mathit{op}}~{}\mathrm{SPEC}(F_{2}\;X)$

where $\overline{\mathit{op}}$ reflects $\mathit{op}$ to the level of ML
specifications, and it follows to be defined. In order to accomplish that, we
need a ”uniform standard” definition for the specifications
$\mathrm{SPEC}(F\;X)$.

The container functors already have a uniform standard definition, and
therefore they are more tempting for our investigation. This approach is a
work-in-progress, and the results obtained up now show that:

  * •

it is possible to specify unary container functors, together with their
initial algebras and final coalgebras, as ML theories;

  * •

it is possible to derive the induction principle and the coinduction principle
as theorems of the corresponding theories;

  * •

the ML reasoning can be used to understand better the intimate structure of
the initial algebra and the final coalgebra.

The approach is instantiated on the lists example, in order to see the
relationship with the classical approach of these data types, and on that of
Moore machines, in order to see the (constant) exponential functor at work.

The paper is structured as follows. Section 2 recalls the definitions for
polynomial functors and for unary container functors, and the the relationship
between them. Section 3 briefly recalls the main elements of matching logic,
together with the theories of the equality and of the sorts. Section 4
includes the main contribution, showing that how the unary container functors
and their related concepts can be specified in matching logic. The
instantiation of the general approach on the examples of lists and Moore
machines are included in Section 5 and Section 6, respectively. The paper ends
with some concluding remarks.

##  2 Polynomials Functors

This section briefly recalls the definition of the polynomial functors and
their (co)algebras. We consider only the particular case of the functors
defined over the category of sets $\mathbb{C}$.

######  Definition 2.1.

[11] Given a functor $F:\mathbb{C}\to\mathbb{C}$, an _$F$ -algebra_ consists
of an object $X$ in $\mathbb{C}$ and an arrow $\alpha:F\;X\to X$. An algebra
morphism $(X,\alpha)\to(X^{\prime},\alpha^{\prime})$ is an arrow $h:X\to
X^{\prime}$ in $\mathbb{C}$ such that $h\circ\alpha=\alpha^{\prime}\circ
F\;h$. An _initial algebra_ for the functor $F$ is an initial object in the
category of $F$-algebras and $F$-algebra morphisms.

######  Example 2.1 (Lists).

The lists over a set of elements $E$ can be defined as an $L$-algebra
$\alpha:L\;X\to X$ for the functor $L:\mathbb{C}\to\mathbb{C}$ given by
$L\;X=\mathbf{1}+E\times X$. Usually, such an algebra is defined by a constant
$\mathit{nil}:\mathbf{1}\to X$ and a binary operation $\mathit{cons}:E\times
X\to X$. The initial $L$-algebra is isomorphic to the finite lists inductively
defined [16] by the grammar

$\displaystyle\mathit{List}::=nil\mid\mathit{cons}(E,\mathit{List})$ (Lst)

We use $\mu X\mathord{.\;}L\;X$ or $\mu L$ to denote the initial model of the
functor $L$.

######  Definition 2.2.

[11] Given a functor $F:\mathbb{C}\to\mathbb{C}$, an _$F$ -coalgebra_ consists
of an object $X$ in $\mathbb{C}$ and an arrow $\gamma:X\to F\;X$. A coalgebra
morphism $(X,\gamma)\to(X^{\prime},\gamma^{\prime})$ is an arrow $h:X\to
X^{\prime}$ in $\mathbb{C}$ such that $h\circ\gamma=\gamma^{\prime}\circ
F\;h$. An _final coalgebra_ for the functor $F$ is a final object in the
category of $F$-coalgebras and $F$-coalgebra morphisms.

######  Example 2.2 (Colists).

The colists over a set of elements $E$ can be defined as an $L$-coalgebra
$\gamma:X\to L\;X$, where $L$ is the functor used for lists (see Example 2.1).
Usually, such a coalgebra is defined by

  * •

a total operation ${\\_}\mathord{.\;}\\!\\!?:X\to\\{1,2\\}$ such that
$x\mathord{.\;}\\!\\!?=\mathsf{if}~{}g(x)=\iota_{1}(\star)~{}\mathsf{then}~{}1~{}\mathsf{else}~{}2~{}\mathsf{fi}$,
where $\star$ is the unique element of $\mathbf{1}$, and

  * •

two partial operations: ${\\_}\mathord{.\;}\mathit{hd}:X\rightharpoonup E$,
and ${\\_}\mathord{.\;}\mathit{tl}:X\rightharpoonup X$ such that
$x\mathord{.\;}\mathit{hd}=e$ and $x\mathord{.\;}\mathit{tl}=x^{\prime}$ iff
$x\mathord{.\;}\\!\\!?=2$ and $g(x)=\iota_{2}(\left\langle
e,x^{\prime}\right\rangle)$.

The final coalgebra is isomorphic to the possible infinite lists coinductively
defined by the grammar (Lst) [16]. We use $\nu X\mathord{.\;}L\;X$ or $\nu L$
to denote the final model of the functor $L$.

######  Example 2.3 (Moore machines).

A Moore machine is an $M$-coalgebra $\alpha:X\to M\;X$, where $M$ is the
functor $M:X\to O\times X^{I}$. Usually, a Moore machine is defined by an
_output_ function $\mathit{out}:X\to O$ and a _transition_ function
$\mathit{tr}:X\to X^{I}$ [15]. The final coalgebra $\nu X\mathord{.\;}M\;X$ is
isomorphic to $(\overline{\mathit{out}},\overline{\mathit{tr}}):O^{I^{*}}\to
O\times(O^{I^{*}})^{I}$, $\overline{\mathit{out}}(f)=f(\varepsilon)$,
$\overline{\mathit{tr}}(f)=g$ with $g(i)(w)=f(\langle i\rangle\cdot w)$ for
$i\in I$ and $w\in I^{*}$, where $f$ is a function $F:I^{*}\to O$, $g$ a
function $g:I\to O^{I^{*}}$, $\varepsilon$ the empty sequence, and $\cdot$ the
concatenation of sequences.

######  Definition 2.3.

[15] The class of _polynomial functors_ is inductively defined as follows:

  * •

the constant functor $A$ (where $A$ is an object in $\mathbb{C}$) is a
polynomial functor;

  * •

the identity functor $\mathit{ID}$ is a polynomial functor;

  * •

the sum $F_{1}+F_{2}$ of two polynomial functors $F_{1}$ and $F_{2}$ is a
polynomial functor;

  * •

the product $F_{1}\times F_{2}$ of two polynomial functors $F_{1}$ and $F_{2}$
is a polynomial functor; and

  * •

the function space functor $F(X)=X^{A}$, where A is an arbitrary object.

An alternative to define polynomial functors is given by the (unary) container
functors [2, 5, 4].

######  Definition 2.4.

An _$A$ -indexed family $a:A\vdash B[a]$_ is a family of objects of
$\mathbb{C}$ indexed by elements of $A$. Categorically, it is an object $B$ of
$\mathbb{C}/A$ and $B[a]$ denotes the elements of $B$ mapped to $a$.

######  Definition 2.5.

Given an $A$-indexed family $a:A\vdash B[a]$, the _dependent product_
$\prod_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]$ is the object of the
_dependent functions_ , which maps an $a{\kern 0.86108pt:\kern 0.86108pt}A$
into a $b{\kern 0.86108pt:\kern 0.86108pt}B[a]$. Set theoretically, we have

$\prod_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]=\left\\{f\in(\bigcup_{a{\kern
0.60275pt:\kern 0.60275pt}A}B[a])^{A}\middle\mid\forall a{\kern
0.86108pt:\kern 0.86108pt}A.f(a)\in B[a]\right\\}$

The _dependent sum_ $\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]$ is the
dual of the dependent product and it consists of the pairs $\left\langle
a,b\right\rangle$ with $a{\kern 0.86108pt:\kern 0.86108pt}A$ and $b{\kern
0.86108pt:\kern 0.86108pt}B[a]$.

######  Definition 2.6.

A functor $F:\mathbb{C}\to\mathbb{C}$ is a _(unary) container functor_ iff it
is naturally isomorphic to a functor of the form $F\;X=\sum_{a{\kern
0.60275pt:\kern 0.60275pt}A}X^{B[a]}$, for some objects $A$ in $\mathbb{C}$
and an $A$-indexed family $a{\kern 0.86108pt:\kern 0.86108pt}A\vdash B[a]$.

######  Remark.

An element of $\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}X^{B[a]}$ is a pair
$\left\langle a,f\right\rangle$, where $a{\kern 0.86108pt:\kern 0.86108pt}A$
is the _shape_ and $f:B[a]\to X$ is the function that labels the _positions_
$B[a]$ with elements from $X$. Another way to define $B$ is as an object in
$\mathbb{C}/A$.

###  2.1 Polynomial Functors as Container Functors

Here we recall the relationship between polynomial functors and container
functors (see, e.g., [2]).

#### Constant Functor

The main idea is to identify the constant value with the shapes $A$. Consider
$B$ as being $a{\kern 0.86108pt:\kern 0.86108pt}A\vdash\mathbf{0}$ (no
positions of shape $a$), where $\mathbf{0}$ denotes the initial object of
$\mathbb{C}$. We get $\sum_{a{\kern 0.60275pt:\kern
0.60275pt}A}X^{B[a]}\approxeq\sum_{a{\kern 0.60275pt:\kern
0.60275pt}A}X^{\mathbf{0}}\approxeq A$.

######  Remark.

The elements of $\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}X^{\mathbf{0}}$ are
pairs $\left\langle a,f:\mathbf{0}\to X\right\rangle$, where $a\in A$. Since
$f:\mathbf{0}\to X$ is unique, we obtain $\left\langle a,f:\mathbf{0}\to
X\right\rangle\approxeq a$.

#### Identity Functor

Consider $A$ as being $\mathbf{1}$ (just one shape) and $B$ as being
$\star{\kern 0.86108pt:\kern 0.86108pt}\mathbf{1}\vdash\mathbf{1}$ (just one
position), where $\star$ is the unique element in $\mathbf{1}$. It follows
that $\sum_{a{\kern 0.60275pt:\kern
0.60275pt}A}X^{B[a]}\approxeq\sum_{\star}X^{\mathbf{1}}\approxeq X$.

######  Remark.

The elements of $\sum_{\star}X^{\mathbf{1}}$ are pairs
$\left\langle\star,f:\mathbf{1}\to X\right\rangle$. Since $f$ selects just one
element $x$ in $X$, it follows that $\left\langle\star,f:\mathbf{1}\to
X\right\rangle\approxeq x$.

#### Sum

Assume that $F\;X=\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}X^{B[a]}$ and
$F^{\prime}\;X=\sum_{a^{\prime}{\kern 0.60275pt:\kern
0.60275pt}A^{\prime}}X^{B^{\prime}[a]^{\prime}}$. Then $(F+F^{\prime})\;X$ is
$\sum_{a^{\prime\prime}{\kern 0.60275pt:\kern
0.60275pt}A+A^{\prime}}X^{[B,B^{\prime}][a^{\prime\prime}]}$, where
$[B,B^{\prime}][a^{\prime\prime}]=B[a]$ if $a^{\prime\prime}=\iota_{1}\;a$,
and $[B,B^{\prime}][a^{\prime\prime}]=B^{\prime}[a^{\prime}]$ if
$a^{\prime\prime}=\iota_{2}\;a^{\prime}$.

######  Remark.

The following commutative diagram may help to understand the definition of
$a^{\prime\prime}{\kern 0.86108pt:\kern
0.86108pt}A+A^{\prime}\vdash[B,B^{\prime}][a^{\prime\prime}]$:

${A+A^{\prime}}$${A}$${A^{\prime}}$${B}$$B+B^{\prime}$${B^{\prime}}$$\scriptstyle{\iota_{1}}$$\scriptstyle{\iota_{2}}$

The arrow $B+B^{\prime}\to A+A^{\prime}$ is equivalently written as the
$A+A^{\prime}$-indexed set $a^{\prime\prime}{\kern 0.86108pt:\kern
0.86108pt}A+A^{\prime}\vdash[B,B^{\prime}][a^{\prime\prime}]$. Set
theoretically, $\sum_{a^{\prime\prime}{\kern 0.60275pt:\kern
0.60275pt}A+A^{\prime}}X^{[B,B^{\prime}][a^{\prime\prime}]}$ is the set of
pairs $\left\langle
a^{\prime\prime},[f,f^{\prime}]:[B,B^{\prime\prime}]\;a^{\prime\prime}\to
X\right\rangle$, where

  * •

either $a^{\prime\prime}=\iota_{1}[a]$, $\left\langle a,f:B[a]\to
X\right\rangle$ in $F\;X$, and $\forall x{\kern 0.86108pt:\kern
0.86108pt}B[a]\mathord{.\;}[f,f^{\prime}]\;x=f\;x$, or

  * •

$a^{\prime\prime}=\iota_{2}[a]^{\prime}$, $\left\langle
a^{\prime},f^{\prime}:B^{\prime}[a]^{\prime}\to X\right\rangle$ in
$F^{\prime}\;X$, and $\forall x^{\prime}{\kern 0.86108pt:\kern
0.86108pt}B[a^{\prime}]\mathord{.\;}[f,f^{\prime}]\;x^{\prime}=f^{\prime}\;x^{\prime}$.

In other words, the shape of the sum is the sum of the component shapes, and a
labelling function for the sum is the sum of two corresponding component
labelling functions.

#### Product

We have $(F+F^{\prime})\;X=\sum_{\left\langle a,a^{\prime}\right\rangle{\kern
0.60275pt:\kern 0.60275pt}A\times A^{\prime}}X^{\langlebar
B,B^{\prime}\ranglebar[\left\langle a,a^{\prime}\right\rangle]}$, where $F\;X$
and $F^{\prime}\;X$ are similar to those from the sum, and $\langlebar
B,B^{\prime}\ranglebar[\left\langle
a,a^{\prime}\right\rangle]=B[a]+B^{\prime}[a^{\prime}]$ (the positions of the
product is the disjoint union of the component positions).

######  Remark.

We prefer to write $\langlebar B,B^{\prime}\ranglebar[a,a^{\prime}]$ for
$\langlebar B,B^{\prime}\ranglebar[\left\langle a,a^{\prime}\right\rangle]$.
Set theoretically, $\sum_{\left\langle a.a^{\prime}\right\rangle{\kern
0.60275pt:\kern 0.60275pt}A\times A^{\prime}}X^{\langlebar
B,B^{\prime}\ranglebar[a,a^{\prime}]}$ is the set of pairs
$\left\langle\left\langle
a,a^{\prime}\right\rangle,[f,f^{\prime}]:B[a]+B^{\prime}[a^{\prime}]\to
X\right\rangle$, where $f:B[a]\to A$ and $f^{\prime}:B^{\prime}[a^{\prime}]\to
A^{\prime}$. In other words, the shape of the product is the product of the
component shapes and a labelling function for the product is the sum of two
corresponding component labelling functions.

#### Exponentiation

Assuming $F\;X=\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}X^{B[a]}$, the
(constant) exponent functor $(F\;X)^{C}$ is $\sum_{g:C\to A}X^{\sum_{c{\kern
0.43054pt:\kern 0.43054pt}C}B[g\;c]}$.

######  Remark.

An element of $\sum_{g:C\to A}X^{\sum_{c{\kern 0.43054pt:\kern
0.43054pt}C}B[g\;c]}$ is a pair $\left\langle g,f\right\rangle$ consisting of
a function $g:C\to A$ assigning shapes to $C$ and a $C$-indexed function
$c{\kern 0.86108pt:\kern 0.86108pt}C\vdash f_{c}:B[g\;c]\to X$ labelling the
positions $B[g\;c]$ for each $c$ in $C$.

##  3 Matching Logic (ML)

Matching logic [13, 9, 8] provides a unifying framework for defining semantics
of programming languages. A programming language is defined in matching logic
as a _logical theory_ , i.e., a set of axioms. The key concept in matching
logic is that of _patterns_ , which can be _matched_ by certain elements. By
building complex patterns, we can match elements that have complex structures
or certain properties, or both. The presentation of matching logic in this
review section follows [8].

######  Definition 3.1.

Let us fix two sets $\mathit{EV}$ and $\mathit{SV}$. The set $\mathit{EV}$
includes _element variables_ $x,y,\dots$. The set $\mathit{SV}$ includes _set
variables_ $X,Y,\dots$. A _matching logic signature_ $\Sigma$ is a set of
_(constant) symbols_ , denoted $\sigma,\sigma_{1},\sigma_{2},\dots$. Let us
fix a signature $\Sigma$. The set of _( $\Sigma$-)patterns_ is inductively
defined as follows:

$\displaystyle\varphi::=$ $\displaystyle\ x\mid X\mid\sigma\mid\varphi_{1}\
\varphi_{2}\mid\bot\mid\varphi_{1}\rightarrow\varphi_{2}\mid\exists
x\mathord{.\;}\varphi\mid\mu X\mathord{.\;}\varphi$

where in $\mu X\mathord{.\;}\varphi$, called a least-fixpoint pattern, we
require that $\varphi$ is positive in $X$, i.e., $X$ does not occur in an odd
number of times of the left-hand sides of implications
$\varphi_{1}\rightarrow\varphi_{2}$.

######  Definition 3.2.

A _(matching logic) $\Sigma$-model_ $M$ consists of

  1. 1.

a nonempty _carrier set_ , which we also denote $M$;

  2. 2.

an _application function_
$\\_{\mathbin{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\bullet$}}}}}}\\_\colon
M\times M\to\mathbb{P}(M)$, where $\mathbb{P}(M)$ is the powerset of $M$; and

  3. 3.

a _symbol interpretation_ $\sigma_{M}\subseteq M$ as a subset for
$\sigma\in\Sigma$.

######  Definition 3.3.

Given $M$ and a _variable valuation_
$\rho\colon(\mathit{EV}\cup\mathit{SV})\to M\cup\mathbb{P}(M)$ such that
$\rho(x)\in M$ for $x\in\mathit{EV}$ and $\rho(X)\subseteq M$ for
$X\in\mathit{SV}$, we inductively define _pattern valuation_
$\left|\varphi\right|_{M,\rho}$ as follows:

  1. 1.

$\left|x\right|_{M,\rho}=\\{\rho(x)\\}$ for $x\in\mathit{EV}$

  2. 2.

$\left|X\right|_{M,\rho}=\rho(X)$ for $X\in\mathit{SV}$

  3. 3.

$\left|\sigma\right|_{M,\rho}=\sigma_{M}$ for $\sigma\in\Sigma$

  4. 4.

$\left|\varphi_{1}\,\varphi_{2}\right|_{M,\rho}=\bigcup_{a_{i}\in\left|\varphi_{i}\right|_{M,\rho},i\in\\{1,2\\}}a_{1}\mathbin{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\bullet$}}}}}a_{2}$;
note that
$a_{1}\mathbin{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\bullet$}}}}}a_{2}$ is a
subset of $M$.

  5. 5.

$\left|\bot\right|_{M,\rho}=\emptyset$

  6. 6.

$\left|\varphi_{1}\rightarrow\varphi_{2}\right|_{M,\rho}=M\setminus(\left|\varphi_{1}\right|_{M,\rho}\setminus\left|\varphi_{2}\right|_{M,\rho})$

  7. 7.

$\left|\exists x\mathord{.\;}\varphi\right|_{M,\rho}=\bigcup_{a\in
M}\left|\varphi\right|_{M,\rho[a/x]}$

  8. 8.

$\left|\mu
X\mathord{.\;}\varphi\right|_{M,\rho}=\mathbf{lfp}(A\mapsto\left|\varphi\right|_{M,\rho[A/X]})$

where $\rho[a/x]$ (resp. $\rho[A/X]$) is the valuation $\rho^{\prime}$ with
$\rho^{\prime}(x)=a$ (resp. $\rho^{\prime}(X)=A$) and agreeing with $\rho$ on
all the other variables. in $\mathit{EV}\cup\mathit{SV}\setminus\\{x\\}$
(resp. $\mathit{EV}\cup\mathit{SV}\setminus\\{X\\}$). We use
$\mathbf{lfp}(A\mapsto\left|\varphi\right|_{M,\rho[A/X]})$ to denote the
smallest set $A$ such that $A=\left|\varphi\right|_{M,\rho[A/X]}$. The
existence of such an $A$ is guaranteed by the requirement that $\varphi$ is
positive in $X$. We abbreviate $\left|\varphi\right|_{M,\rho}$ as
$\left|\varphi\right|_{\rho}$ and further as $\left|\varphi\right|$ if
$\varphi$ is closed.

######  Definition 3.4.

We say that $\varphi$ _holds_ in $M$, written $M\vDash\varphi$, if
$\left|\varphi\right|_{M,\rho}=M$ for all $\rho$. For a pattern set $\Gamma$,
we write $M\vDash\Gamma$, if $M\vDash\psi$ for all $\psi\in\Gamma$. We write
$\Gamma\vDash\varphi$, if $M\vDash\Gamma$ implies $M\vDash\varphi$ for all
$M$.

The following common constructs can be defined from the basic pattern syntax
as syntactic sugar in the usual way:

$\displaystyle\neg\varphi$ $\displaystyle\equiv\varphi\rightarrow\bot\qquad$
$\displaystyle\varphi_{1}\vee\varphi_{2}$
$\displaystyle\equiv\neg\varphi_{1}\rightarrow\varphi_{2}\qquad$
$\displaystyle\varphi_{1}\wedge\varphi_{2}$
$\displaystyle\equiv\neg(\neg\varphi_{1}\vee\neg\varphi_{2})$
$\displaystyle\top$ $\displaystyle\equiv\neg\bot$ $\displaystyle\forall
x\mathord{.\;}\varphi$ $\displaystyle\equiv\neg\exists
x\mathord{.\;}\neg\varphi$ $\displaystyle\nu X\mathord{.\;}\varphi$
$\displaystyle\equiv\neg\mu X\mathord{.\;}\neg\varphi[\neg X/X]$

We assume the standard precedence between the above constructs.

#### Equality

The equality can be defined as a derived construct (see [13, 8]). Two patterns
$\varphi_{1}$ and $\varphi_{2}$ are equal, written $\varphi_{1}=\varphi_{2}$,
iff it is equivalent to $\top$ if the two patterns are matched by the same
elements. Otherwise, it is equivalent to $\bot$. To express that in ML, a new
symbol $\mathit{def}\in\Sigma$ is introduced, called the _definedness_ symbol,
and specify it with the axiom  (Definedness) . The resulted theory can be
described as follows:

⬇

spec $\mathsf{EQUALITY}$

Symbols: $\mathsf{def}$

Notations: $\lceil\varphi\rceil\equiv\mathsf{def}\ \varphi$

Axioms: $\scalebox{0.95}[1.0]{{{(Definedness)}}}\quad\forall
x\mathord{.\;}\lceil x\rceil$

Notations:

$\left\lfloor\varphi\right\rfloor\equiv\neg\lceil\neg\varphi\rceil\par$ //
totality

$\varphi_{1}=\varphi_{2}\equiv\left\lfloor\varphi_{1}\leftrightarrow\varphi_{2}\right\rfloor\par$
// equality

$\varphi_{1}\subseteq\varphi_{2}\equiv\left\lfloor\varphi_{1}\rightarrow\varphi_{2}\right\rfloor\par$
// set inclusion

$x\in\varphi\equiv x\subseteq\varphi\par$ // membership

endspec

#### Sorts

Matching logic has no builtin support for sorts. Instead, we define a _theory
of sorts_ to support arbitrary sort structures following the “sort-as-
predicate” paradigm. A _sort_ has a name and is associated with a set of its
_inhabitants_. In matching logic, we use a symbol $s\in\Sigma$ to represent
the sort name and use $(\mathsf{inh}\ s)$ to represent all its inhabitants,
where $\mathsf{inh}\in\Sigma$ is an ordinary symbol. For better readability,
we define the notation $\top_{\\!\\!s}\equiv\mathsf{inh}\ s$.

⬇

spec $\mathsf{SORT}$ Imports: $\mathsf{EQUALITY}$

Symbols: $\mathit{inh},\mathit{Sort}$

Notations:

$\top_{\\!\\!s}\equiv\mathit{inh}\ s\par$ // inhabitants of sort $s$

$s_{1}\leq s_{2}\equiv\top_{\\!\\!s_{1}}\subseteq\top_{\\!\\!s_{2}}\par$ //
subsort relation

$\neg_{s}\varphi\equiv(\neg\varphi)\wedge\top_{\\!\\!s}\par$ // negation
within sort $s$

$\forall x{\kern 0.77498pt:\kern 0.77498pt}s\mathord{.\;}\varphi\equiv\forall
x\mathord{.\;}x\in\top_{\\!\\!s}\rightarrow\varphi\par$ // $\forall$ within
sort $s$

$\exists x{\kern 0.77498pt:\kern 0.77498pt}s\mathord{.\;}\varphi\equiv\exists
x\mathord{.\;}x\in\top_{\\!\\!s}\land\varphi\par$ // $\exists$ within sort $s$

$\mu X{\kern 0.77498pt:\kern 0.77498pt}s\mathord{.\;}\varphi\equiv\mu
X\mathord{.\;}X\subseteq\top_{\\!\\!s}\land\varphi\par$ // $\mu$ within sort
$s$

$\nu X{\kern 0.77498pt:\kern 0.77498pt}s\mathord{.\;}\varphi\equiv\nu
X\mathord{.\;}X\subseteq\top_{\\!\\!s}\land\varphi\par$ // $\nu$ within sort
$s$

$\varphi{\kern 0.77498pt:\kern 0.77498pt}s\equiv\exists z{\kern
0.77498pt:\kern 0.77498pt}s\mathord{.\;}\varphi=z\par$ // “typing”

$f{\kern 0.77498pt:\kern 0.77498pt}s_{1}\otimes\cdots\otimes s_{n}\to
s\equiv\forall x_{1}{\kern 0.77498pt:\kern 0.77498pt}s_{1}\ldots\forall
x_{n}{\kern 0.77498pt:\kern 0.77498pt}s_{n}\mathord{.\;}\exists y{\kern
0.77498pt:\kern 0.77498pt}s\mathord{.\;}f\,x_{1}\ldots x_{n}=y$

// functional

$f{\kern 0.77498pt:\kern 0.77498pt}s_{1}\otimes\cdots\otimes
s_{n}\rightharpoonup s\equiv\forall x_{1}{\kern 0.77498pt:\kern
0.77498pt}s_{1}\ldots\forall x_{n}{\kern 0.77498pt:\kern
0.77498pt}s_{n}\mathord{.\;}\exists y{\kern 0.77498pt:\kern
0.77498pt}s\mathord{.\;}f\,x_{1}\ldots x_{n}\rightarrow y$

// partially functional

Axioms:

$\exists x\mathord{.\;}\mathit{Sort}=x$

$\mathit{Sort}\in\top_{\\!\\!\mathit{Sort}}$

endspec

The ML specifications for the sum, product, and function sorts are given in
[8]. For reader convenience, we recall them in Appendix A.

##  4 Specifying Initial Algebra and Final Coalgebra for Container Functors in
ML

In this section we show how to specify a unary container functor in ML and how
to extract the structures for their initial algebra and the final coalgebra.

###  4.1 Capturing Elements from the Category $\mathbb{C}$

  * •

$\mathbf{0}$ is specified by $\bot$;

  * •

$\mathbf{1}=\\{\star\\}$ is specified by

    * –

a symbol $\mathit{star}\in\Sigma$;

    * –

a notation: $\star\equiv\mathit{star}$; and

    * –

an axiom
$~{}~{}~{}~{}\begin{aligned} &\exists
y\mathord{.\;}\star=y&&\textnormal{({singleton})}\\\ \end{aligned}$

  * •

$\mathbf{0}\xrightarrow{\raisebox{2.0pt}{\hbox{!`}}}X$ is specified by

    * –

a symbol $\mathit{iniMor}\in\Sigma$;

    * –

a notation: $\raisebox{2.0pt}{\hbox{!`}}\equiv\mathit{iniMor}$; and

    * –

an axiom
$~{}~{}~{}~{}\begin{aligned} &\forall
x\mathord{.\;}\raisebox{2.0pt}{\hbox{!`}}\;x=\bot&&\textnormal{({{captures~{}}$\mathbf{0}\xrightarrow{\raisebox{2.0pt}{\hbox{!`}}}X$})}\\\
\end{aligned}$

  * •

$\mathbf{1}\xleftarrow{\hbox{!}}X$ is specified by

    * –

a symbol $\mathit{finMor}\in\Sigma$;

    * –

a notation: $\hbox{!}\equiv\mathit{finMor}$; and

    * –

an axiom
$~{}~{}~{}~{}\begin{aligned} &\forall
x\mathord{.\;}\hbox{!}\;x=\star&&\textnormal{({{captures~{}}$\mathbf{1}\xleftarrow{\hbox{!}}X$})}\\\
\end{aligned}$

######  Remark.

An alternative way to specify $\mathbf{1}$ is by $\top$, in which case
$\mathbf{1}\xleftarrow{\hbox{!}}X$ is the inclusion: $\forall
x\mathord{.\;}x\in X\rightarrow\hbox{!}\;x=x$. This version is used when we
compute the greatest fixpoint.

###  4.2 Expressing Indexed Families in ML

An $A$-indexed family $a{\kern 0.86108pt:\kern 0.86108pt}A\vdash B[a]$ is
specified by a constant symbol $\mathit{depOf}\in\Sigma$, a notation
$B[a]\equiv\mathit{depOf}\;B\;a$, and two axioms:

  * •

$A$ is a sort: $A{\kern 0.86108pt:\kern 0.86108pt}\mathit{Sort}$ (equivalent
to $A\in\top_{\\!\\!\mathit{Sort}}$), and

  * •

for each $a{\kern 0.86108pt:\kern 0.86108pt}A$, $B[a]$ is a sort: $\forall
a{\kern 0.86108pt:\kern 0.86108pt}A\mathord{.\;}B[a]{\kern 0.86108pt:\kern
0.86108pt}\mathit{Sort}$

where we assumed that $A$ and $B$ are specified as functional patterns.

###  4.3 Expressing Dependent Products/Sums in ML

A dependent product $\prod_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]$ is
specified by a constant symbol $\mathit{DepProd}\in\Sigma$, a notation
$\prod_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]\equiv\mathit{DepProd}\;A\;B$
($a$ plays a local role and its name can be changed111Actually, $\Pi$ should
be captured as a binder [10], but this is not needed for the purpose of this
paper.), and by adding the axioms:

  * •

$\prod_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]$ is a sort: $\prod_{a{\kern
0.60275pt:\kern 0.60275pt}A}B[a]{\kern 0.86108pt:\kern
0.86108pt}\mathit{Sort}$

  * •

$\top_{\\!\\!\prod_{a{\kern 0.43054pt:\kern 0.43054pt}A}B[a]}$ is the set of
dependent functions:

$\top_{\\!\\!\prod_{a{\kern 0.43054pt:\kern 0.43054pt}A}B[a]}=\exists
f\mathord{.\;}f\land((\lceil\top_{\\!\\!A}\rceil\land\forall a{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\exists b{\kern 0.86108pt:\kern
0.86108pt}B[a]\mathord{.\;}f\;a=b)\lor(\neg\lceil\top_{\\!\\!A}\rceil\land
f=\raisebox{2.0pt}{\hbox{!`}}))$

The above axiom distinguishes between two cases: the sort $A$ is non-empty, in
which case $\top_{\\!\\!\prod_{a{\kern 0.43054pt:\kern 0.43054pt}A}B[a]}$
includes the dependent functions that maps an $a{\kern 0.86108pt:\kern
0.86108pt}A$ into a $b{\kern 0.86108pt:\kern 0.86108pt}B[a]$, and when the
sort $A$ is empty, in which case $\top_{\\!\\!\prod_{a{\kern 0.43054pt:\kern
0.43054pt}A}B[a]}$ consists of the function given by the initial morphism.

Similarly, a dependent sum $\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]$ is
specified by a constant $\mathit{DepSum}\in\Sigma$, a notation $\sum_{a{\kern
0.60275pt:\kern 0.60275pt}A}B[a]\equiv\mathit{DepSum}\;A\;B$ (again, $a$ plays
a local role and its name can be changed), and by adding the axioms:

  * •

$\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}B[a]$ is a sort: $\sum_{a{\kern
0.60275pt:\kern 0.60275pt}A}B[a]{\kern 0.86108pt:\kern
0.86108pt}\mathit{Sort}$

  * •

$\top_{\\!\\!\sum_{a{\kern 0.43054pt:\kern 0.43054pt}A}B[a]}$ is the set fo
dependent pairs:

$\top_{\\!\\!\sum_{a{\kern 0.43054pt:\kern 0.43054pt}A}B[a]}=\exists a{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\exists b{\kern 0.86108pt:\kern
0.86108pt}B[a]\mathord{.\;}\left\langle a,b\right\rangle$

###  4.4 Expressing Unary Container Functors in ML

Let $X\mapsto F\;X=\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}X^{B[a]}$ be a
container functor. Recall that $F\;X$ is the set of pairs $\left\langle
a,f\right\rangle$ with $a{\kern 0.86108pt:\kern 0.86108pt}A$ and $f{\kern
0.86108pt:\kern 0.86108pt}X^{B[a]}$ (or, equivalently, $f{\kern
0.86108pt:\kern 0.86108pt}B[a]\to X$). If $X$ is specified as the set of
inhabitants $\top_{\\!\\!s}$ of a sort $s{\kern 0.86108pt:\kern
0.86108pt}\mathit{Sort}$ and $\top_{\\!\\!B[a]}\not=\bot$ (that is equivalent
to $B[a]\not\approxeq\mathbf{0}$ in $\mathbb{C}$), then $X^{B[a]}$ is
specified by the sort $B[a]\mathbin{\textnormal{\small$\to$⃝}}s$ [8] (see also
Appendix A.2) and the specification of $\sum_{a{\kern 0.60275pt:\kern
0.60275pt}A}X^{B[a]}$ is a particular case of dependent sum specification.
Otherwise, we have to explicitly specify $X^{B[a]}$ by the notation

$X^{B[a]}\equiv\exists
f\mathord{.\;}f\land(((\top_{\\!\\!B[a]}\not=\bot)\land\forall b{\kern
0.86108pt:\kern 0.86108pt}B[a]\mathord{.\;}\exists x\mathord{.\;}f\;b=x\land
x\in X)\lor((\top_{\\!\\!B[a]}=\bot)\land f=\raisebox{2.0pt}{\hbox{!`}}))$

and use it directly in the specification of $\sum_{a{\kern 0.60275pt:\kern
0.60275pt}A}X^{B[a]}$:

$\exists a{\kern 0.86108pt:\kern 0.86108pt}A\mathord{.\;}\exists
f\mathord{.\;}\left\langle a,f\right\rangle\land f\in X^{B[a]}$

which is equivalent to

$\exists a{\kern 0.86108pt:\kern 0.86108pt}A\mathord{.\;}\exists
f\mathord{.\;}\left\langle
a,f\right\rangle\land(((\top_{\\!\\!B[a]}\not=\bot)\land\forall b{\kern
0.86108pt:\kern 0.86108pt}B[a]\mathord{.\;}\exists x\mathord{.\;}f\;b=x\land
x\in X)\lor((\top_{\\!\\!B[a]}=\bot)\land f=\raisebox{2.0pt}{\hbox{!`}}))$

Recall that if $\top_{\\!\\!B[a]}=\bot$ ($B[a]\approxeq\mathbf{0}$) then there
is just one function $\mathbf{0}\xrightarrow{\raisebox{2.0pt}{\hbox{!`}}}X$
specified by $\raisebox{2.0pt}{\hbox{!`}}\equiv\mathit{iniMor}$.

###  4.5 Specifying Initial Algebra

Let $X\mapsto F\;X=\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}X^{B[a]}$ be a
container functor. The initial $F$-algebra is specified by using the
characterization given by the ”no junk and no confusion” properties for the
constructors [8]:

  * •

a constructor $\mathit{cons}\in\Sigma$ specified by the following axioms:
$\begin{aligned} &\forall a{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\forall f\mathord{.\;}f\in X^{B[a]}\rightarrow\exists
x\mathord{.\;}x\in X\land\mathit{cons}\;\left\langle
a,f\right\rangle=x&&\textnormal{({Functional})}\\\ &\forall a,a^{\prime}{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\forall
f,f^{\prime}\mathord{.\;}\mathit{cons}\;\left\langle
a,f\right\rangle=\mathit{cons}\;\left\langle
a^{\prime},f^{\prime}\right\rangle\rightarrow a=a^{\prime}\land
f=f^{\prime}&&\textnormal{({No Confusion})}\end{aligned}$

  * •

a sort $\mu F$ with initial semantics:
$\begin{aligned} \top_{\\!\\!\mu F}=\mu X\mathord{.\;}\exists a{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle
a,X^{B[a]}\right\rangle&&\textnormal{({No Junk})}\end{aligned}$

##### Computing the least fixpoint

Let $\varphi_{F}(X)$ denote the pattern $\exists a{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle a,X^{B[a]}\right\rangle$.
Given a model $M$ and a valuation $\rho$, we have $\left|\mu
X\mathord{.\;}\varphi_{F}(X)\right|_{M,\rho}=\mathbf{lfp}(A\mapsto\left|\varphi_{F}(X)\right|_{M,\rho[A/X]})$.
We also denote by $A\mapsto\phi_{F}(A)$ the function A
$\mapsto\left|\varphi_{F}(X)\right|_{M,\rho[A/X]}$. If $\phi_{F}$ is
continuous, then $\mathbf{lfp}(\phi_{F})=\bigcup_{n\geq
0}\phi^{n}_{F}(\emptyset)=\emptyset\cup\phi_{F}(\emptyset)\cup\phi^{2}_{F}(\emptyset)\cup\cdots$.
Since $\phi_{F}(\emptyset)=\left|\varphi_{F}(\bot)\right|_{M,\rho})$ and
writing $\varphi(\psi)$ for $\varpi[\psi/X]$, we (informally) obtain that
$\mathbf{lfp}(\phi_{F})$ is the interpretation of the infinite disjunction

$\bot\lor\varphi_{F}(\bot)\lor\varphi^{2}_{F}(\bot)\lor\varphi^{3}_{F}(\bot)\lor\cdots$

according to $M$ and $\rho$. We have
$\varphi^{n}_{F}(\bot)\rightarrow\varphi^{n+1}_{F}(\bot)$ and each
$\varphi^{n}_{F}(\bot)$ gives an approximation of $\top_{\\!\\!\mu
F}\approxeq\mathbf{lfp}(\phi_{F})$. So, in order to understand how the
elements of the initial algebra look like, we have to investigate these ML
patterns.

$\varphi_{F}(\bot)$.

We have $X^{B[a]}=\bot^{B[a]}\not=\bot$ iff $\top_{\\!\\!B[a]}=\bot$, because
otherwise we have $(\forall b{\kern 0.86108pt:\kern
0.86108pt}B[a]\mathord{.\;}\exists y\mathord{.\;}f\;b=y\land y\in\bot)=\bot$.
It follows that $\bot^{B[a]}$ consists of the unique function ¡. We obtain

$\varphi_{F}(\bot)=\exists a_{1}{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\mathit{cons}\left\langle
a_{1},\raisebox{2.0pt}{\hbox{!`}}\right\rangle\land(\top_{\\!\\!{B[a_{1}]}}=\bot)$

i.e., each $a_{1}{\kern 0.86108pt:\kern 0.86108pt}A$, with its corresponding
dependent sort $B[a_{1}]$ empty, defines a constant constructor.
If $\forall a{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\top_{\\!\\!B[a]}\not=\bot$ then $(\exists a{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle
a,\top_{\\!\\!B[a]\mathbin{\textnormal{\small$\to$⃝}}\mathbb{n}\;{X}}\right\rangle)=\bot$
and hence $\top_{\\!\\!\mu L}=\bot$.

$\varphi^{2}_{F}(\bot)=\exists a_{2}{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle
a_{2},\varphi_{F}(\bot)^{B[a_{2}]}\right\rangle$.

If $\top_{\\!\\!B[a_{2}]}=\bot$ then $\varphi_{F}(\bot)^{B[a_{2}]}$ consists
of the constant constructor $\mathit{cons}\;\left\langle
a_{2},\raisebox{2.0pt}{\hbox{!`}}\right\rangle$, i.e.,
$\varphi_{F}(\bot)^{B[a_{2}]}=\bot^{B[a_{2}]}$. If
$\top_{\\!\\!B[a_{2}]}\not=\bot$ then we have

$\varphi_{F}(\bot)^{B[a_{2}]}=\exists f\mathord{.\;}f\land\forall b{\kern
0.86108pt:\kern 0.86108pt}B[a_{2}]\mathord{.\;}\exists a_{1}{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}f\;b=\mathit{cons}\left\langle
a_{1},\raisebox{2.0pt}{\hbox{!`}}\right\rangle\land(\top_{\\!\\!{B[a_{1}]}}=\bot)$

We obtain

$\varphi^{2}_{F}(\bot)=\varphi_{F}(\bot)\lor\exists a_{2}{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle
a_{2},\varphi_{F}(\bot)^{B[a_{2}]}\right\rangle\land(\top_{\\!\\!B[a_{2}]}\not=\bot)$

…

######  Remark.

The ML pattern (4.5) can be seen as an informal translation in ML of the
colimit (1).

##### Deriving Induction Principle

Once we have seen how the least fixpoint is computed, we may derive the
following _Induction Principle_ :

$\dfrac{\forall a{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle
a,\psi\right\rangle\rightarrow\psi}{\top_{\\!\\!\mu F}\rightarrow\psi}$

The justification for this principle is similar to that for lists given in
[8].

###  4.6 Specifying Final Coalgebra

Let $X\mapsto F\;X=\sum_{a{\kern 0.60275pt:\kern 0.60275pt}A}X^{B[a]}$ be a
container functor. The final $F$-coalgebra is specified by:

  * •

the constructor $\mathit{cons}$ together with its axioms;

  * •

a sort $\nu F$ with final semantics:
$~{}~{}~{}~{}\begin{aligned} \top_{\\!\\!\nu F}=\nu X\mathord{.\;}\exists
a{\kern 0.86108pt:\kern 0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle
a,X^{B[a]}\right\rangle&&\textnormal{({No Redundancy (Cojunk)})}\end{aligned}$

  * •

two destructors $\mathit{out},\mathit{nxt}\in\Sigma$ together with the
notations:
$~{}~{}~{}~{}\begin{aligned} &x.\mathit{out}\equiv\mathit{out}\;x\\\
&x.\mathit{nxt}\equiv\mathit{nxt}\;x\end{aligned}$
and the axioms:
$~{}~{}~{}~{}\begin{aligned} &\forall a{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\forall f\mathord{.\;}(\mathit{cons}\;\left\langle
a,f\right\rangle).\mathit{out}=a&&\textnormal{({No Ambiguity
(Coconfusion).1)})}\\\ &\forall a{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\forall f\mathord{.\;}(\mathit{cons}\;\left\langle
a,f\right\rangle).\mathit{nxt}=f&&\textnormal{({No Ambiguity
(Coconfusion).2)})}\\\ &\forall x{\kern 0.86108pt:\kern 0.86108pt}\nu
F\mathord{.\;}(\mathit{cons}\;\left\langle
x.\mathit{out},x.\mathit{nxt}\right\rangle)=x&&\textnormal{({No Ambiguity
(Coconfusion).3)})}\end{aligned}$

##### Computing the greatest fixpoint

Since $\mathbf{gfp}(\phi_{F})=\bigcap_{n\geq
0}\phi^{n}_{F}(M)=M\cap\phi_{F}(M)\cap\phi^{2}_{F}(M)\cap\cdots$, we have to
investigate the infinite conjunction

$\top\land\varphi_{F}(\top)\land\varphi^{2}_{F}(\top)\land\varphi^{3}_{F}(\top)\land\cdots$

in order to understand how the elements of the final coalgebra look like.

$\varphi_{F}(\top)$.

We have $\mathit{cons}\;\left\langle a,\top^{B[a]}\right\rangle=\exists
x,y\mathord{.\;}x\land x.\mathit{out}=a\land x.\mathit{nxt}=y$.

$\varphi_{F}^{2}(\top)$.

We have

$\displaystyle\varphi_{F}^{2}(\top)$ $\displaystyle=\exists a{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\mathit{cons}\;\left\langle
a,\varphi_{F}(\top)^{B[a]}\right\rangle$ $\displaystyle=(\exists a{\kern
0.86108pt:\kern 0.86108pt}A\mathord{.\;}\exists x\mathord{.\;}\exists y{\kern
0.86108pt:\kern 0.86108pt}\mathbb{n}\;{F\;\top}\mathord{.\;}x\land
x.\mathit{out}=a\land x.\mathit{nxt}=y)$ $\displaystyle=(\exists
a,a^{\prime}{\kern 0.86108pt:\kern 0.86108pt}A\mathord{.\;}\exists
x,z\mathord{.\;}\exists y{\kern 0.86108pt:\kern
0.86108pt}\mathbb{n}\;{F\;\top}\mathord{.\;}x\land x.\mathit{out}=a\land
x.\mathit{nxt}=y\land y.\mathit{out}=a^{\prime}\land y.\mathit{nxt}=z)$

…

######  Remark.

The ML pattern (4.6) can be seen as an ML informal translation of the colimit
(1).

##### Deriving Coinduction Principle

Once we have seen how the greatest fixpoint is computed, we may derive the
following _Conduction Principle_ :

$\dfrac{\forall a{\kern 0.86108pt:\kern
0.86108pt}A\mathord{.\;}\psi\rightarrow\mathit{cons}\;\left\langle
a,\psi\right\rangle}{\top_{\\!\\!\psi\rightarrow\nu F}}$

The justification for this principle is similar to that for streams given in
[8].

##  5 Case Study: Lists Using Container Functors

First, we express $L\;X=\mathbf{1}+E\times X$ as a unary container functor,
using $\mathbf{1}\approxeq\sum_{\star{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}}X^{\mathbf{0}[\star]}$, $E\approxeq\sum_{e{\kern
0.60275pt:\kern 0.60275pt}E}X^{\mathbf{0}[e]}$, and
$X\approxeq\sum_{\star{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}}X^{\mathbf{1}[\star]}$:

$\displaystyle L\;X$ $\displaystyle=\sum_{\star{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}}X^{\mathbf{0}[\star]}+\sum_{e{\kern 0.60275pt:\kern
0.60275pt}E}X^{\mathbf{0}[e]}\times\sum_{\star{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}}X^{\mathbf{1}[\star]}$ $\displaystyle=\sum_{\star{\kern
0.60275pt:\kern 0.60275pt}\mathbf{1}}X^{\mathbf{0}[\star]}+\sum_{\left\langle
e,\star\right\rangle{\kern 0.60275pt:\kern
0.60275pt}E\times\mathbf{1}}X^{\mathbf{0}[e]+\mathbf{1}[\star]}$
$\displaystyle=\sum_{a{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}+E\times\mathbf{1}}X^{[\mathbf{0},\langlebar\mathbf{0},\mathbf{1}\ranglebar][a]}$

Using the isomorphisms $E\times\mathbf{1}\approxeq E$ and
$\langlebar\mathbf{0},\mathbf{1}\ranglebar[\left\langle
e,\star\right\rangle]=\mathbf{0}[e]+\mathbf{1}[\star]=\mathbf{0}+\mathbf{1}\approxeq\mathbf{1}$
in the category $\mathbb{C}$, we obtain the reduced form
$L^{c}\;X=\sum_{a{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}+E}X^{[\mathbf{0},\mathbf{1}][a]}$ of the container
functor $L$. From the definition of the sum of container functors we deduce
that the elements of $\sum_{a{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}+E}X^{[\mathbf{0},\mathbf{1}][a]}$ are pairs
$\\{\left\langle\star,f\right\rangle\mid f:\mathbf{0}\to
X\\}\uplus\\{\left\langle e,f^{\prime}\right\rangle\mid
e:E,f^{\prime}:\mathbf{1}\to X\\}$. The only function $\mathbf{0}\to X$ is ¡,
and $f^{\prime}:\mathbf{1}\to X\approxeq f^{\prime}\in X$.

The specification in ML of the initial algebra $\mu L^{c}$ includes:

  * •

a constructor symbol $\mathit{cons}$ and a sort symbol $\mu F$;

  * •

the axioms:
$~{}~{}~{}~{}\begin{aligned} &\exists y{\kern 0.86108pt:\kern 0.86108pt}\mu
L^{c}\mathord{.\;}\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle=y&&\textnormal{({Functional.1})}\\\
&\forall e{\kern 0.86108pt:\kern 0.86108pt}E\mathord{.\;}\forall
f^{\prime}{\kern 0.86108pt:\kern 0.86108pt}\mu L^{c}\mathord{.\;}\exists
y{\kern 0.86108pt:\kern 0.86108pt}\mu
L^{c}\mathord{.\;}\mathit{cons}\;\left\langle
e,f^{\prime}\right\rangle=y&&\textnormal{({Functional.2})}\\\ &\forall e{\kern
0.86108pt:\kern 0.86108pt}E\mathord{.\;}\forall f^{\prime}{\kern
0.86108pt:\kern 0.86108pt}\mu
L^{c}\mathord{.\;}\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle\not=\mathit{cons}\;\left\langle
e,f^{\prime}\right\rangle&&\textnormal{({No Confusion.1})}\\\ &\forall
e,e^{\prime}{\kern 0.86108pt:\kern 0.86108pt}E\mathord{.\;}\forall
f,f^{\prime}{\kern 0.86108pt:\kern 0.86108pt}\mu
L\mathord{.\;}\mathit{cons}\;\left\langle
e,f\right\rangle=\mathit{cons}\;\left\langle
e,f^{\prime}\right\rangle\rightarrow e=e^{\prime}\land
f=f^{\prime}&&\textnormal{({No Confusion.2})}\\\ &\top_{\\!\\!\mu L^{c}}=\mu
X\mathord{.\;}(\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle\lor\mathit{cons}\;\left\langle
E,X\right\rangle)&&\textnormal{({No Junk})}\end{aligned}$

Comparing with the specification from [8], we obviously have the equivalences
$\mathit{nil}\approxeq\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle$
and $\mathit{cons}\;e\;\ell\approxeq\mathit{cons}\;\left\langle
e,\ell\right\rangle$.

The ML specification of the final coalgebra further includes:

  * •

the destructor symbols $\mathit{out},\mathit{nxt}\in\Sigma$;

  * •

the axioms
$~{}~{}~{}~{}\begin{aligned}
&\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle\mathord{.\;}\mathit{out}=\star&&\textnormal{({No
Coconfusion.1.1)})}\\\ &\forall e{\kern 0.86108pt:\kern
0.86108pt}E\mathord{.\;}\forall f{\kern 0.86108pt:\kern 0.86108pt}\nu
L^{c}\mathord{.\;}\mathit{cons}\;\left\langle
e,f\right\rangle\mathord{.\;}\mathit{out}=e&&\textnormal{({No
Coconfusion.1.2)})}\\\
&\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle\mathord{.\;}\mathit{nxt}=\raisebox{2.0pt}{\hbox{!`}}&&\textnormal{({No
Coconfusion.2.1)})}\\\ &\forall e{\kern 0.86108pt:\kern
0.86108pt}E\mathord{.\;}\forall f{\kern 0.86108pt:\kern 0.86108pt}\nu
L^{c}\mathord{.\;}\mathit{cons}\;\left\langle
e,f\right\rangle\mathord{.\;}\mathit{nxt}=f&&\textnormal{({No
Coconfusion.2.2)})}\\\ &\forall x{\kern 0.86108pt:\kern 0.86108pt}\nu
L^{c}\mathord{.\;}(\mathit{cons}\;\left\langle
x.\mathit{out},x.\mathit{nxt}\right\rangle)=x&&\textnormal{({No
Coconfusion.3)})}\\\ &\top_{\\!\\!\nu L^{c}}=\nu
X\mathord{.\;}(\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle\lor\mathit{cons}\;\left\langle
E,X\right\rangle)&&\textnormal{({No Cojunk})}\end{aligned}$

Comparing with the specification of streams (inifinite lists) from [8], we
obviously have the equivalences
$\ell\mathord{.\;}\mathit{out}\approxeq\mathit{hd}\;\ell$ and
$\ell\mathord{.\;}\mathit{nxt}\approxeq\mathit{tl}\;\ell$. Using
$\mathit{nil}\approxeq\mathit{cons}\;\left\langle\star,\raisebox{2.0pt}{\hbox{!`}}\right\rangle$,
we get $\mathit{hd}\;\mathit{nil}=\star$ and
$\mathit{tl}\;\mathit{nil}=\raisebox{2.0pt}{\hbox{!`}}$, which is different
from the usual approach, where $\mathit{hd}$ and $\mathit{tl}$ are partial
operations.

##  6 Case Study: Moore Machines

Here we consider an example of (constant) exponential functor, whose ML
specification is more tricky. Moore machines (automata) have the signature
given by the functor $M\;X=O\times X^{I}$, where $O$ is for outputs and $I$
for inputs.

#### Capturing Final M-Coalgebra in ML Using Container Functors

We first express $M$ as a unary container functor:

$\displaystyle M\;X$ $\displaystyle=O\times X^{I}$
$\displaystyle\approxeq\sum_{o{\kern 0.60275pt:\kern
0.60275pt}O}X^{\mathbf{0}}\times(\sum_{\star{\kern 0.60275pt:\kern
0.60275pt}\mathbf{1}}X^{\mathbf{1}})^{\sum_{i{\kern 0.43054pt:\kern
0.43054pt}I}X^{\mathbf{0}}}$ $\displaystyle=\sum_{o{\kern 0.60275pt:\kern
0.60275pt}O}X^{\mathbf{0}}\times\sum_{g{\kern 0.60275pt:\kern
0.60275pt}I\to\mathbf{1}}X^{\sum_{i{\kern 0.43054pt:\kern
0.43054pt}I}\mathbf{1}[g\;i]}$ $\displaystyle=\sum_{\left\langle
o,g\right\rangle{\kern 0.60275pt:\kern
0.60275pt}(O\times(I\to\mathbf{1}))}X^{\mathbf{0}[o]+\sum_{i{\kern
0.43054pt:\kern 0.43054pt}I}\mathbf{1}[g\;i]}$
$\displaystyle\approxeq\sum_{o{\kern 0.60275pt:\kern
0.60275pt}O}X^{\sum_{i{\kern 0.43054pt:\kern 0.43054pt}I}\mathbf{1}}$
$\displaystyle\approxeq\sum_{o{\kern 0.60275pt:\kern 0.60275pt}O}X^{I}$
$\displaystyle=M^{c}\;X$

The instantiation of the ML specification for the final coalgebra is as
follows:

  * •

the constructor $\mathit{cons}\in\Sigma$ is specified by the following axioms:
$\begin{aligned} &\forall o{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}\forall f\mathord{.\;}f\in X^{I}\rightarrow\exists
x\mathord{.\;}x\in X\land\mathit{cons}\;\left\langle
a,f\right\rangle=x&&\textnormal{({Functional})}\\\ &\forall o,o^{\prime}{\kern
0.86108pt:\kern 0.86108pt}O\mathord{.\;}\forall
f,f^{\prime}\mathord{.\;}\mathit{cons}\;\left\langle
a,f\right\rangle=\mathit{cons}\;\left\langle
a^{\prime},f^{\prime}\right\rangle\rightarrow a=a^{\prime}\land
f=f^{\prime}&&\textnormal{({No Confusion})}\end{aligned}$

  * •

the destructors $\mathit{out},\mathit{nxt}\in\Sigma$ are specified by the
axioms:
$~{}~{}~{}~{}\begin{aligned} &\forall o{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}\forall f\mathord{.\;}f\in
X^{I}\rightarrow(\mathit{cons}\;\left\langle
a,f\right\rangle).\mathit{out}=a&&\textnormal{({No Coconfusion.1)})}\\\
&\forall a{\kern 0.86108pt:\kern 0.86108pt}A\mathord{.\;}\forall
f\mathord{.\;}f\mathord{.\;}f\in X^{I}\rightarrow(\mathit{cons}\;\left\langle
a,f\right\rangle).\mathit{nxt}=f&&\textnormal{({No Coconfusion.2)})}\\\
&\forall x{\kern 0.86108pt:\kern 0.86108pt}\nu
F\mathord{.\;}(\mathit{cons}\;\left\langle
x.\mathit{out},x.\mathit{nxt}\right\rangle)=x&&\textnormal{({No
Coconfusion.3)})}\end{aligned}$

  * •

the sort $\nu M^{c}$ with final semantics:
$~{}~{}~{}~{}\begin{aligned} \top_{\\!\\!\nu M^{c}}=\nu X\mathord{.\;}\exists
o{\kern 0.86108pt:\kern 0.86108pt}O\mathord{.\;}\mathit{cons}\;\left\langle
o,X^{I}\right\rangle&&\textnormal{({No Cojunk})}\end{aligned}$

We should have

$\top_{\\!\\!\nu M^{c}}\approxeq\nu X\mathord{.\;}M^{C}\;X$

Computing
$\top\land\varphi_{M}(\top)\land\varphi^{2}_{M}(\top)\land\varphi^{3}_{M}(\top)\land\cdots$,
where $\varphi_{M}(X)\equiv\exists o{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}\mathit{cons}\;\left\langle o,X^{I}\right\rangle$:

$\varphi_{M}(\top)={}$

$\exists o_{0}{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}\mathit{cons}\;\left\langle
o,X^{I}\right\rangle=\exists o_{0}{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}\exists f_{0}\mathord{.\;}\mathit{cons}\;\left\langle
o_{0},f_{0}\right\rangle\land(\forall i{\kern 0.86108pt:\kern
0.86108pt}I\mathord{.\;}\exists x_{1}\mathord{.\;}f_{0}\;i=x_{1})$. When
describing a dynamic system, the use of destructors is more intuitive:

$\varphi_{M}(\top)=\exists x_{0}\mathord{.\;}\exists o_{0}{\kern
0.86108pt:\kern
0.86108pt}O\mathord{.\;}x_{0}\land(x_{0}.\mathit{out}=o_{0}\land\forall
i{\kern 0.86108pt:\kern 0.86108pt}I\mathord{.\;}\exists
y\mathord{.\;}x_{0}.\mathit{nxt}\;i=y)$

It is easy to see that $x_{0}=\mathit{cons}\;\left\langle
o_{0},f_{0}\right\rangle$ and $f_{0}\;i=x_{0}.\mathit{nxt}\;i$.

$\varphi^{2}_{M}(\top)={}$

$\exists o_{1}{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}\mathit{cons}\;\left\langle
o_{1},X^{I}\right\rangle=\exists o_{1}{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}\exists f_{1}\mathord{.\;}\mathit{cons}\;\left\langle
o_{1},f_{1}\right\rangle\land(\forall i{\kern 0.86108pt:\kern
0.86108pt}I\mathord{.\;}\exists x_{2}\mathord{.\;}f_{1}\;i=x_{2}\land
x_{2}\in\varphi_{M}(\top))$. Again, it becomes more suggestive using the
destructors:

$\displaystyle\varphi^{2}_{M}(\top)$ $\displaystyle=\exists
x_{1}\mathord{.\;}\exists o_{1}{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}x_{1}\land(x_{1}.\mathit{out}=o_{1}\land\forall
i{\kern 0.86108pt:\kern 0.86108pt}I\mathord{.\;}\exists
x_{0}\mathord{.\;}x_{1}.\mathit{nxt}\;i=x_{0}\land x_{0}\in\varphi_{M}(\top))$
$\displaystyle=\exists x_{1}\mathord{.\;}\exists o_{1}{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}x_{1}\land(x_{1}.\mathit{out}=o_{1}\land\forall
i{\kern 0.86108pt:\kern 0.86108pt}I\mathord{.\;}\exists
x_{0}\mathord{.\;}\exists o_{0}{\kern 0.86108pt:\kern
0.86108pt}O\mathord{.\;}x_{0}.\mathit{out}=o_{0}\land\forall i{\kern
0.86108pt:\kern 0.86108pt}I\mathord{.\;}\exists
y\mathord{.\;}x_{0}.\mathit{nxt}\;i=y)$

…

We have $\top_{\\!\\!\nu M}\ni x\approxeq f\in O^{I^{*}}$ iff
$x.\mathit{out}=f\;\epsilon$ and $\forall i{\kern 0.86108pt:\kern
0.86108pt}I\mathord{.\;}x.\mathit{nxt}\;i=\overline{\mathit{tr}}(f)(i)$.

##  7 Conclusion

The technical experiments reported in this paper show that both the initial
models and the final models for polynomial functors can be fully captured in
matching logic (ML) using their representation as unary container functors.
The ML specification of the polynomial functors is possible due to the fact
the sum, product, and function sorts can be specified in ML [8], and these
specifications are a part of capturing the category of sets $\mathbb{C}$ in
ML.

A functor represented as a ”classical” polynomial can be translated into a
container functor shape using the fact the later are closed under sum,
product, and exponential. However, the result could be cumbersome and not easy
to handle in matching logic because the construction starts from constant and
identity functors. Therefore it is preferable to simplify it using the
isomorphisms in the category of sets.

This result can help in defining in ML programming languages using both
inductive data-types and coinductive data-types. Another advantage is given by
a better understanding of the abstract constructions from the category theory.
A possibly use is as follows:

  * •

define in front-end a suitable syntax for data types intended to be defined as
initial algebra or final coalgebra;

  * •

extract the canonical form of the functor underlying the front-end definition;

  * •

generate the corresponding ML theory;

  * •

derive the proof principles needed to soundly handle the defined data type.

Future work will focus on the following aspects of the proposed approach:

  * •

a more formal presentation of the approach;

  * •

how to capture in ML the iteration principle and the primitive recursive
principle;

  * •

extending the approach to larger classes of functors admitting initial
algebras and final coalgebras, e.g., indexed containers [4], the bounded
natural functors (BNFs) underlying Isabelle/HOL’s datatypes [17], or the
quotients of polynomial functors, experimentally implemented in Lean [6].

## References

  * [1]
  * [2] Michael Gordon Abbott, Thorsten Altenkirch & Neil Ghani (2005): _Containers: Constructing strictly positive types_.  Theor. Comput. Sci. 342(1), pp. 3–27, 10.1016/j.tcs.2005.06.002.
  * [3] Jirí Adámek (2003): _On final coalgebras of continuous functors_.  Theor. Comput. Sci. 294(1/2), pp. 3–29, 10.1016/S0304-3975(01)00240-7.
  * [4] Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride & Peter Morris (2015): _Indexed containers_.  J. Funct. Program. 25, 10.1017/S095679681500009X.
  * [5] Thorsten Altenkirch & Peter Morris (2009): _Indexed Containers_.  In: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, IEEE Computer Society, pp. 277–285, 10.1109/LICS.2009.33.
  * [6] Jeremy Avigad, Mario Carneiro & Simon Hudon (2019): _Data Types as Quotients of Polynomial Functors_.  In John Harrison, John O’Leary & Andrew Tolmach, editors: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, LIPIcs 141, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 6:1–6:19, 10.4230/LIPIcs.ITP.2019.6.
  * [7] Xiaohong Chen, Dorel Lucanu & Grigore Roşu (2020): _Initial Algebra Semantics in Matching Logic_.  Technical Report, University of Illinois at Urbana-Champaign.  Available at http://hdl.handle.net/2142/107781.
  * [8] Xiaohong Chen, Dorel Lucanu & Grigore Roşu (2021): _Matching logic explained_.  Journal of Logical and Algebraic Methods in Programming 120, pp. 1–36, 10.1016/j.jlamp.2021.100638.
  * [9] Xiaohong Chen & Grigore Roşu (2019): _Matching $\mu$-logic_.  In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’19), IEEE, Vancouver, Canada, pp. 1–13, 10.1109/LICS.2019.8785675.
  * [10] Xiaohong Chen & Grigore Roșu (2020): _A general approach to define binders using matching logic_.  Proc. ACM Program. Lang. 4(ICFP), pp. 88:1–88:32, 10.1145/3408970.
  * [11] Bart Jacobs & Jan Rutten (2012): _An introduction to (co)algebra and (co)induction_.  In Davide Sangiorgi & Jan J. M. M. Rutten, editors: Advanced Topics in Bisimulation and Coinduction, Cambridge tracts in theoretical computer science 52, Cambridge University Press, pp. 38–99.  Available at http://www.cambridge.org/gb/knowledge/isbn/item6542021.
  * [12] Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang & Grigore Roșu (2023): _Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier_.  Proc. ACM Program. Lang. 7(OOPSLA1), pp. 56–84, 10.1145/3586029.
  * [13] Grigore Roşu (2017): _Matching logic_.  Logical Methods in Computer Science 13(4), pp. 1–61, 10.23638/LMCS-13(4:28)2017.
  * [14] Grigore Roșu & Xiaohong Chen (2020): _Matching logic: the foundation of the K framework (invited talk)_.  In Jasmin Blanchette & Catalin Hritcu, editors: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, ACM, p. 1, 10.1145/3372885.3378574.
  * [15] Jan J. M. M. Rutten (2000): _Universal coalgebra: a theory of systems_.  Theor. Comput. Sci. 249(1), pp. 3–80, 10.1016/S0304-3975(00)00056-6.
  * [16] Davide Sangiorgi (2012): _An Introduction to Bisimulation and Coinduction_.  Cambridge University Press.  A preliminary version of Chapter 2 from which we adapt paterial can be found at http://www.cs.unibo.it/~sangio/DOC_public/corsoFL.pdf.
  * [17] Dmitriy Traytel, Andrei Popescu & Jasmin Christian Blanchette (2012): _Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving_.  In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, IEEE Computer Society, pp. 596–605, 10.1109/LICS.2012.75.

##  Appendix A Capturing Sort Operator in ML

We recall from [8] the ML specifications for the main operators over sorts.

###  A.1 Sum Sort

Given two sorts $s_{1}$ and $s_{2}$, we define a new sort
$s_{1}{\otimes}s_{2}$, called the _product (sort) of $s_{1}$ and $s_{2}$_, as
follows:

⬇

spec $\textsf{SUM}_{s_{1},s_{2}}$

Imports: SORT

Symbols: $\oplus,\iota_{1},\iota_{2},\epsilon_{1},\epsilon_{2}$

Notations: $s_{1}{\oplus}s_{2}\equiv{\oplus}\,s_{1}\,s_{2}$

Axioms:

(Sum Sort)

$s_{1}\in\top_{\\!\\!\top_{\\!\\!\mathit{Sort}}}\wedge
s_{2}\in\top_{\\!\\!\top_{\\!\\!\mathit{Sort}}}\rightarrow
s_{1}{\oplus}s_{2}\in\top_{\\!\\!\top_{\\!\\!\mathit{Sort}}}$

(Inject Left)

$\iota_{1}:{s_{1}}\to{s_{1}{\oplus}s_{2}}$

(Inject Right)

$\iota_{2}:{s_{2}}\to{s_{1}{\oplus}s_{2}}$

(Eject Left)

$\epsilon_{1}:{s_{1}{\oplus}s_{2}}\rightharpoonup{s_{1}}$

(Eject Right)

$\epsilon_{2}:{s_{1}{\oplus}s_{2}}\rightharpoonup{s_{2}}$

(Inverse InjEj1)

$\forall x{\kern 0.77498pt:\kern
0.77498pt}s_{i}\mathord{.\;}\epsilon_{i}\,(\iota_{i}\,x)=x,~{}i=1,2$

(Inverse InjEj2)

$\forall x{\kern 0.77498pt:\kern
0.77498pt}s_{3-i}\mathord{.\;}\epsilon_{i}\,(\iota_{3-i}\,x)=\bot,~{}i=1,2$

(CoProduct)

$\forall s_{1},s_{2}{\kern 0.77498pt:\kern
0.77498pt}\top_{\\!\\!\mathit{Sort}}\mathord{.\;}\top_{\\!\\!s_{1}{\oplus}s_{2}}\subseteq(\iota_{1}\,\top_{\\!\\!s_{1}})\lor(\iota_{2}\,\top_{\\!\\!s_{2}})$

endspec\end{lstlisting}

\subsection{Pair Sort}

\begin{lstlisting}[language=matchinglogic]

spec $\mathsf{PAIR}_{s_{1},s_{2}}$ Imports: $\mathsf{SORT}$

Symbols: $\mathit{Pair},\mathit{pair},\mathit{fst},\mathit{snd}$

Notations: $s_{1}\otimes s_{2}\equiv\mathit{Pair}\ s_{1}\ s_{2},$
$\left\langle\varphi_{1},\varphi_{2}\right\rangle\equiv\mathit{pair}\
\varphi_{1}\ \varphi_{2}$

Axioms: $\sslash$ all axioms are quantified by ‘‘$\forall s_{1},s_{2}{\kern
0.77498pt:\kern 0.77498pt}\top_{\\!\\!\mathit{Sort}}$’’

$\begin{array}[]{ll}\scalebox{0.95}[1.0]{{{(Pair Sort)}}}&(s_{1}\otimes
s_{2}){\kern 0.77498pt:\kern 0.77498pt}\mathit{Sort}\\\
\scalebox{0.95}[1.0]{{{(Pair)}}}&\forall x_{1}{\kern 0.77498pt:\kern
0.77498pt}s_{1}\mathord{.\;}\forall x_{2}{\kern 0.77498pt:\kern
0.77498pt}s_{2}\mathord{.\;}\left\langle x_{1},x_{2}\right\rangle{\kern
0.77498pt:\kern 0.77498pt}(s_{1}\otimes s_{2})\\\ \scalebox{0.95}[1.0]{{{(Pair
Fst)}}}&\forall x_{1}{\kern 0.77498pt:\kern
0.77498pt}s_{1}\mathord{.\;}\forall x_{2}{\kern 0.77498pt:\kern
0.77498pt}s_{2}\mathord{.\;}\mathit{fst}\ \left\langle
x_{1},x_{2}\right\rangle=x_{1}\\\ \scalebox{0.95}[1.0]{{{(Pair Snd)}}}&\forall
x_{1}{\kern 0.77498pt:\kern 0.77498pt}s_{1}\mathord{.\;}\forall x_{2}{\kern
0.77498pt:\kern 0.77498pt}s_{2}\mathord{.\;}\mathit{snd}\ \left\langle
x_{1},x_{2}\right\rangle=x_{2}\\\ \scalebox{0.95}[1.0]{{{(Pair Inj)}}}&\forall
x_{1},y_{1}{\kern 0.77498pt:\kern 0.77498pt}s_{1}\mathord{.\;}\forall
x_{2},y_{2}{\kern 0.77498pt:\kern 0.77498pt}s_{2}\mathord{.\;}\\\
&\quad\left\langle x_{1},x_{2}\right\rangle{=}\left\langle
y_{1},y_{2}\right\rangle\rightarrow x_{1}{=}x_{2}\land y_{1}{=}y_{2}\\\
\scalebox{0.95}[1.0]{{{(Pair Domain)}}}&\top_{\\!\\!s_{1}\otimes
s_{2}}=\left\langle\top_{\\!\\!s_{1}},\top_{\\!\\!s_{2}}\right\rangle\end{array}$

endspec

###  A.2 Function Sort

⬇

spec $\mathsf{FUN}_{s_{1},s_{2}}$ Imports: $\mathsf{SORT}$

Symbols: $\mathit{Function}$

Notations:
$s_{1}\mathbin{\textnormal{\small$\to$⃝}}s_{2}\equiv\mathit{Function}\ s_{1}\
s_{2}$

Axioms: // all axioms are quantified by ‘‘$\forall s_{1},s_{2}{\kern
0.77498pt:\kern 0.77498pt}\top_{\\!\\!\mathit{Sort}}$’’

$\begin{array}[]{ll}\scalebox{0.95}[1.0]{{{(Func
Sort)}}}&(s_{1}\mathbin{\textnormal{\small$\to$⃝}}s_{2}){\kern 0.77498pt:\kern
0.77498pt}\mathit{Sort}\\\ \scalebox{0.95}[1.0]{{{(Func
Domain)}}}\\!\\!\\!&\top_{\\!\\!s_{1}\mathbin{\textnormal{\scriptsize$\to$⃝}}s_{2}}=\exists
f\mathord{.\;}f\land\forall x{\kern 0.77498pt:\kern
0.77498pt}s_{1}\mathord{.\;}(f\,x){\kern 0.77498pt:\kern 0.77498pt}s_{2}\\\
\scalebox{0.95}[1.0]{{{(Func Ext)}}}&\forall f,g{\kern 0.77498pt:\kern
0.77498pt}s_{1}{\mathbin{\textnormal{\small$\to$⃝}}}s_{2}\mathord{.\;}(\forall
x{\kern 0.77498pt:\kern 0.77498pt}s_{1}\mathord{.\;}f\ x=g\
x)\,{\rightarrow}\,f\,{=}\,g\end{array}$

endspec

######  Remark.

Note that we do not explicitly define the constructors of function sorts.
Instead, we axiomatize the _behaviors_ of a function. Indeed, axiom  (Func
Domain) states that a “function” $f$ of sort
$s_{1}\mathbin{\textnormal{\small$\to$⃝}}s_{2}$ is one such that for any $x$
of sort $s_{1}$, $(f\ x)$ has sort $s_{2}$. Axiom  (Func Ext) states that two
functions $f$ and $g$ of sort $s_{1}\mathbin{\textnormal{\small$\to$⃝}}s_{2}$
are equal iff they are behavioral equivalent, i.e., they return the same
values on all arguments of sort $s_{1}$.